English
Flat is a local property of ring homomorphisms: to check flatness it suffices to check after localization on a cover that generates the unit ideal.
Русский
Плоскость является локальным свойством гомоморфизмов колец: проверка плоскости сводится к локализации на покрытии, порождающем единичную идеал.
LaTeX
$$$$\text{PropertyIsLocal}(Flat).$$$$
Lean4
/-- Flat is a local property of ring homomorphisms. -/
theorem propertyIsLocal : PropertyIsLocal Flat
where
localizationAwayPreserves := isStableUnderBaseChange.localizationPreserves.away
ofLocalizationSpanTarget := ofLocalizationSpanTarget
ofLocalizationSpan :=
ofLocalizationSpanTarget.ofLocalizationSpan
(stableUnderComposition.stableUnderCompositionWithLocalizationAway holdsForLocalizationAway).left
StableUnderCompositionWithLocalizationAwayTarget :=
(stableUnderComposition.stableUnderCompositionWithLocalizationAway holdsForLocalizationAway).right
