Commit 2025-04-03 11:07 9f9c150c

View on Github →

feat(AlgebraicGeometry): faithfully flat morphisms are topological quotient maps (#23608)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

added theorem AlgebraicGeometry.IsLocalAtSource.sigmaDesc

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

added theorem AlgebraicGeometry.Flat.isQuotientMap_of_surjective

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

added theorem AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

added theorem AlgebraicGeometry.Surjective.sigmaDesc_of_union_range_eq_univ

Modified Mathlib/AlgebraicGeometry/PullbackCarrier.lean

Modified Mathlib/RingTheory/RingHom/Flat.lean

added theorem RingHom.Flat.generalizingMap_comap

added theorem flat_algebraMap_iff

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

added theorem PrimeSpectrum.isQuotientMap_of_generalizingMap

added theorem PrimeSpectrum.isQuotientMap_of_specializingMap