feat(linear_algebra/bilinear_form): Existence of orthogonal basis wit…

…h respect to a bilinear form (#5814)

We state and prove the result that there exists an orthogonal basis with respect to a symmetric nondegenerate.

docs/undergrad.yaml

@@ -196,7 +196,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     bilinear forms: 'bilin_form'
     alternating bilinear forms: 'alt_bilin_form.is_alt'
     symmetric bilinear forms: 'sym_bilin_form.is_sym'
-    nondegenerate forms:
+    nondegenerate forms: 'bilin_form.nondegenerate'
     matrix representation: 'bilin_form.to_matrix'
     change of coordinates: 'bilin_form.to_matrix_comp'
     rank of a bilinear form:

src/linear_algebra/basic.lean

@@ -1580,6 +1580,15 @@ submodule.map_smul f _ a h
 lemma range_smul' (f : V →ₗ[K] V₂) (a : K) : range (a • f) = ⨆(h : a ≠ 0), range f :=
 submodule.map_smul' f _ a
 
+lemma span_singleton_sup_ker_eq_top (f : V →ₗ[K] K) {x : V} (hx : f x ≠ 0) :
+  (K ∙ x) ⊔ f.ker = ⊤ :=
+eq_top_iff.2 (λ y hy, submodule.mem_sup.2 ⟨(f y * (f x)⁻¹) • x,
+  submodule.mem_span_singleton.2 ⟨f y * (f x)⁻¹, rfl⟩,
+    ⟨y - (f y * (f x)⁻¹) • x,
+      by rw [linear_map.mem_ker, f.map_sub, f.map_smul, smul_eq_mul, mul_assoc,
+             inv_mul_cancel hx, mul_one, sub_self],
+      by simp only [add_sub_cancel'_right]⟩⟩)
+
 end field
 
 end linear_map

src/linear_algebra/bilinear_form.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Andreas Swerdlow. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Andreas Swerdlow
+Author: Andreas Swerdlow, Kexing Ying
 -/
 
 import linear_algebra.matrix
@@ -13,14 +13,18 @@ import linear_algebra.nonsingular_inverse
 
 This file defines a bilinear form over a module. Basic ideas
 such as orthogonality are also introduced, as well as reflexivive,
-symmetric and alternating bilinear forms. Adjoints of linear maps
-with respect to a bilinear form are also introduced.
+symmetric, non-degenerate and alternating bilinear forms. Adjoints of
+linear maps with respect to a bilinear form are also introduced.
 
 A bilinear form on an R-(semi)module M, is a function from M x M to R,
 that is linear in both arguments. Comments will typically abbreviate
 "(semi)module" as just "module", but the definitions should be as general as
 possible.
 
+The result that there exists an orthogonal basis with respect to a symmetric,
+nondegenerate bilinear form can be found in `quadratic_form.lean` with
+`exists_orthogonal_basis`.
+
 ## Notations
 
 Given any term B of type bilin_form, due to a coercion, can use
@@ -29,8 +33,9 @@ the notation B x y to refer to the function field, ie. B x y = B.bilin x y.
 In this file we use the following type variables:
  - `M`, `M'`, ... are semimodules over the semiring `R`,
  - `M₁`, `M₁'`, ... are modules over the ring `R₁`,
- - `M₂`, `M₂'`, ... are semimodules over the commutative semiring `R₂`
- - `M₃`, `M₃'`, ... are modules over the commutative ring `R₃`
+ - `M₂`, `M₂'`, ... are semimodules over the commutative semiring `R₂`,
+ - `M₃`, `M₃'`, ... are modules over the commutative ring `R₃`,
+ - `V`, ... is a semimodule over the field `K`.
 
 ## References
 
@@ -57,13 +62,16 @@ variables {R : Type u} {M : Type v} [semiring R] [add_comm_monoid M] [semimodule
 variables {R₁ : Type u} {M₁ : Type v} [ring R₁] [add_comm_group M₁] [module R₁ M₁]
 variables {R₂ : Type u} {M₂ : Type v} [comm_semiring R₂] [add_comm_monoid M₂] [semimodule R₂ M₂]
 variables {R₃ : Type u} {M₃ : Type v} [comm_ring R₃] [add_comm_group M₃] [module R₃ M₃]
+variables {V : Type u} {K : Type v} [field K] [add_comm_group V] [vector_space K V]
 variables {B : bilin_form R M} {B₁ : bilin_form R₁ M₁} {B₂ : bilin_form R₂ M₂}
 
 namespace bilin_form
 
 instance : has_coe_to_fun (bilin_form R M) :=
 ⟨_, λ B, B.bilin⟩
 
+initialize_simps_projections bilin_form (bilin -> apply)
+
 @[simp] lemma coe_fn_mk (f : M → M → R) (h₁ h₂ h₃ h₄) :
   (bilin_form.mk f h₁ h₂ h₃ h₄ : M → M → R) = f :=
 rfl
@@ -356,13 +364,33 @@ rfl
 
 end lin_mul_lin
 
-/-- The proposition that two elements of a bilinear form space are orthogonal -/
+/-- The proposition that two elements of a bilinear form space are orthogonal. For orthogonality
+of an indexed set of elements, use `bilin_form.is_Ortho`. -/
 def is_ortho (B : bilin_form R M) (x y : M) : Prop :=
 B x y = 0
 
-lemma ortho_zero (x : M) : is_ortho B (0 : M) x :=
+lemma is_ortho_def {B : bilin_form R M} {x y : M} :
+  B.is_ortho x y ↔ B x y = 0 := iff.rfl
+
+lemma is_ortho_zero_left (x : M) : is_ortho B (0 : M) x :=
 zero_left x
 
+lemma is_ortho_zero_right (x : M) : is_ortho B x (0 : M) :=
+zero_right x
+
+lemma ne_zero_of_not_is_ortho_self {B : bilin_form K V}
+  (x : V) (hx₁ : ¬ B.is_ortho x x) : x ≠ 0 :=
+λ hx₂, hx₁ (hx₂.symm ▸ is_ortho_zero_left _)
+
+/-- A set of vectors `v` is orthogonal with respect to some bilinear form `B` if and only
+if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use
+`bilin_form.is_ortho` -/
+def is_Ortho {n : Type w} (B : bilin_form R M) (v : n → M) : Prop :=
+∀ i j : n, i ≠ j → B.is_ortho (v j) (v i)
+
+lemma is_Ortho_def {n : Type w} {B : bilin_form R M} {v : n → M} :
+  B.is_Ortho v ↔ ∀ i j : n, i ≠ j → B (v j) (v i) = 0 := iff.rfl
+
 section
 
 variables {R₄ M₄ : Type*} [domain R₄] [add_comm_group M₄] [module R₄ M₄] {G : bilin_form R₄ M₄}
@@ -393,6 +421,32 @@ begin
   { rw [smul_right, H, mul_zero] },
 end
 
+/-- A set of orthogonal vectors `v` with respect to some bilinear form `B` is linearly independent
+  if for all `i`, `B (v i) (v i) ≠ 0`. -/
+lemma linear_independent_of_is_Ortho
+  {n : Type w} {B : bilin_form K V} {v : n → V}
+  (hv₁ : B.is_Ortho v) (hv₂ : ∀ i, ¬ B.is_ortho (v i) (v i)) :
+  linear_independent K v :=
+begin
+  classical,
+  rw linear_independent_iff',
+  intros s w hs i hi,
+  have : B (s.sum $ λ (i : n), w i • v i) (v i) = 0,
+  { rw [hs, zero_left] },
+  have hsum : s.sum (λ (j : n), w j * B (v j) (v i)) =
+    s.sum (λ (j : n), if i = j then w j * B (v j) (v i) else 0),
+  { refine finset.sum_congr rfl (λ j hj, _),
+    by_cases (i = j),
+    { rw [if_pos h] },
+    { rw [if_neg h, is_Ortho_def.1 hv₁ _ _ h, mul_zero] } },
+  simp_rw [map_sum_left, smul_left, hsum, finset.sum_ite_eq] at this,
+  rw [if_pos, mul_eq_zero] at this,
+  cases this,
+  { assumption },
+  { exact false.elim (hv₂ i $ this) },
+  { assumption }
+end
+
 end
 
 section is_basis
@@ -505,6 +559,17 @@ rfl
 lemma matrix.to_bilin'_apply (M : matrix n n R₃) (x y : n → R₃) :
   matrix.to_bilin' M x y = ∑ i j, x i * M i j * y j := rfl
 
+lemma matrix.to_bilin'_apply' (M : matrix n n R₃) (v w : n → R₃) :
+  matrix.to_bilin' M v w = matrix.dot_product v (M.mul_vec w) :=
+begin
+  simp_rw [matrix.to_bilin'_apply, matrix.dot_product,
+           matrix.mul_vec, matrix.dot_product],
+  refine finset.sum_congr rfl (λ _ _, _),
+  rw finset.mul_sum,
+  refine finset.sum_congr rfl (λ _ _, _),
+  rw ← mul_assoc,
+end
+
 @[simp] lemma matrix.to_bilin'_std_basis (M : matrix n n R₃) (i j : n) :
   matrix.to_bilin' M (std_basis R₃ (λ _, R₃) i 1) (std_basis R₃ (λ _, R₃) j 1) =
     M i j :=
@@ -1020,3 +1085,154 @@ begin
 end
 
 end matrix_adjoints
+
+namespace bilin_form
+
+section orthogonal
+
+/-- The orthogonal complement of a submodule `N` with respect to some bilinear form is the set of
+elements `x` which are orthogonal to all elements of `N`; i.e., for all `y` in `N`, `B x y = 0`.
+
+Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
+chirality; in addition to this "left" orthogonal complement one could define a "right" orthogonal
+complement for which, for all `y` in `N`, `B y x = 0`.  This variant definition is not currently
+provided in mathlib. -/
+def orthogonal (B : bilin_form R M) (N : submodule R M) : submodule R M :=
+{ carrier := { m | ∀ n ∈ N, is_ortho B n m },
+  zero_mem' := λ x _, is_ortho_zero_right x,
+  add_mem' := λ x y hx hy n hn,
+    by rw [is_ortho, add_right, show B n x = 0, by exact hx n hn,
+        show B n y = 0, by exact hy n hn, zero_add],
+  smul_mem' := λ c x hx n hn,
+    by rw [is_ortho, smul_right, show B n x = 0, by exact hx n hn, mul_zero] }
+
+variables {N L : submodule R M}
+
+@[simp] lemma mem_orthogonal_iff {N : submodule R M} {m : M} :
+  m ∈ B.orthogonal N ↔ ∀ n ∈ N, is_ortho B n m := iff.rfl
+
+lemma orthogonal_le (h : N ≤ L) : B.orthogonal L ≤ B.orthogonal N :=
+λ _ hn l hl, hn l (h hl)
+
+lemma le_orthogonal_orthogonal (hB : refl_bilin_form.is_refl B) :
+  N ≤ B.orthogonal (B.orthogonal N) :=
+λ n hn m hm, hB _ _ (hm n hn)
+
+-- ↓ This lemma only applies in fields as we require `a * b = 0 → a = 0 ∨ b = 0`
+lemma span_singleton_inf_orthogonal_eq_bot
+  {B : bilin_form K V} {x : V} (hx : ¬ B.is_ortho x x) :
+  (K ∙ x) ⊓ B.orthogonal (K ∙ x) = ⊥ :=
+begin
+  rw ← finset.coe_singleton,
+  refine eq_bot_iff.2 (λ y h, _),
+  rcases mem_span_finset.1 h.1 with ⟨μ, rfl⟩,
+  have := h.2 x _,
+  { rw finset.sum_singleton at this ⊢,
+    suffices hμzero : μ x = 0,
+    { rw [hμzero, zero_smul, submodule.mem_bot] },
+    change B x (μ x • x) = 0 at this, rw [smul_right] at this,
+    exact or.elim (zero_eq_mul.mp this.symm) id (λ hfalse, false.elim $ hx hfalse) },
+  { rw submodule.mem_span; exact λ _ hp, hp $ finset.mem_singleton_self _ }
+end
+
+-- ↓ This lemma only applies in fields since we use the `mul_eq_zero`
+lemma orthogonal_span_singleton_eq_to_lin_ker {B : bilin_form K V} (x : V) :
+  B.orthogonal (K ∙ x) = (bilin_form.to_lin B x).ker :=
+begin
+  ext y,
+  simp_rw [mem_orthogonal_iff, linear_map.mem_ker,
+           submodule.mem_span_singleton ],
+  split,
+  { exact λ h, h x ⟨1, one_smul _ _⟩ },
+  { rintro h _ ⟨z, rfl⟩,
+    rw [is_ortho, smul_left, mul_eq_zero],
+    exact or.intro_right _ h }
+end
+
+lemma span_singleton_sup_orthogonal_eq_top {B : bilin_form K V}
+  {x : V} (hx : ¬ B.is_ortho x x) :
+  (K ∙ x) ⊔ B.orthogonal (K ∙ x) = ⊤ :=
+begin
+  rw orthogonal_span_singleton_eq_to_lin_ker,
+  exact linear_map.span_singleton_sup_ker_eq_top _ hx,
+end
+
+/-- Given a bilinear form `B` and some `x` such that `B x x ≠ 0`, the span of the singleton of `x`
+  is complement to its orthogonal complement. -/
+lemma is_compl_span_singleton_orthogonal {B : bilin_form K V}
+  {x : V} (hx : ¬ B.is_ortho x x) : is_compl (K ∙ x) (B.orthogonal $ K ∙ x) :=
+{ inf_le_bot := eq_bot_iff.1 $ span_singleton_inf_orthogonal_eq_bot hx,
+  top_le_sup := eq_top_iff.1 $ span_singleton_sup_orthogonal_eq_top hx }
+
+end orthogonal
+
+/-- The restriction of a bilinear form on a submodule. -/
+@[simps apply]
+def restrict (B : bilin_form R M) (W : submodule R M) : bilin_form R W :=
+{ bilin := λ a b, B a b,
+  bilin_add_left := λ _ _ _, add_left _ _ _,
+  bilin_smul_left := λ _ _ _, smul_left _ _ _,
+  bilin_add_right := λ _ _ _, add_right _ _ _,
+  bilin_smul_right := λ _ _ _, smul_right _ _ _}
+
+/-- The restriction of a symmetric bilinear form on a submodule is also symmetric. -/
+lemma restrict_sym (B : bilin_form R M) (hB : sym_bilin_form.is_sym B)
+  (W : submodule R M) : sym_bilin_form.is_sym $ B.restrict W :=
+λ x y, hB x y
+
+/-- A nondegenerate bilinear form is a bilinear form such that the only element that is orthogonal
+to every other element is `0`; i.e., for all nonzero `m` in `M`, there exists `n` in `M` with
+`B m n ≠ 0`.
+
+Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a
+chirality; in addition to this "left" nondegeneracy condition one could define a "right"
+nondegeneracy condition that in the situation described, `B n m ≠ 0`.  This variant definition is
+not currently provided in mathlib. In finite dimension either definition implies the other. -/
+def nondegenerate (B : bilin_form R M) : Prop :=
+∀ m : M, (∀ n : M, B m n = 0) → m = 0
+
+/-- A bilinear form is nondegenerate if and only if it has a trivial kernel. -/
+theorem nondegenerate_iff_ker_eq_bot {B : bilin_form R₂ M₂} :
+  B.nondegenerate ↔ B.to_lin.ker = ⊥ :=
+begin
+  rw linear_map.ker_eq_bot',
+  split; intro h,
+  { refine λ m hm, h _ (λ x, _),
+    rw [← to_linear_map_apply, hm], refl },
+  { intros m hm, apply h,
+    ext, exact hm x }
+end
+
+section
+
+variable [finite_dimensional K V]
+
+/-- Given a nondegenerate bilinear form `B` on a finite-dimensional vector space, `B.to_dual` is
+the linear equivalence between a vector space and its dual with the underlying linear map
+`B.to_lin`. -/
+noncomputable def to_dual (B : bilin_form K V) (hB : B.nondegenerate) :
+  V ≃ₗ[K] module.dual K V :=
+B.to_lin.linear_equiv_of_ker_eq_bot
+  (nondegenerate_iff_ker_eq_bot.mp hB) subspace.dual_findim_eq.symm
+
+lemma to_dual_def {B : bilin_form K V} (hB : B.nondegenerate) {m n : V} :
+  B.to_dual hB m n = B m n := rfl
+
+end
+
+/-- The restriction of a symmetric, non-degenerate bilinear form on the orthogonal complement of 
+the span of a singleton is also non-degenerate. -/
+lemma restrict_orthogonal_span_singleton_nondegenerate (B : bilin_form K V)
+  (hB₁ : nondegenerate B) (hB₂ : sym_bilin_form.is_sym B) {x : V} (hx : ¬ B.is_ortho x x) :
+  nondegenerate $ B.restrict $ B.orthogonal (K ∙ x) :=
+begin
+  refine λ m hm, submodule.coe_eq_zero.1 (hB₁ m.1 (λ n, _)),
+  have : n ∈ (K ∙ x) ⊔ B.orthogonal (K ∙ x) :=
+    (span_singleton_sup_orthogonal_eq_top hx).symm ▸ submodule.mem_top,
+  rcases submodule.mem_sup.1 this with ⟨y, hy, z, hz, rfl⟩,
+  specialize hm ⟨z, hz⟩,
+  rw restrict at hm,
+  erw [add_right, show B m.1 y = 0, by rw hB₂; exact m.2 y hy, hm, add_zero]
+end
+
+end bilin_form

src/linear_algebra/dual.lean

@@ -525,6 +525,15 @@ end
 
 variables [finite_dimensional K V] [finite_dimensional K V₁]
 
+@[simp] lemma dual_findim_eq :
+  findim K (module.dual K V) = findim K V :=
+begin
+  obtain ⟨n, hn, hf⟩ := exists_is_basis_finite K V,
+  refine linear_equiv.findim_eq _,
+  haveI : fintype n := set.finite.fintype hf,
+  refine (hn.to_dual_equiv _).symm,
+end
+
 /-- The quotient by the dual is isomorphic to its dual annihilator.  -/
 noncomputable def quot_dual_equiv_annihilator (W : subspace K V) :
   W.dual_lift.range.quotient ≃ₗ[K] W.dual_annihilator :=

src/linear_algebra/finite_dimensional.lean

@@ -903,6 +903,20 @@ calc  findim K V
 ... = findim K f.range : by rw [ker_eq_bot.2 hf, findim_bot, add_zero]
 ... ≤ findim K V₂ : submodule.findim_le _
 
+/-- Given a linear map `f` between two vector spaces with the same dimension, if
+`ker f = ⊥` then `linear_equiv_of_ker_eq_bot` is the induced isomorphism
+between the two vector spaces. -/
+noncomputable def linear_equiv_of_ker_eq_bot
+  [finite_dimensional K V] [finite_dimensional K V₂]
+  (f : V →ₗ[K] V₂) (hf : f.ker = ⊥) (hdim : findim K V = findim K V₂) : V ≃ₗ[K] V₂ :=
+linear_equiv.of_bijective f hf (linear_map.range_eq_top.2 $
+  (linear_map.injective_iff_surjective_of_findim_eq_findim hdim).1 (linear_map.ker_eq_bot.1 hf))
+
+@[simp] lemma linear_equiv_of_ker_eq_bot_apply
+  [finite_dimensional K V] [finite_dimensional K V₂]
+  {f : V →ₗ[K] V₂} (hf : f.ker = ⊥) (hdim : findim K V = findim K V₂) (x : V) :
+  f.linear_equiv_of_ker_eq_bot hf hdim x = f x := rfl
+
 end linear_map
 
 namespace alg_hom
@@ -968,6 +982,15 @@ begin
   apply not_le_of_lt hst h_eq_top,
 end
 
+lemma findim_add_eq_of_is_compl
+  [finite_dimensional K V] {U W : submodule K V} (h : is_compl U W) :
+  findim K U + findim K W = findim K V :=
+begin
+  rw [← submodule.dim_sup_add_dim_inf_eq, top_le_iff.1 h.2, le_bot_iff.1 h.1,
+      findim_bot, add_zero],
+  exact findim_top
+end
+
 end submodule
 
 section span