rTensor_injective_of_forall_fg_rTensor_injective

English

If injectivity holds for all FG submodules, then it holds for any submodule M'.

Русский

Если инъективность верна для всех FG-подмодулей, то она верна и для любого подмодуля M'.

LaTeX

$$$(\\forall M' : Submodule R M, M'.FG) \\Rightarrow Injective(rTensor N M'.subtype) \\Rightarrow Injective(rTensor N M'.subtype)$$

Lean4

/-- If the map $M' \otimes N \to M \otimes N$ is injective for every finitely generated submodule
$M' \subseteq M$, then it is in fact injective for every submodule $M' \subseteq M$. -/
theorem rTensor_injective_of_forall_fg_rTensor_injective
    (hMN : ∀ (M' : Submodule R M) (_ : M'.FG), Injective (rTensor N M'.subtype)) (M' : Submodule R M) :
    Injective (rTensor N M'.subtype) :=
  (forall_vanishesTrivially_iff_forall_rTensor_injective R).mp
    ((forall_vanishesTrivially_iff_forall_fg_rTensor_injective R).mpr hMN) M'

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