tensorProduct_mapIncl_injective_of_left

English

If p ⊆ M and q ⊆ N are submodules with M flat and N flat, then mapIncl p q : p ⊗ q → M ⊗ N is injective.

Русский

Если p ⊆ M, q ⊆ N — подмодули, и M,N плоские, то mapIncl p q инъективно.

LaTeX

$$$\\text{Injective}(\\mathrm{mapIncl}\\, p\\, q)$$$

Lean4

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

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