iff_lift_lsmul_comp_subtype_injective

English

The flatness condition is equivalent to the corresponding lTensor injectivity property for all rings and modules, via a standard commutation isomorphism.

Русский

Условие плоскости эквивалентно соответствующему свойству инъективности отображения, связанного через тензор, для всех колец и модулей.

LaTeX

$$$\text{Flat } R M \iff \forall I,\; I.FG \to Injective(TensorProduct.lift (I.subtype))$$$

Lean4

/-- An `R`-module `M` is flat if for all finitely generated ideals `I` of `R`,
the canonical map `I ⊗ M →ₗ M` is injective. -/
theorem iff_lift_lsmul_comp_subtype_injective :
    Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective (TensorProduct.lift ((lsmul R M).comp I.subtype)) := by
  simp [iff_rTensor_injective, ← lid_comp_rTensor]

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