feat(LinearAlgebra/TensorProduct/RightExactness): generalize TensorProduct.(map|mk)_surjective to [Comm]Semiring (#20034)

Originally they were `[Comm]Ring`.

Author: acmepjz

Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

@@ -165,6 +165,25 @@ lemma LinearMap.rTensor_exact_iff_lTensor_exact :
     (e₂ := TensorProduct.comm _ _ _) (e₃ := TensorProduct.comm _ _ _)
     (by ext; simp) (by ext; simp)
 
+variable (hg : Function.Surjective g)
+    {N' P' : Type*} [AddCommMonoid N'] [AddCommMonoid P'] [Module R N'] [Module R P']
+    {g' : N' →ₗ[R] P'} (hg' : Function.Surjective g')
+
+include hg hg' in
+theorem TensorProduct.map_surjective : Function.Surjective (TensorProduct.map g g') := by
+  rw [← lTensor_comp_rTensor, coe_comp]
+  exact Function.Surjective.comp (lTensor_surjective _ hg') (rTensor_surjective _ hg)
+
+variable (M R) in
+theorem TensorProduct.mk_surjective (S) [Semiring S] [Algebra R S]
+    (h : Function.Surjective (algebraMap R S)) :
+    Function.Surjective (TensorProduct.mk R S M 1) := by
+  rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
+  rintro _ ⟨x, y, rfl⟩
+  obtain ⟨x, rfl⟩ := h x
+  rw [Algebra.algebraMap_eq_smul_one, smul_tmul]
+  exact ⟨x • y, rfl⟩
+
 end Semiring
 
 variable {R M N P : Type*} [CommRing R]
@@ -393,11 +412,6 @@ variable {M' N' P' : Type*}
     {f' : M' →ₗ[R] N'} {g' : N' →ₗ[R] P'}
     (hfg' : Exact f' g') (hg' : Function.Surjective g')
 
-include hg hg' in
-theorem TensorProduct.map_surjective : Function.Surjective (TensorProduct.map g g') := by
-  rw [← lTensor_comp_rTensor, coe_comp]
-  exact Function.Surjective.comp (lTensor_surjective _ hg') (rTensor_surjective _ hg)
-
 include hg hg' hfg hfg' in
 /-- Kernel of a product map (right-exactness of tensor product) -/
 theorem TensorProduct.map_ker :
@@ -414,18 +428,6 @@ theorem TensorProduct.map_ker :
   rw [range_eq_top.mpr (rTensor_surjective M' hg), Submodule.map_top]
   rw [Exact.linearMap_ker_eq (lTensor_exact P hfg' hg')]
 
-variable (M)
-
-variable (R) in
-theorem TensorProduct.mk_surjective (S) [Semiring S] [Algebra R S]
-    (h : Surjective (algebraMap R S)) :
-    Surjective (TensorProduct.mk R S M 1) := by
-  rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
-  rintro _ ⟨x, y, rfl⟩
-  obtain ⟨x, rfl⟩ := h x
-  rw [Algebra.algebraMap_eq_smul_one, smul_tmul]
-  exact ⟨x • y, rfl⟩
-
 end Modules
 
 section Algebras