Commit 2025-02-12 16:16 256efff0

View on Github →

chore(RingTheory/Spectrum/Prime/Basic): move functoriality to its own file (#21498)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Spectrum/Maximal/Localization.lean

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

deleted def PrimeSpectrum.comapEquiv

deleted theorem PrimeSpectrum.exists_maximal_nmem_range_sigmaToPi_of_infinite

deleted theorem PrimeSpectrum.preimage_specComap_zeroLocus

deleted theorem PrimeSpectrum.preimage_specComap_zeroLocus_aux

deleted def PrimeSpectrum.sigmaToPi

deleted theorem PrimeSpectrum.sigmaToPi_injective

deleted theorem PrimeSpectrum.sigmaToPi_not_surjective_of_infinite

deleted theorem PrimeSpectrum.specComap_asIdeal

deleted theorem PrimeSpectrum.specComap_comp

deleted theorem PrimeSpectrum.specComap_comp_apply

deleted theorem PrimeSpectrum.specComap_id

deleted theorem PrimeSpectrum.specComap_injective_of_surjective

deleted theorem image_specComap_zeroLocus_eq_zeroLocus_comap

deleted theorem range_specComap_of_surjective

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

added def PrimeSpectrum.comapEquiv

added theorem PrimeSpectrum.exists_maximal_nmem_range_sigmaToPi_of_infinite

added theorem PrimeSpectrum.preimage_specComap_zeroLocus

added theorem PrimeSpectrum.preimage_specComap_zeroLocus_aux

added def PrimeSpectrum.sigmaToPi

added theorem PrimeSpectrum.sigmaToPi_injective

added theorem PrimeSpectrum.sigmaToPi_not_surjective_of_infinite

added theorem PrimeSpectrum.specComap_asIdeal

added theorem PrimeSpectrum.specComap_comp

added theorem PrimeSpectrum.specComap_comp_apply

added theorem PrimeSpectrum.specComap_id

added theorem PrimeSpectrum.specComap_injective_of_surjective

added theorem image_specComap_zeroLocus_eq_zeroLocus_comap

added theorem range_specComap_of_surjective