fix: generalize CommSemiring to Semiring for bilinear map composition

eric-wieser · eric-wieser · commit 09fe2f6305e4 · 2025-06-26T22:09:34.000Z
This file could do with further variable cleanup, but that's left for a later PR.
diff --git a/Mathlib/LinearAlgebra/BilinearMap.lean b/Mathlib/LinearAlgebra/BilinearMap.lean
@@ -220,21 +220,65 @@ theorem lflip_apply {R₀ : Type*} [Semiring R₀] [Module R₀ P] [SMulCommClas
 
 end Semiring
 
+section Semiring'
+
+variable {R : Type*} [Semiring R] {R₂ : Type*} [Semiring R₂]
+variable {A : Type*} [Semiring A] {B : Type*} [Semiring B]
+variable {R₃ : Type*} [Semiring R₃] {R₄ : Type*} [Semiring R₄]
+variable {M : Type*} {N : Type*} {P : Type*} {Q : Type*}
+variable [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q]
+variable [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q]
+variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
+variable {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
+variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃]
+variable {R₅ : Type*} [Semiring R₅] [Module R₅ P] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅}
+
+variable (P σ₂₃ R₅)
+
+/-- Composing a semilinear map `M → N` and a semilinear map `N → P` to form a semilinear map
+`M → P` is itself a linear map. -/
+def lcompₛₗ (f : M →ₛₗ[σ₁₂] N) : (N →ₛₗ[σ₂₃] P) →ₗ[R₅] M →ₛₗ[σ₁₃] P :=
+  letI := SMulCommClass.symm
+  flip <| LinearMap.comp (flip id) f
+
+variable {P σ₂₃ R₅}
+
+@[simp]
+theorem lcompₛₗ_apply (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) :
+    lcompₛₗ P σ₂₃ R₅ f g x = g (f x) := rfl
+
+/-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
+form a bilinear map `M → Q → P`. -/
+def compl₂ (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P where
+  toFun a := (lcompₛₗ P σ₂₃ R₅ g) (h a)
+  map_add' _ _ := by
+    simp [map_add]
+  map_smul' _ _ := by
+    simp only [LinearMap.map_smulₛₗ, lcompₛₗ]
+    rfl
+
+@[simp]
+theorem compl₂_apply (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) :
+  h.compl₂ g m q = h m (g q) := rfl
+
+@[simp]
+theorem compl₂_id (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) : h.compl₂ LinearMap.id = h := by
+  ext
+  rw [compl₂_apply, id_coe, _root_.id]
+
+end Semiring'
+
 section CommSemiring
 
-variable {R : Type*} [CommSemiring R] {R₂ : Type*} [CommSemiring R₂]
+variable {R : Type*} [CommSemiring R] {R₂ : Type*} [Semiring R₂]
 variable {A : Type*} [Semiring A] {B : Type*} [Semiring B]
-variable {R₃ : Type*} [CommSemiring R₃] {R₄ : Type*} [CommSemiring R₄]
 variable {M : Type*} {N : Type*} {P : Type*} {Q : Type*}
 variable {Mₗ : Type*} {Nₗ : Type*} {Pₗ : Type*} {Qₗ Qₗ' : Type*}
 variable [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q]
 variable [AddCommMonoid Mₗ] [AddCommMonoid Nₗ] [AddCommMonoid Pₗ]
 variable [AddCommMonoid Qₗ] [AddCommMonoid Qₗ']
-variable [Module R M] [Module R₂ N] [Module R₃ P] [Module R₄ Q]
+variable [Module R M]
 variable [Module R Mₗ] [Module R Nₗ] [Module R Pₗ] [Module R Qₗ] [Module R Qₗ']
-variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
-variable {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
-variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₄₂ σ₂₃ σ₄₃]
 variable (R)
 
 /-- Create a bilinear map from a function that is linear in each component.
@@ -252,16 +296,13 @@ theorem mk₂_apply (f : M → Nₗ → Pₗ) {H1 H2 H3 H4} (m : M) (n : Nₗ) :
 
 variable {R}
 
-variable (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
 
 variable (A Pₗ)
 variable [Module A Pₗ] [SMulCommClass R A Pₗ]
 
 /-- Composing a given linear map `M → N` with a linear map `N → P` as a linear map from
 `Nₗ →ₗ[R] Pₗ` to `M →ₗ[R] Pₗ`. -/
-def lcomp (f : M →ₗ[R] Nₗ) : (Nₗ →ₗ[R] Pₗ) →ₗ[A] M →ₗ[R] Pₗ :=
-  letI := SMulCommClass.symm
-  flip <| LinearMap.comp (flip id) f
+def lcomp (f : M →ₗ[R] Nₗ) : (Nₗ →ₗ[R] Pₗ) →ₗ[A] M →ₗ[R] Pₗ := lcompₛₗ Pₗ _ _ f
 
 variable {A Pₗ}
 
@@ -270,19 +311,6 @@ theorem lcomp_apply (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) (x : M) : l
 
 theorem lcomp_apply' (f : M →ₗ[R] Nₗ) (g : Nₗ →ₗ[R] Pₗ) : lcomp A Pₗ f g = g ∘ₗ f := rfl
 
-variable (P σ₂₃)
-
-/-- Composing a semilinear map `M → N` and a semilinear map `N → P` to form a semilinear map
-`M → P` is itself a linear map. -/
-def lcompₛₗ (f : M →ₛₗ[σ₁₂] N) : (N →ₛₗ[σ₂₃] P) →ₗ[R₃] M →ₛₗ[σ₁₃] P :=
-  flip <| LinearMap.comp (flip id) f
-
-variable {P σ₂₃}
-
-@[simp]
-theorem lcompₛₗ_apply (f : M →ₛₗ[σ₁₂] N) (g : N →ₛₗ[σ₂₃] P) (x : M) :
-    lcompₛₗ P σ₂₃ f g x = g (f x) := rfl
-
 variable (R M Nₗ Pₗ)
 
 /-- Composing linear maps as a bilinear map from `(M →ₗ[R] N) × (N →ₗ[R] P)` to `M →ₗ[R] P` -/
@@ -304,28 +332,9 @@ theorem llcomp_apply' (f : Nₗ →ₗ[R] Pₗ) (g : M →ₗ[R] Nₗ) : llcomp
 
 end
 
-/-- Composing a linear map `Q → N` and a bilinear map `M → N → P` to
-form a bilinear map `M → Q → P`. -/
-def compl₂ {R₅ : Type*} [CommSemiring R₅] [Module R₅ P] [SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅}
-    (h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P) (g : Q →ₛₗ[σ₄₂] N) : M →ₛₗ[σ₁₅] Q →ₛₗ[σ₄₃] P where
-  toFun a := (lcompₛₗ P σ₂₃ g) (h a)
-  map_add' _ _ := by
-    simp [map_add]
-  map_smul' _ _ := by
-    simp only [LinearMap.map_smulₛₗ, lcompₛₗ]
-    rfl
-
-@[simp]
-theorem compl₂_apply (g : Q →ₛₗ[σ₄₂] N) (m : M) (q : Q) : f.compl₂ g m q = f m (g q) := rfl
-
-@[simp]
-theorem compl₂_id : f.compl₂ LinearMap.id = f := by
-  ext
-  rw [compl₂_apply, id_coe, _root_.id]
-
 /-- 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₁₂ {R₁ : Type*} [CommSemiring R₁] [Module R₂ N] [Module R₂ Pₗ] [Module R₁ Pₗ]
+def compl₁₂ {R₁ : Type*} [Semiring R₁] [Module R₂ N] [Module R₂ Pₗ] [Module R₁ Pₗ]
     [Module R₁ Mₗ] [SMulCommClass R₂ R₁ Pₗ] [Module R₁ Qₗ] [Module R₂ Qₗ']
     (f : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ) (g : Qₗ →ₗ[R₁] Mₗ) (g' : Qₗ' →ₗ[R₂] N) :
     Qₗ →ₗ[R₁] Qₗ' →ₗ[R₂] Pₗ :=
@@ -444,7 +453,7 @@ open Function
 section restrictScalarsRange
 
 variable {R S M P M' P' : Type*}
-  [CommSemiring R] [CommSemiring S] [SMul S R]
+  [Semiring R] [Semiring S] [SMul S R]
   [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P]
   [Module S M] [Module S P]
   [IsScalarTower S R M] [IsScalarTower S R P]
