Commit 2025-04-02 12:19 fb7d6661

View on Github →

feat(RingTheory): Chevalley's theorem (#23571) Also shows that flat ring homomorphisms of finite presentation are open maps on the prime spectrum

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/FinitePresentation.lean

added theorem RingHom.finitePresentation_algebraMap

Created Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean

added theorem PrimeSpectrum.isConstructible_comap_C

added theorem PrimeSpectrum.isConstructible_comap_image

added theorem PrimeSpectrum.isConstructible_range_comap

added theorem PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation

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

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

added theorem PrimeSpectrum.ConstructibleSetData.isConstructible_toSet

added theorem PrimeSpectrum.exists_constructibleSetData_iff

added theorem PrimeSpectrum.exists_range_eq_of_isConstructible

added theorem PrimeSpectrum.isClosed_of_stableUnderSpecialization_of_isConstructible

added theorem PrimeSpectrum.isOpen_of_stableUnderGeneralization_of_isConstructible

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

added theorem PrimeSpectrum.exists_comap_evalRingHom_eq

added theorem PrimeSpectrum.iUnion_range_specComap_comp_evalRingHom

added theorem PrimeSpectrum.sigmaToPi_bijective

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

added theorem PrimeSpectrum.isConstructible_basicOpen

added theorem PrimeSpectrum.isRetrocompact_basicOpen

added theorem PrimeSpectrum.isRetrocompact_zeroLocus_compl

added theorem PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg