English
If b ∈ I, then a + b ∈ I iff a ∈ I.
Русский
Если b ∈ I, то a + b ∈ I тогда и только тогда, когда a ∈ I.
LaTeX
$$$\forall I\; (b:\alpha) (a:\alpha),\; b \in I \rightarrow (a+b \in I \iff a \in I).$$$
Lean4
/-- Flat algebras satisfy the going down property. -/
@[stacks 00HS]
instance of_flat [Module.Flat R S] : Algebra.HasGoingDown R S :=
by
apply of_specComap_localRingHom_surjective
intro P hP
have : IsLocalHom (algebraMap (Localization.AtPrime <| P.under R) (Localization.AtPrime P)) :=
by
rw [RingHom.algebraMap_toAlgebra]
exact Localization.isLocalHom_localRingHom (P.under R) P (algebraMap R S) Ideal.LiesOver.over
have : Module.FaithfullyFlat (Localization.AtPrime (P.under R)) (Localization.AtPrime P) :=
Module.FaithfullyFlat.of_flat_of_isLocalHom
apply PrimeSpectrum.specComap_surjective_of_faithfullyFlat
