feat(linear_algebra/sesquilinear_form): preliminary results for nondegeneracy (#12269)

Several lemmas needed to define nondegenerate bilinear forms and show that the canonical pairing of the algebraic dual is nondegenerate.

Add domain restriction of bilinear maps in the second component and in both compenents.

Some type-class generalizations for symmetric, alternating, and reflexive sesquilinear forms.

Author: mcdoll

src/algebra/quandle.lean

@@ -595,7 +595,7 @@ def to_envel_group.map {R : Type*} [rack R] {G : Type*} [group G] :
   { to_fun := λ x, quotient.lift_on x (to_envel_group.map_aux f)
                     (λ a b ⟨hab⟩, to_envel_group.map_aux.well_def f hab),
     map_one' := begin
-      change quotient.lift_on ⟦unit⟧ (to_envel_group.map_aux f) _ = 1,
+      change quotient.lift_on ⟦rack.pre_envel_group.unit⟧ (to_envel_group.map_aux f) _ = 1,
       simp [to_envel_group.map_aux],
     end,
     map_mul' := λ x y, quotient.induction_on₂ x y (λ x y, begin

src/linear_algebra/bilinear_form.lean

@@ -634,11 +634,6 @@ end
 
 end basis
 
-end bilin_form
-
-
-namespace bilin_form
-
 /-- The proposition that a bilinear form is reflexive -/
 def is_refl (B : bilin_form R M) : Prop := ∀ (x y : M), B x y = 0 → B y x = 0
 
@@ -748,7 +743,6 @@ lemma is_adjoint_pair.sub (h : is_adjoint_pair B₁ B₁' f₁ g₁) (h' : is_ad
   is_adjoint_pair B₁ B₁' (f₁ - f₁') (g₁ - g₁') :=
 λ x y, by rw [linear_map.sub_apply, linear_map.sub_apply, sub_left, sub_right, h, h']
 
-variables {M₂' : Type*} [add_comm_monoid M₂'] [module R₂ M₂']
 variables {B₂' : bilin_form R₂ M₂'} {f₂ f₂' : M₂ →ₗ[R₂] M₂'} {g₂ g₂' : M₂' →ₗ[R₂] M₂}
 
 lemma is_adjoint_pair.smul (c : R₂) (h : is_adjoint_pair B₂ B₂' f₂ g₂) :

src/linear_algebra/bilinear_map.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Mario Carneiro
 -/
 
 import linear_algebra.basic
+import linear_algebra.basis
 
 /-!
 # Basics on bilinear maps
@@ -29,6 +30,8 @@ commuting actions, and `ρ₁₂ : R →+* R₂` and `σ₁₂ : S →+* S₂`.
 bilinear
 -/
 
+variables {ι₁ ι₂ : Type*}
+
 namespace linear_map
 
 section semiring
@@ -89,6 +92,9 @@ theorem ext₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
   (H : ∀ m n, f m n = g m n) : f = g :=
 linear_map.ext (λ m, linear_map.ext $ λ n, H m n)
 
+lemma congr_fun₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : f = g) (x y) : f x y = g x y :=
+linear_map.congr_fun (linear_map.congr_fun h x) y
+
 section
 
 local attribute [instance] smul_comm_class.symm
@@ -106,6 +112,9 @@ end
 
 @[simp] theorem flip_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (m : M) (n : N) : flip f n m = f m n := rfl
 
+@[simp] lemma flip_flip [smul_comm_class R₂ S₂ P] (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) :
+  f.flip.flip = f := linear_map.ext₂ (λ x y, ((f.flip).flip_apply _ _).trans (f.flip_apply _ _))
+
 open_locale big_operators
 
 variables {R}
@@ -134,6 +143,24 @@ theorem map_sum₂ {ι : Type*} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂]
   f (∑ i in t, x i) y = ∑ i in t, f (x i) y :=
 (flip f y).map_sum
 
+/-- Restricting a bilinear map in the second entry -/
+def dom_restrict₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : submodule S N) :
+  M →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P :=
+{ to_fun := λ m, (f m).dom_restrict q,
+  map_add' := λ m₁ m₂, linear_map.ext $ λ _, by simp only [map_add, dom_restrict_apply, add_apply],
+  map_smul' := λ c m, linear_map.ext $ λ _, by simp only [map_smulₛₗ, dom_restrict_apply,
+    smul_apply]}
+
+lemma dom_restrict₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (q : submodule S N) (x : M) (y : q) :
+  f.dom_restrict₂ q x y = f x y := rfl
+
+/-- Restricting a bilinear map in both components -/
+def dom_restrict₁₂ (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : submodule R M) (q : submodule S N) :
+  p →ₛₗ[ρ₁₂] q →ₛₗ[σ₁₂] P := (f.dom_restrict p).dom_restrict₂ q
+
+lemma dom_restrict₁₂_apply (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (p : submodule R M) (q : submodule S N)
+  (x : p) (y : q) : f.dom_restrict₁₂ p q x y = f x y := rfl
+
 end semiring
 
 section comm_semiring
@@ -243,7 +270,13 @@ end comm_semiring
 
 section comm_ring
 
-variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
+variables {R R₂ S S₂ M N P : Type*}
+variables [comm_ring R] [comm_ring S] [comm_ring R₂] [comm_ring S₂]
+variables [add_comm_group M] [add_comm_group N] [add_comm_group P]
+variables [module R M] [module S N] [module R₂ P] [module S₂ P]
+variables [smul_comm_class S₂ R₂ P]
+variables {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
+variables (b₁ : basis ι₁ R M) (b₂ : basis ι₂ S N)
 
 lemma lsmul_injective [no_zero_smul_divisors R M] {x : R} (hx : x ≠ 0) :
   function.injective (lsmul R M x) :=
@@ -253,6 +286,22 @@ lemma ker_lsmul [no_zero_smul_divisors R M] {a : R} (ha : a ≠ 0) :
   (linear_map.lsmul R M a).ker = ⊥ :=
 linear_map.ker_eq_bot_of_injective (linear_map.lsmul_injective ha)
 
+
+/-- Two bilinear maps are equal when they are equal on all basis vectors. -/
+lemma ext_basis {B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}
+  (h : ∀ i j, B (b₁ i) (b₂ j) = B' (b₁ i) (b₂ j)) : B = B' :=
+b₁.ext $ λ i, b₂.ext $ λ j, h i j
+
+/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis. -/
+lemma sum_repr_mul_repr_mul {B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (x y) :
+  (b₁.repr x).sum (λ i xi, (b₂.repr y).sum (λ j yj, (ρ₁₂ xi) • (σ₁₂ yj) • B (b₁ i) (b₂ j))) =
+  B x y :=
+begin
+  conv_rhs { rw [← b₁.total_repr x, ← b₂.total_repr y] },
+  simp_rw [finsupp.total_apply, finsupp.sum, map_sum₂, map_sum, map_smulₛₗ₂, map_smulₛₗ],
+end
+
+
 end comm_ring
 
 end linear_map

src/linear_algebra/linear_pmap.lean

@@ -113,6 +113,15 @@ This version works for modules over division rings. -/
 mk_span_singleton' x y $ λ c hc, (smul_eq_zero.1 hc).elim
   (λ hc, by rw [hc, zero_smul]) (λ hx', absurd hx' hx)
 
+lemma mk_span_singleton_apply' (K : Type*) {E F : Type*} [division_ring K]
+  [add_comm_group E] [module K E] [add_comm_group F] [module K F] {x : E} (hx : x ≠ 0) (y : F):
+  (mk_span_singleton x y hx).to_fun
+  ⟨x, (submodule.mem_span_singleton_self x : x ∈ submodule.span K {x})⟩ = y :=
+begin
+  convert linear_pmap.mk_span_singleton_apply x y _ (1 : K) _;
+  simp [submodule.mem_span_singleton_self],
+end
+
 /-- Projection to the first coordinate as a `linear_pmap` -/
 protected def fst (p : submodule R E) (p' : submodule R F) : linear_pmap R (E × F) E :=
 { domain := p.prod p',

src/linear_algebra/matrix/bilinear_form.lean

@@ -179,7 +179,7 @@ begin
   simp only [bilin_form.to_matrix'_apply, bilin_form.comp_apply, transpose_apply, matrix.mul_apply,
     linear_map.to_matrix', linear_equiv.coe_mk, sum_mul],
   rw sum_comm,
-  conv_lhs { rw ← sum_repr_mul_repr_mul (pi.basis_fun R₃ n) (l _) (r _) },
+  conv_lhs { rw ← bilin_form.sum_repr_mul_repr_mul (pi.basis_fun R₃ n) (l _) (r _) },
   rw finsupp.sum_fintype,
   { apply sum_congr rfl,
     rintros i' -,
@@ -310,7 +310,7 @@ begin
   simp only [bilin_form.to_matrix_apply, bilin_form.comp_apply, transpose_apply, matrix.mul_apply,
     linear_map.to_matrix', linear_equiv.coe_mk, sum_mul],
   rw sum_comm,
-  conv_lhs { rw ← sum_repr_mul_repr_mul b },
+  conv_lhs { rw ← bilin_form.sum_repr_mul_repr_mul b },
   rw finsupp.sum_fintype,
   { apply sum_congr rfl,
     rintros i' -,

src/linear_algebra/sesquilinear_form.lean

@@ -6,6 +6,8 @@ Authors: Andreas Swerdlow
 import algebra.module.linear_map
 import linear_algebra.bilinear_map
 import linear_algebra.matrix.basis
+import linear_algebra.dual
+import linear_algebra.linear_pmap
 
 /-!
 # Sesquilinear form
@@ -52,24 +54,38 @@ variables [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module
 /-- The proposition that two elements of a sesquilinear form space are orthogonal -/
 def is_ortho (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x y) : Prop := B x y = 0
 
-lemma is_ortho_def {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} {x y} :
-  B.is_ortho x y ↔ B x y = 0 := iff.rfl
+lemma is_ortho_def {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R} {x y} : B.is_ortho x y ↔ B x y = 0 := iff.rfl
 
 lemma is_ortho_zero_left (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x) : is_ortho B (0 : M₁) x :=
-  by { dunfold is_ortho, rw [ map_zero B, zero_apply] }
+by { dunfold is_ortho, rw [ map_zero B, zero_apply] }
 
 lemma is_ortho_zero_right (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] R) (x) : is_ortho B x (0 : M₂) :=
-  map_zero (B x)
+map_zero (B x)
+
+lemma is_ortho_flip {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R} {x y} :
+  B.is_ortho x y ↔ B.flip.is_ortho y x :=
+by simp_rw [is_ortho_def, flip_apply]
 
 /-- 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*} (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R) (v : n → M₁) : Prop :=
+def is_Ortho (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R) (v : n → M₁) : Prop :=
 pairwise (B.is_ortho on v)
 
-lemma is_Ortho_def {n : Type*} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R} {v : n → M₁} :
+lemma is_Ortho_def {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R} {v : n → M₁} :
   B.is_Ortho v ↔ ∀ i j : n, i ≠ j → B (v i) (v j) = 0 := iff.rfl
 
+lemma is_Ortho_flip (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R) {v : n → M₁} :
+  B.is_Ortho v ↔ B.flip.is_Ortho v :=
+begin
+  simp_rw is_Ortho_def,
+  split; intros h i j hij,
+  { rw flip_apply,
+    exact h j i (ne.symm hij) },
+  simp_rw flip_apply at h,
+  exact h j i (ne.symm hij),
+end
+
 end comm_ring
 section field
 
@@ -127,14 +143,15 @@ end
 
 end field
 
-variables [comm_ring R] [add_comm_group M] [module R M]
-  [comm_ring R₁] [add_comm_group M₁] [module R₁ M₁]
-  {I : R →+* R} {I₁ : R₁ →+* R} {I₂ : R₁ →+* R}
-  {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
-  {B' : M →ₗ[R] M →ₛₗ[I] R}
 
 /-! ### Reflexive bilinear forms -/
 
+section reflexive
+
+variables [comm_semiring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁]
+  {I₁ : R₁ →+* R} {I₂ : R₁ →+* R}
+  {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
+
 /-- The proposition that a sesquilinear form is reflexive -/
 def is_refl (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) : Prop :=
   ∀ (x y), B x y = 0 → B y x = 0
@@ -148,28 +165,56 @@ lemma eq_zero : ∀ {x y}, B x y = 0 → B y x = 0 := λ x y, H x y
 lemma ortho_comm {x y} : is_ortho B x y ↔ is_ortho B y x := ⟨eq_zero H, eq_zero H⟩
 
 end is_refl
+end reflexive
 
 /-! ### Symmetric bilinear forms -/
 
+section symmetric
+
+variables [comm_semiring R] [add_comm_monoid M] [module R M]
+  {I : R →+* R} {B : M →ₛₗ[I] M →ₗ[R] R}
+
 /-- The proposition that a sesquilinear form is symmetric -/
-def is_symm (B : M →ₗ[R] M →ₛₗ[I] R) : Prop :=
+def is_symm (B : M →ₛₗ[I] M →ₗ[R] R) : Prop :=
   ∀ (x y), I (B x y) = B y x
 
 namespace is_symm
 
-variable (H : B'.is_symm)
-include H
+protected lemma eq (H : B.is_symm) (x y) : I (B x y) = B y x := H x y
 
-protected lemma eq (x y) : (I (B' x y)) = B' y x := H x y
+lemma is_refl (H : B.is_symm) : B.is_refl := λ x y H1, by { rw ←H.eq, simp [H1] }
 
-lemma is_refl : B'.is_refl := λ x y H1, by { rw [←H], simp [H1] }
+lemma ortho_comm (H : B.is_symm) {x y} : is_ortho B x y ↔ is_ortho B y x := H.is_refl.ortho_comm
 
-lemma ortho_comm {x y} : is_ortho B' x y ↔ is_ortho B' y x := H.is_refl.ortho_comm
+lemma dom_restrict_symm (H : B.is_symm) (p : submodule R M) : (B.dom_restrict₁₂ p p).is_symm :=
+begin
+  intros x y,
+  simp_rw dom_restrict₁₂_apply,
+  exact H x y,
+end
 
 end is_symm
 
+lemma is_symm_iff_eq_flip {B : M →ₗ[R] M →ₗ[R] R} : B.is_symm ↔ B = B.flip :=
+begin
+  split; intro h,
+  { ext,
+    rw [←h, flip_apply, ring_hom.id_apply] },
+  intros x y,
+  conv_lhs { rw h },
+  rw [flip_apply, ring_hom.id_apply],
+end
+
+end symmetric
+
+
 /-! ### Alternating bilinear forms -/
 
+section alternating
+
+variables [comm_ring R] [comm_semiring R₁] [add_comm_monoid M₁] [module R₁ M₁]
+  {I₁ : R₁ →+* R} {I₂ : R₁ →+* R} {I : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R}
+
 /-- The proposition that a sesquilinear form is alternating -/
 def is_alt (B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] R) : Prop := ∀ x, B x x = 0
 
@@ -199,6 +244,21 @@ lemma ortho_comm {x y} : is_ortho B x y ↔ is_ortho B y x := H.is_refl.ortho_co
 
 end is_alt
 
+lemma is_alt_iff_eq_neg_flip  [no_zero_divisors R] [char_zero R] {B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R} :
+  B.is_alt ↔ B = -B.flip :=
+begin
+  split; intro h,
+  { ext,
+    simp_rw [neg_apply, flip_apply],
+    exact (h.neg _ _).symm },
+  intros x,
+  let h' := congr_fun₂ h x x,
+  simp only [neg_apply, flip_apply, ←add_eq_zero_iff_eq_neg] at h',
+  exact add_self_eq_zero.mp h',
+end
+
+end alternating
+
 end linear_map
 
 namespace submodule