tensorProduct_mapIncl_injective_of_right

English

If p ⊆ M and q ⊆ N are submodules with M flat and q flat, then the natural map p ⊗ q → M ⊗ N is injective.

Русский

Если p ⊆ M и q ⊆ N — это подмодули, и M, q плоские, то естественное отображение p ⊗ q → M ⊗ N инъективно.

LaTeX

$$$\\mathrm{mapIncl}\, p\\, q: p \\otimes_R q \\to M \\otimes_R N\\;\\text{ injective}$$$

Lean4

/-- If p and q are submodules of M and N respectively, and M and q are flat,
then `p ⊗ q → M ⊗ N` is injective. -/
theorem _root_.Module.Flat.tensorProduct_mapIncl_injective_of_right [Module.Flat R M] [Module.Flat R q] :
    Function.Injective (mapIncl p q) :=
  TensorProduct.map_injective_of_flat_flat _ _ p.subtype_injective q.subtype_injective

Похожие утверждения