English
Alternative presentation of the same injectivity: the canonical map M → B ⊗_A M is injective when B is faithfully flat over A.
Русский
Альтернативная формулировка той же инъекции: каноническое отображение M → B ⊗_A M инъективно, когда B плоско над A.
LaTeX
$$Injective(\text{M} \to B \otimes_A \text{M})$$
Lean4
/-- If `B` is a faithfully flat `A`-module and `M` is any `A`-module, the canonical
map `M →ₗ[A] B ⊗[A] M` is injective. -/
theorem tensorProduct_mk_injective (M : Type*) [AddCommGroup M] [Module A M] :
Function.Injective (TensorProduct.mk A B M 1) :=
by
rw [← Module.FaithfullyFlat.lTensor_injective_iff_injective A B]
have :
(lTensor B <| TensorProduct.mk A B M 1) =
(TensorProduct.leftComm A B B M).symm.comp (TensorProduct.mk A B (B ⊗[A] M) 1) :=
by
apply TensorProduct.ext'
intro x y
simp
rw [this, coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective]
exact Algebra.TensorProduct.mk_one_injective_of_isScalarTower _
