chore(linear_algebra): generalize conversion between matrices and bilinear forms to semirings (#14263)

Only one lemma was moved (`dual_distrib_apply`), none were renamed, and no proofs were meaningfully changed.

Section markers were shuffled around, and some variables exchanged for variables with weaker typeclass assumptions.

A few other things have been generalized to semiring at the same time; `linear_map.trace` and `linear_map.smul_rightₗ`

Author: eric-wieser

src/linear_algebra/basic.lean

@@ -418,12 +418,6 @@ def dom_restrict'
 @[simp] lemma dom_restrict'_apply (f : M →ₗ[R] M₂) (p : submodule R M) (x : p) :
   dom_restrict' p f x = f x := rfl
 
-end comm_semiring
-
-section comm_ring
-variables [comm_ring R] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃]
-variables [module R M] [module R M₂] [module R M₃]
-
 /--
 The family of linear maps `M₂ → M` parameterised by `f ∈ M₂ → R`, `x ∈ M`, is linear in `f`, `x`.
 -/
@@ -438,7 +432,7 @@ def smul_rightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M :=
 @[simp] lemma smul_rightₗ_apply (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
   (smul_rightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M) f x c = (f c) • x := rfl
 
-end comm_ring
+end comm_semiring
 
 end linear_map
 

src/linear_algebra/bilinear_form.lean

@@ -616,20 +616,20 @@ end
 
 section basis
 
-variables {B₃ F₃ : bilin_form R₃ M₃}
-variables {ι : Type*} (b : basis ι R₃ M₃)
+variables {F₂ : bilin_form R₂ M₂}
+variables {ι : Type*} (b : basis ι R₂ M₂)
 
 /-- Two bilinear forms are equal when they are equal on all basis vectors. -/
-lemma ext_basis (h : ∀ i j, B₃ (b i) (b j) = F₃ (b i) (b j)) : B₃ = F₃ :=
+lemma ext_basis (h : ∀ i j, B₂ (b i) (b j) = F₂ (b i) (b j)) : B₂ = F₂ :=
 to_lin.injective $ 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 (x y : M₃) :
-  (b.repr x).sum (λ i xi, (b.repr y).sum (λ j yj, xi • yj • B₃ (b i) (b j))) = B₃ x y :=
+lemma sum_repr_mul_repr_mul (x y : M₂) :
+  (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, sum_left, sum_right,
-    smul_left, smul_right, smul_eq_mul]
+    smul_left, smul_right, smul_eq_mul],
 end
 
 end basis
@@ -781,18 +781,15 @@ def is_pair_self_adjoint_submodule : submodule R₂ (module.End R₂ M₂) :=
   f ∈ is_pair_self_adjoint_submodule B₂ F₂ ↔ is_pair_self_adjoint B₂ F₂ f :=
 by refl
 
-variables {M₃' : Type*} [add_comm_group M₃'] [module R₃ M₃']
-variables (B₃ F₃ : bilin_form R₃ M₃)
-
-lemma is_pair_self_adjoint_equiv (e : M₃' ≃ₗ[R₃] M₃) (f : module.End R₃ M₃) :
-  is_pair_self_adjoint B₃ F₃ f ↔
-    is_pair_self_adjoint (B₃.comp ↑e ↑e) (F₃.comp ↑e ↑e) (e.symm.conj f) :=
+lemma is_pair_self_adjoint_equiv (e : M₂' ≃ₗ[R₂] M₂) (f : module.End R₂ M₂) :
+  is_pair_self_adjoint B₂ F₂ f ↔
+    is_pair_self_adjoint (B₂.comp ↑e ↑e) (F₂.comp ↑e ↑e) (e.symm.conj f) :=
 begin
-  have hₗ : (F₃.comp ↑e ↑e).comp_left (e.symm.conj f) = (F₃.comp_left f).comp ↑e ↑e :=
+  have hₗ : (F₂.comp ↑e ↑e).comp_left (e.symm.conj f) = (F₂.comp_left f).comp ↑e ↑e :=
     by { ext, simp [linear_equiv.symm_conj_apply], },
-  have hᵣ : (B₃.comp ↑e ↑e).comp_right (e.symm.conj f) = (B₃.comp_right f).comp ↑e ↑e :=
+  have hᵣ : (B₂.comp ↑e ↑e).comp_right (e.symm.conj f) = (B₂.comp_right f).comp ↑e ↑e :=
     by { ext, simp [linear_equiv.conj_apply], },
-  have he : function.surjective (⇑(↑e : M₃' →ₗ[R₃] M₃) : M₃' → M₃) := e.surjective,
+  have he : function.surjective (⇑(↑e : M₂' →ₗ[R₂] M₂) : M₂' → M₂) := e.surjective,
   show bilin_form.is_adjoint_pair _ _ _ _  ↔ bilin_form.is_adjoint_pair _ _ _ _,
   rw [is_adjoint_pair_iff_comp_left_eq_comp_right, is_adjoint_pair_iff_comp_left_eq_comp_right,
       hᵣ, hₗ, comp_inj _ _ he he],
@@ -818,6 +815,8 @@ def self_adjoint_submodule := is_pair_self_adjoint_submodule B₂ B₂
 @[simp] lemma mem_self_adjoint_submodule (f : module.End R₂ M₂) :
   f ∈ B₂.self_adjoint_submodule ↔ B₂.is_self_adjoint f := iff.rfl
 
+variables (B₃ : bilin_form R₃ M₃)
+
 /-- The set of skew-adjoint endomorphisms of a module with bilinear form is a submodule. (In fact
 it is a Lie subalgebra.) -/
 def skew_adjoint_submodule := is_pair_self_adjoint_submodule (-B₃) B₃

src/linear_algebra/contraction.lean

@@ -20,8 +20,7 @@ some basic properties of these maps.
 contraction, dual module, tensor product
 -/
 
-variables (R M N P Q : Type*) [add_comm_group M]
-variables [add_comm_group N] [add_comm_group P] [add_comm_group Q]
+variables {ι : Type*} (R M N P Q : Type*)
 
 local attribute [ext] tensor_product.ext
 
@@ -30,10 +29,11 @@ section contraction
 open tensor_product linear_map matrix
 open_locale tensor_product big_operators
 
-section comm_ring
-
-variables [comm_ring R] [module R M] [module R N] [module R P] [module R Q]
-variables {ι : Type*} [decidable_eq ι] [fintype ι] (b : basis ι R M)
+section comm_semiring
+variables [comm_semiring R]
+variables [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q]
+variables [module R M] [module R N] [module R P] [module R Q]
+variables [decidable_eq ι] [fintype ι] (b : basis ι R M)
 
 /-- The natural left-handed pairing between a module and its dual. -/
 def contract_left : (module.dual R M) ⊗ M →ₗ[R] R := (uncurry _ _ _ _).to_fun linear_map.id
@@ -100,6 +100,16 @@ begin
   rw [and_iff_not_or_not, not_not] at hij, cases hij; simp [hij],
 end
 
+end comm_semiring
+
+section comm_ring
+variables [comm_ring R]
+variables [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group Q]
+variables [module R M] [module R N] [module R P] [module R Q]
+variables [decidable_eq ι] [fintype ι] (b : basis ι R M)
+
+variables {R M N P Q}
+
 /-- If `M` is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function
 provides this equivalence in return for a basis of `M`. -/
 @[simps apply]
@@ -157,7 +167,9 @@ open module tensor_product linear_map
 
 section comm_ring
 
-variables [comm_ring R] [module R M] [module R N] [module R P] [module R Q]
+variables [comm_ring R]
+variables [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group Q]
+variables [module R M] [module R N] [module R P] [module R Q]
 variables [free R M] [finite R M] [free R N] [finite R N] [nontrivial R]
 
 /-- When `M` is a finite free module, the map `ltensor_hom_to_hom_ltensor` is an equivalence. Note

src/linear_algebra/dual.lean

@@ -351,7 +351,7 @@ section dual_pair
 open module
 
 variables {R M ι : Type*}
-variables [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι]
+variables [comm_semiring R] [add_comm_monoid M] [module R M] [decidable_eq ι]
 
 /-- `e` and `ε` have characteristic properties of a basis and its dual -/
 @[nolint has_inhabited_instance]
@@ -448,7 +448,7 @@ namespace submodule
 
 universes u v w
 
-variables {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M]
+variables {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M] [module R M]
 variable {W : submodule R M}
 
 /-- The `dual_restrict` of a submodule `W` of `M` is the linear map from the
@@ -464,7 +464,7 @@ linear_map.dom_restrict' W
 
 /-- The `dual_annihilator` of a submodule `W` is the set of linear maps `φ` such
   that `φ w = 0` for all `w ∈ W`. -/
-def dual_annihilator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M]
+def dual_annihilator {R : Type u} {M : Type v} [comm_semiring R] [add_comm_monoid M]
   [module R M] (W : submodule R M) : submodule R $ module.dual R M :=
 W.dual_restrict.ker
 
@@ -624,11 +624,12 @@ end
 
 end subspace
 
-variables {R : Type*} [comm_ring R] {M₁ : Type*} {M₂ : Type*}
-variables [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂]
-
 open module
 
+section dual_map
+variables {R : Type*} [comm_semiring R] {M₁ : Type*} {M₂ : Type*}
+variables [add_comm_monoid M₁] [module R M₁] [add_comm_monoid M₂] [module R M₂]
+
 /-- Given a linear map `f : M₁ →ₗ[R] M₂`, `f.dual_map` is the linear map between the dual of
 `M₂` and `M₁` such that it maps the functional `φ` to `φ ∘ f`. -/
 def linear_map.dual_map (f : M₁ →ₗ[R] M₂) : dual R M₂ →ₗ[R] dual R M₁ :=
@@ -680,7 +681,11 @@ lemma linear_equiv.dual_map_trans {M₃ : Type*} [add_comm_group M₃] [module R
   g.dual_map.trans f.dual_map = (f.trans g).dual_map :=
 rfl
 
+end dual_map
+
 namespace linear_map
+variables {R : Type*} [comm_semiring R] {M₁ : Type*} {M₂ : Type*}
+variables [add_comm_monoid M₁] [module R M₁] [add_comm_monoid M₂] [module R M₂]
 
 variable (f : M₁ →ₗ[R] M₂)
 
@@ -767,9 +772,7 @@ end linear_map
 
 namespace tensor_product
 
-variables (R) (M : Type*) (N : Type*)
-variables [add_comm_group M] [add_comm_group N]
-variables [module R M] [module R N]
+variables (R : Type*) (M : Type*) (N : Type*)
 
 variables {ι κ : Type*}
 variables [decidable_eq ι] [decidable_eq κ]
@@ -782,7 +785,10 @@ local attribute [ext] tensor_product.ext
 
 open tensor_product
 open linear_map
-open module (dual)
+
+section
+variables [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N]
+variables [module R M] [module R N]
 
 /--
 The canonical linear map from `dual M ⊗ dual N` to `dual (M ⊗ N)`,
@@ -794,6 +800,18 @@ def dual_distrib : (dual R M) ⊗[R] (dual R N) →ₗ[R] dual R (M ⊗[R] N) :=
 
 variables {R M N}
 
+@[simp]
+lemma dual_distrib_apply (f : dual R M) (g : dual R N) (m : M) (n : N) :
+  dual_distrib R M N (f ⊗ₜ g) (m ⊗ₜ n) = f m * g n :=
+by simp only [dual_distrib, coe_comp, function.comp_app, hom_tensor_hom_map_apply,
+  comp_right_apply, linear_equiv.coe_coe, map_tmul, lid_tmul, algebra.id.smul_eq_mul]
+
+end
+
+variables {R M N}
+variables [comm_ring R] [add_comm_group M] [add_comm_group N]
+variables [module R M] [module R N]
+
 /--
 An inverse to `dual_tensor_dual_map` given bases.
 -/
@@ -803,12 +821,6 @@ def dual_distrib_inv_of_basis (b : basis ι R M) (c : basis κ R N) :
 ∑ i j, (ring_lmap_equiv_self R ℕ _).symm (b.dual_basis i ⊗ₜ c.dual_basis j)
     ∘ₗ applyₗ (c j) ∘ₗ applyₗ (b i) ∘ₗ (lcurry R M N R)
 
-@[simp]
-lemma dual_distrib_apply (f : dual R M) (g : dual R N) (m : M) (n : N) :
-  dual_distrib R M N (f ⊗ₜ g) (m ⊗ₜ n) = f m * g n :=
-by simp only [dual_distrib, coe_comp, function.comp_app, hom_tensor_hom_map_apply,
-  comp_right_apply, linear_equiv.coe_coe, map_tmul, lid_tmul, algebra.id.smul_eq_mul]
-
 @[simp]
 lemma dual_distrib_inv_of_basis_apply (b : basis ι R M) (c : basis κ R N)
   (f : dual R (M ⊗[R] N)) : dual_distrib_inv_of_basis b c f =

src/linear_algebra/matrix/basis.lean

@@ -38,7 +38,8 @@ open_locale matrix
 section basis_to_matrix
 
 variables {ι ι' κ κ' : Type*}
-variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
+variables {R M : Type*} [comm_semiring R] [add_comm_monoid M] [module R M]
+variables {R₂ M₂ : Type*} [comm_ring R₂] [add_comm_group M₂] [module R₂ M₂]
 
 open function matrix
 
@@ -84,7 +85,7 @@ begin
 end
 
 /-- The basis constructed by `units_smul` has vectors given by a diagonal matrix. -/
-@[simp] lemma to_matrix_units_smul [decidable_eq ι] (w : ι → Rˣ) :
+@[simp] lemma to_matrix_units_smul [decidable_eq ι] (e : basis ι R₂ M₂) (w : ι → R₂ˣ) :
   e.to_matrix (e.units_smul w) = diagonal (coe ∘ w) :=
 begin
   ext i j,
@@ -94,7 +95,8 @@ begin
 end
 
 /-- The basis constructed by `is_unit_smul` has vectors given by a diagonal matrix. -/
-@[simp] lemma to_matrix_is_unit_smul [decidable_eq ι] {w : ι → R} (hw : ∀ i, is_unit (w i)) :
+@[simp] lemma to_matrix_is_unit_smul [decidable_eq ι] (e : basis ι R₂ M₂) {w : ι → R₂}
+  (hw : ∀ i, is_unit (w i)) :
   e.to_matrix (e.is_unit_smul hw) = diagonal w :=
 e.to_matrix_units_smul _
 
@@ -147,7 +149,7 @@ end basis
 
 section mul_linear_map_to_matrix
 
-variables {N : Type*} [add_comm_group N] [module R N]
+variables {N : Type*} [add_comm_monoid N] [module R N]
 variables (b : basis ι R M) (b' : basis ι' R M) (c : basis κ R N) (c' : basis κ' R N)
 variables (f : M →ₗ[R] N)