feat: characterise the kernel of the map M ⊗[R] N →ₗ[A] M ⊗[A] N (leanprover-community#36752)

Let $A$ be an $R$-algebra and $M$ and $N$ be $A$-modules.

In this PR we prove that the kernel of the natural map $M ⊗_R N → M ⊗_A N$ is spanned by elements of the form $(am) ⊗_R n - m ⊗_R (an)$.

Co-authored-by: leo <leonid.ryvkin@rub.de>

Author: Ljon4ik4

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -328,6 +328,8 @@ def mapOfCompatibleSMul : M ⊗[A] N →ₗ[S] M ⊗[R] N where
 @[simp] theorem mapOfCompatibleSMul_tmul (m n) : mapOfCompatibleSMul R A S M N (m ⊗ₜ n) = m ⊗ₜ n :=
   rfl
 
+/- The map `mapOfCompatibleSMul` is surjective. Its kernel is characterized by the Lemma
+`TensorProduct.ker_mapOfCompatibleSMul`. -/
 theorem mapOfCompatibleSMul_surjective : Function.Surjective (mapOfCompatibleSMul R A S M N) :=
   fun x ↦ x.induction_on (⟨0, map_zero _⟩) (fun m n ↦ ⟨_, mapOfCompatibleSMul_tmul ..⟩)
     fun _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x + y, by simpa using congr($hx + $hy)⟩

Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

@@ -14,7 +14,8 @@ public import Mathlib.RingTheory.Ideal.Quotient.Defs
 
 # Interaction between Quotients and Tensor Products
 
-This file contains constructions that relate quotients and tensor products.
+This file contains constructions that relate quotients and tensor products. This file is also a home
+for results whose proof depends on both tensor products and linear algebraic quotients.
 Let `M, N` be `R`-modules, `m ≤ M` and `n ≤ N` be an `R`-submodules and `I ≤ R` an ideal. We prove
 the following isomorphisms:
 
@@ -297,4 +298,32 @@ lemma tensorQuotientEquiv_symm_apply_mk_tmul (n : Submodule B N) (x : M) (y : N)
       x ⊗ₜ[R] Submodule.Quotient.mk y :=
   rfl
 
+
+variable [Module A N] [IsScalarTower R A N]
+
+/- This lemma characterizes the kernel of `TensorProduct.mapOfCompatibleSMul`. Together with
+`TensorProduct.mapOfCompatibleSMul_surjective` it gives an alternative characterization of
+`M ⊗[A] N` as the quotient of `M ⊗[R] N` by the submodule `S` described below. -/
+lemma ker_mapOfCompatibleSMul :
+    (mapOfCompatibleSMul A R A M N).ker =
+      Submodule.span A {(a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) | (a : A) (m : M) (n : N)} := by
+  refine (Submodule.span_eq_of_le (mapOfCompatibleSMul A R A M N).ker ?_ ?_).symm
+  · rintro - ⟨a, m, n, rfl⟩
+    simp [smul_tmul]
+  · let S := Submodule.span A {(a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) | (a : A) (m : M) (n : N)}
+    let F : M ⊗[A] N →ₗ[A] (M ⊗[R] N) ⧸ S := TensorProduct.lift ({
+      toFun m := {
+        toFun n := S.mkQ (m ⊗ₜ[R] n)
+        map_add' _ _ := by simp [tmul_add]
+        map_smul' a n := by
+          rw [Submodule.mkQ_apply, Submodule.mkQ_apply, ← Submodule.Quotient.mk_smul, eq_comm,
+            Submodule.Quotient.eq, RingHom.id_apply]
+          exact Submodule.subset_span ⟨a, m, n, rfl⟩ }
+      map_add' _ _ := by ext _; simp [add_tmul]
+      map_smul' _ _ := by simp; rfl })
+    have h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ := by ext; simp [S, F]
+    change (mapOfCompatibleSMul A R A M N).ker ≤ S
+    rw [← Submodule.ker_mkQ S, ← h]
+    exact (mapOfCompatibleSMul A R A M N).ker_le_ker_comp F
+
 end TensorProduct.AlgebraTensorModule