Commit 2025-02-13 14:24 ad42f0c3

View on Github →

feat(RingTheory): flat algebras satisfy going down (#21798) We introduce a predicate on algebras Algebra.HasGoingDown capturing if an algebra satisfies the going-down property. Then we show that flat algebras satisfy this predicate. Co-authored by: Sihan Su ssh@stu.pku.edu.cn Co-authored by: Yi Song sif4delta0@mail.ustc.edu.cn

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Flat/Localization.lean

Created Mathlib/RingTheory/Ideal/GoingDown.lean

added theorem Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap

added theorem Algebra.HasGoingDown.of_specComap_localRingHom_surjective

added theorem Algebra.HasGoingDown.trans

added theorem Ideal.exists_ideal_le_liesOver_of_le

added theorem Ideal.exists_ideal_lt_liesOver_of_lt

Modified Mathlib/RingTheory/Localization/AtPrime.lean

added theorem Ideal.isPrime_map_of_isLocalizationAtPrime

added theorem Ideal.under_map_of_isLocalizationAtPrime