English
Flatness is equivalent to injectivity of rTensor with respect to all ideals I.
Русский
Плоскость эквивалентна инъективности rTensor по отношению ко всем идеалам I.
LaTeX
$$$\\text{Flat}(R,M) \\iff \\forall I, \\text{FG} \\to \\text{Injective}(rTensor M (I.subtype))$$$
Lean4
/-- An `R`-module `M` is flat iff for all ideals `I` of `R`, the tensor product of the
inclusion `I → R` and the identity `M → M` is injective. See `iff_rTensor_injective` to
restrict to finitely generated ideals `I`. -/
theorem iff_rTensor_injective' : Flat R M ↔ ∀ I : Ideal R, Function.Injective (rTensor M I.subtype) := by
simp_rw [iff_characterModule_baer, Baer, rTensor_injective_iff_lcomp_surjective, Surjective, DFunLike.ext_iff,
Subtype.forall, lcomp_apply, Submodule.subtype_apply]
