feat(linear_algebra/matrix): Add matrix properties for sesquilinear f…

…orms (#15906)

The main goal of this PR is to move `linear_algebra/matrix/bilinear_form` to the curried bilinear map form. Since this file as quite few dependencies we copy it to a new file `linear_algebra/matrix/sesquilinear_form` and then move all the dependencies.

The structure is taken literally from `linear_algebra/matrix/bilinear_form` with generalizations and easier proofs where possible. The new lemmas are named exactly as the old ones with the following changes:
- the namespace changed from `bilin_form` to `linear_map`
- `bilin` is changed to `linear_map₂`. In case there is the necessity for separate bilinear and semi-bilinear lemmas we use `linear_map₂` and `linear_mapₛₗ₂`
- If `bilin` is not in the name of a lemma, `matrix` is changed to `matrix₂` to avoid nameclashes with lemmas for linear maps `M →ₛₗ[ρ₁₂] N`

Moreover, the following changes were necessary:

`linear_algebra/bilinear_map`:
- Weakened some typeclass assumptions
- Added bilinear version of `sum_repr_mul_repr_mul` and moved sesquilinear version to `sum_repr_mul_repr_mulₛₗ`

`linear_algebra/matrix/bilinear_form`:
- Moved `basis.equiv_fun_symm_std_basis` to `linear_algebra/std_basis`
- `adjoint_pair` section: Removed a few definitions (they are now in `linear_algebra/matrix/sesquilinear_form`) and added a prime to the names of lemmas that have the same name as the version in `linear_algebra/matrix/sesquilinear_form`

`linear_algebra/sesquilinear_form`:
- Added a few missing lemmas about left-separating bilinear forms (note that `separating_left` was previously known as `nondegenerate`)

`linear_algebra/std_basis`:
- Lemma `std_basis_apply'` for calculating the application of `i' : ι` to `(std_basis R (λ (_x : ι), R) i)`

`algebra/hom/ring/`:
- Lemmas for calculating a ring homomorphism applied to `ite 0 1` and `ite 1 0`

The last two additions are needed to get a reasonable proof for `matrix.to_linear_map₂'_aux_std_basis`.



Co-authored-by: Moritz Doll <doll@uni-bremen.de>

src/algebra/hom/ring.lean

@@ -391,6 +391,14 @@ protected lemma map_bit0 (f : α →+* β) : ∀ a, f (bit0 a) = bit0 (f a) := m
 /-- Ring homomorphisms preserve `bit1`. -/
 protected lemma map_bit1 (f : α →+* β) : ∀ a, f (bit1 a) = bit1 (f a) := map_bit1 f
 
+@[simp] lemma map_ite_zero_one {F : Type*} [ring_hom_class F α β] (f : F) (p : Prop) [decidable p] :
+  f (ite p 0 1) = ite p 0 1 :=
+by { split_ifs; simp [h] }
+
+@[simp] lemma map_ite_one_zero {F : Type*} [ring_hom_class F α β] (f : F) (p : Prop) [decidable p] :
+  f (ite p 1 0) = ite p 1 0 :=
+by { split_ifs; simp [h] }
+
 /-- `f : α →+* β` has a trivial codomain iff `f 1 = 0`. -/
 lemma codomain_trivial_iff_map_one_eq_zero : (0 : β) = 1 ↔ f 1 = 0 := by rw [map_one, eq_comm]
 

src/algebra/lie/skew_adjoint.lean

@@ -119,7 +119,7 @@ begin
     A ∈ skew_adjoint_matrices_submodule (Pᵀ ⬝ J ⬝ P),
   { simp only [lie_subalgebra.mem_coe, submodule.mem_map_equiv, lie_subalgebra.mem_map_submodule,
       coe_coe], exact this, },
-  simp [matrix.is_skew_adjoint, J.is_adjoint_pair_equiv _ _ P (is_unit_of_invertible P)],
+  simp [matrix.is_skew_adjoint, J.is_adjoint_pair_equiv' _ _ P (is_unit_of_invertible P)],
 end
 
 lemma skew_adjoint_matrices_lie_subalgebra_equiv_apply

src/linear_algebra/bilinear_map.lean

@@ -256,6 +256,9 @@ include σ₄₃
   f.compl₂ g m q = f m (g q) := rfl
 omit σ₄₃
 
+@[simp] theorem compl₂_id : f.compl₂ linear_map.id = f :=
+by { ext, rw [compl₂_apply, id_coe, id.def] }
+
 /-- Composing linear maps `Q → M` and `Q' → N` with a bilinear map `M → N → P` to
 form a bilinear map `Q → Q' → P`. -/
 def compl₁₂ (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ) :
@@ -265,6 +268,10 @@ def compl₁₂ (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] M
 @[simp] theorem compl₁₂_apply (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Qₗ →ₗ[R] Mₗ) (g' : Qₗ' →ₗ[R] Nₗ)
   (x : Qₗ) (y : Qₗ') : f.compl₁₂ g g' x y = f (g x) (g' y) := rfl
 
+@[simp] theorem compl₁₂_id_id (f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ) :
+  f.compl₁₂ (linear_map.id) (linear_map.id) = f :=
+by { ext, simp_rw [compl₁₂_apply, id_coe, id.def] }
+
 lemma compl₁₂_inj {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ}
   (hₗ : function.surjective g) (hᵣ : function.surjective g') :
   f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂ :=
@@ -301,29 +308,29 @@ end comm_semiring
 section comm_ring
 
 variables {R R₂ S S₂ M N P : Type*}
+variables {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]
+
+section add_comm_monoid
+
+variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
+variables [add_comm_monoid Mₗ] [add_comm_monoid Nₗ] [add_comm_monoid Pₗ]
 variables [module R M] [module S N] [module R₂ P] [module S₂ P]
+variables [module R Mₗ] [module R Nₗ] [module R 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) :=
-smul_right_injective _ hx
-
-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)
+variables (b₁ : basis ι₁ R M) (b₂ : basis ι₂ S N) (b₁' : basis ι₁ R Mₗ) (b₂' : basis ι₂ R Nₗ)
 
 
 /-- 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) :
+/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.
+
+Version for semi-bilinear maps, see `sum_repr_mul_repr_mul` for the bilinear version. -/
+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
@@ -332,6 +339,34 @@ begin
     linear_map.map_smulₛₗ₂, linear_map.map_smulₛₗ],
 end
 
+/-- Write out `B x y` as a sum over `B (b i) (b j)` if `b` is a basis.
+
+Version for bilinear maps, see `sum_repr_mul_repr_mulₛₗ` for the semi-bilinear version. -/
+lemma sum_repr_mul_repr_mul {B : Mₗ →ₗ[R] Nₗ →ₗ[R] 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,
+    linear_map.map_smul₂, linear_map.map_smul],
+end
+
+end add_comm_monoid
+
+section add_comm_group
+
+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]
+
+lemma lsmul_injective [no_zero_smul_divisors R M] {x : R} (hx : x ≠ 0) :
+  function.injective (lsmul R M x) :=
+smul_right_injective _ hx
+
+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)
+
+end add_comm_group
 
 end comm_ring
 

src/linear_algebra/finsupp_vector_space.lean

@@ -210,3 +210,39 @@ begin
 end
 
 end module
+
+namespace basis
+
+variables {R M n : Type*}
+variables [decidable_eq n] [fintype n]
+variables [semiring R] [add_comm_monoid M] [module R M]
+
+lemma _root_.finset.sum_single_ite (a : R) (i : n) :
+  finset.univ.sum (λ (x : n), finsupp.single x (ite (i = x) a 0)) = finsupp.single i a :=
+begin
+  rw finset.sum_congr_set {i} (λ (x : n), finsupp.single x (ite (i = x) a 0))
+    (λ _, finsupp.single i a),
+  { simp },
+  { intros x hx,
+    rw set.mem_singleton_iff at hx,
+    simp [hx] },
+  intros x hx,
+  have hx' : ¬i = x :=
+  begin
+    refine ne_comm.mp _,
+    rwa mem_singleton_iff at hx,
+  end,
+  simp [hx'],
+end
+
+@[simp] lemma equiv_fun_symm_std_basis (b : basis n R M) (i : n) :
+  b.equiv_fun.symm (linear_map.std_basis R (λ _, R) i 1) = b i :=
+begin
+  have := equiv_like.injective b.repr,
+  apply_fun b.repr,
+  simp only [equiv_fun_symm_apply, std_basis_apply', linear_equiv.map_sum,
+    linear_equiv.map_smulₛₗ, ring_hom.id_apply, repr_self, finsupp.smul_single', boole_mul],
+  exact finset.sum_single_ite 1 i,
+end
+
+end basis

src/linear_algebra/matrix/bilinear_form.lean

@@ -9,6 +9,7 @@ import linear_algebra.matrix.nondegenerate
 import linear_algebra.matrix.nonsingular_inverse
 import linear_algebra.matrix.to_linear_equiv
 import linear_algebra.bilinear_form
+import linear_algebra.matrix.sesquilinear_form
 
 /-!
 # Bilinear form
@@ -245,18 +246,6 @@ noncomputable def bilin_form.to_matrix : bilin_form R₂ M₂ ≃ₗ[R₂] matri
 noncomputable def matrix.to_bilin : matrix n n R₂ ≃ₗ[R₂] bilin_form R₂ M₂ :=
 (bilin_form.to_matrix b).symm
 
-@[simp] lemma basis.equiv_fun_symm_std_basis (i : n) :
-  b.equiv_fun.symm (std_basis R₂ (λ _, R₂) i 1) = b i :=
-begin
-  rw [b.equiv_fun_symm_apply, finset.sum_eq_single i],
-  { rw [std_basis_same, one_smul] },
-  { rintros j - hj,
-    rw [std_basis_ne _ _ _ _ hj, zero_smul] },
-  { intro,
-    have := mem_univ i,
-    contradiction }
-end
-
 @[simp] lemma bilin_form.to_matrix_apply (B : bilin_form R₂ M₂) (i j : n) :
   bilin_form.to_matrix b B i j = B (b i) (b j) :=
 by rw [bilin_form.to_matrix, linear_equiv.trans_apply, bilin_form.to_matrix'_apply, congr_apply,
@@ -373,18 +362,6 @@ variables {n : Type*} [fintype n]
 variables (b : basis n R₃ M₃)
 variables (J J₃ A A' : matrix n n R₃)
 
-/-- The condition for the square matrices `A`, `A'` to be an adjoint pair with respect to the square
-matrices `J`, `J₃`. -/
-def matrix.is_adjoint_pair := Aᵀ ⬝ J₃ = J ⬝ A'
-
-/-- The condition for a square matrix `A` to be self-adjoint with respect to the square matrix
-`J`. -/
-def matrix.is_self_adjoint := matrix.is_adjoint_pair J J A A
-
-/-- The condition for a square matrix `A` to be skew-adjoint with respect to the square matrix
-`J`. -/
-def matrix.is_skew_adjoint := matrix.is_adjoint_pair J J A (-A)
-
 @[simp] lemma is_adjoint_pair_to_bilin' [decidable_eq n] :
   bilin_form.is_adjoint_pair (matrix.to_bilin' J) (matrix.to_bilin' J₃)
       (matrix.to_lin' A) (matrix.to_lin' A') ↔
@@ -421,7 +398,7 @@ begin
   refl,
 end
 
-lemma matrix.is_adjoint_pair_equiv [decidable_eq n] (P : matrix n n R₃) (h : is_unit P) :
+lemma matrix.is_adjoint_pair_equiv' [decidable_eq n] (P : matrix n n R₃) (h : is_unit P) :
   (Pᵀ ⬝ J ⬝ P).is_adjoint_pair (Pᵀ ⬝ J ⬝ P) A A' ↔
     J.is_adjoint_pair J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹) :=
 have h' : is_unit P.det := P.is_unit_iff_is_unit_det.mp h,
@@ -444,45 +421,32 @@ variables [decidable_eq n]
 
 /-- The submodule of pair-self-adjoint matrices with respect to bilinear forms corresponding to
 given matrices `J`, `J₂`. -/
-def pair_self_adjoint_matrices_submodule : submodule R₃ (matrix n n R₃) :=
+def pair_self_adjoint_matrices_submodule' : submodule R₃ (matrix n n R₃) :=
 (bilin_form.is_pair_self_adjoint_submodule (matrix.to_bilin' J) (matrix.to_bilin' J₃)).map
   ((linear_map.to_matrix' : ((n → R₃) →ₗ[R₃] (n → R₃)) ≃ₗ[R₃] matrix n n R₃) :
   ((n → R₃) →ₗ[R₃] (n → R₃)) →ₗ[R₃] matrix n n R₃)
 
-@[simp] lemma mem_pair_self_adjoint_matrices_submodule :
+lemma mem_pair_self_adjoint_matrices_submodule' :
   A ∈ (pair_self_adjoint_matrices_submodule J J₃) ↔ matrix.is_adjoint_pair J J₃ A A :=
-begin
-  simp only [pair_self_adjoint_matrices_submodule, linear_equiv.coe_coe,
-    linear_map.to_matrix'_apply, submodule.mem_map, bilin_form.mem_is_pair_self_adjoint_submodule],
-  split,
-  { rintros ⟨f, hf, hA⟩,
-    have hf' : f = A.to_lin' := by rw [←hA, matrix.to_lin'_to_matrix'], rw hf' at hf,
-    rw ← is_adjoint_pair_to_bilin',
-    exact hf, },
-  { intros h, refine ⟨A.to_lin', _, linear_map.to_matrix'_to_lin' _⟩,
-    exact (is_adjoint_pair_to_bilin' _ _ _ _).mpr h, },
-end
+by simp only [mem_pair_self_adjoint_matrices_submodule]
 
 /-- The submodule of self-adjoint matrices with respect to the bilinear form corresponding to
 the matrix `J`. -/
-def self_adjoint_matrices_submodule : submodule R₃ (matrix n n R₃) :=
+def self_adjoint_matrices_submodule' : submodule R₃ (matrix n n R₃) :=
   pair_self_adjoint_matrices_submodule J J
 
-@[simp] lemma mem_self_adjoint_matrices_submodule :
+lemma mem_self_adjoint_matrices_submodule' :
   A ∈ self_adjoint_matrices_submodule J ↔ J.is_self_adjoint A :=
-by { erw mem_pair_self_adjoint_matrices_submodule, refl, }
+by simp only [mem_self_adjoint_matrices_submodule]
 
 /-- The submodule of skew-adjoint matrices with respect to the bilinear form corresponding to
 the matrix `J`. -/
-def skew_adjoint_matrices_submodule : submodule R₃ (matrix n n R₃) :=
+def skew_adjoint_matrices_submodule' : submodule R₃ (matrix n n R₃) :=
   pair_self_adjoint_matrices_submodule (-J) J
 
-@[simp] lemma mem_skew_adjoint_matrices_submodule :
+lemma mem_skew_adjoint_matrices_submodule' :
   A ∈ skew_adjoint_matrices_submodule J ↔ J.is_skew_adjoint A :=
-begin
-  erw mem_pair_self_adjoint_matrices_submodule,
-  simp [matrix.is_skew_adjoint, matrix.is_adjoint_pair],
-end
+by simp only [mem_skew_adjoint_matrices_submodule]
 
 end matrix_adjoints