English
If every localization of R at a maximal ideal is a valuation ring, then a module M over R is flat iff it has no torsion.
Русский
Если каждая локализация кольца R в максимальной идеальной локализации являетсяvaluation ring, тогда R-модуль M плоский тогда и только тогда, когда у него отсутствует торсион.
LaTeX
$$$Flat\\,R\\,M \\iff torsion\\,R\\,M = \\bot$ \n\\text{(under suitable localization hypotheses)}$$
Lean4
/-- If every localization of `R` at a maximal ideal is a valuation ring then an `R`-module
is flat iff it has no torsion. -/
theorem flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal [IsDomain R]
(h : ∀ (P : Ideal R), [P.IsMaximal] → ValuationRing (Localization P.primeCompl)) : Flat R M ↔ torsion R M = ⊥ :=
by
refine ⟨fun _ ↦ Flat.torsion_eq_bot, fun h ↦ ?_⟩
apply flat_of_localized_maximal
intro P hP
rw [← Submodule.noZeroSMulDivisors_iff_torsion_eq_bot] at h
rw [← flat_iff_of_isLocalization (Localization P.primeCompl) P.primeCompl, Flat.flat_iff_torsion_eq_bot_of_isBezout, ←
Submodule.noZeroSMulDivisors_iff_torsion_eq_bot]
infer_instance
