English
There exists a linear isomorphism M ⊗_R (N / n) ≅_R (M ⊗_R N) / (M ⊗_R n) for any R-submodule n of N.
Русский
Существует линейное изоморфизмом между M ⊗ (N / n) и (M ⊗ N) / (M ⊗ n) при любой подмодульной n ⊆ N.
LaTeX
$$$$ M \otimes_R (N / n) \cong_R (M \otimes_R N) / (M \otimes_R n). $$$$
Lean4
/-- Let `M, N` be `R`-modules, `n ≤ N` be an `R`-submodule. Then we have a linear isomorphism between
tensor products of the quotient and the quotient of the tensor product:
`M ⊗[R] (N ⧸ n) ≃ₗ[R] (M ⊗[R] N) ⧸ (M ⊗ n)`.
-/
noncomputable def tensorQuotientEquiv (n : Submodule R N) :
M ⊗[R] (N ⧸ (n : Submodule R N)) ≃ₗ[R] (M ⊗[R] N) ⧸ (LinearMap.range (map (LinearMap.id : M →ₗ[R] M) n.subtype)) :=
congr ((Submodule.quotEquivOfEqBot _ rfl).symm) (LinearEquiv.refl _ _) ≪≫ₗ
quotientTensorQuotientEquiv (⊥ : Submodule R M) n ≪≫ₗ
Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _)
(by
simp only [Submodule.map_sup]
erw [Submodule.map_id, Submodule.map_id]
simp only [sup_eq_right]
rw [range_map_eq_span_tmul, range_map_eq_span_tmul]
simp)
