Commit 2024-09-24 20:52 38464838

View on Github →

chore (PrimeSpectrum): RingHom.primeComap and API (#15114) We break out the function PrimeSpectrum.comap.toFun into RingHom.primeComap and copy the API for PrimeSpectrum.comap independent of the Zariski topology into RingTheory.PrimeSpectrum for primeComap. We then feed that API back into the proofs for comap directly.

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

deleted theorem PrimeSpectrum.preimage_comap_zeroLocus_aux

Modified Mathlib/RingTheory/PrimeSpectrum.lean

added theorem PrimeSpectrum.localization_specComap_injective

added theorem PrimeSpectrum.localization_specComap_range

added theorem PrimeSpectrum.preimage_specComap_zeroLocus

added theorem PrimeSpectrum.preimage_specComap_zeroLocus_aux

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