English
A flat R-module M is characterized by the injectivity of lift of lsmul with subtype across all I.
Русский
Плоскость M над R характеризуется инъективностью lift от lsmul с подклассами I.
LaTeX
$$$Flat(R,M) \\iff \\forall I, FG \\to Injective( TensorProduct.lift ((lsmul R M).comp I.subtype) )$$$
Lean4
/-- A module `M` over a ring `R` is flat iff for all finitely generated ideals `I` of `R`, the
tensor product of the inclusion `I → R` and the identity `M → M` is injective. See
`iff_rTensor_injective'` to extend to all ideals `I`. -/
theorem iff_rTensor_injective : Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective (I.subtype.rTensor M) :=
by
refine iff_rTensor_injective'.trans ⟨fun h I _ ↦ h I, fun h I ↦ (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_⟩
obtain ⟨J, hfg, hle, y, rfl⟩ := Submodule.exists_fg_le_eq_rTensor_inclusion x
rw [← rTensor_comp_apply] at hx
rw [(injective_iff_map_eq_zero _).mp (h hfg) y hx, map_zero]
