Commit 2025-01-20 12:00 edaed4a2

View on Github →

refactor(RingTheory): split off heavy results from Mathlib/RingTheory/Spectrum/*/Basic.lean (#20845) Split off heavy results from Mathlib/RingTheory/Spectrum/Prime/Basic.lean and Mathlib/RingTheory/Spectrum/Maximal/Basic.lean to be able to import these files where only definitions and basic results are needed.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/KrullDimension/Basic.lean

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

deleted theorem MaximalSpectrum.finite_of_toPiLocalization_pi_surjective

deleted theorem MaximalSpectrum.finite_of_toPiLocalization_surjective

deleted theorem MaximalSpectrum.iInf_localization_eq_bot

deleted theorem MaximalSpectrum.mapPiLocalization_bijective

deleted theorem MaximalSpectrum.mapPiLocalization_comp

deleted theorem MaximalSpectrum.mapPiLocalization_id

deleted theorem MaximalSpectrum.mapPiLocalization_naturality

deleted def MaximalSpectrum.toPiLocalization

deleted theorem MaximalSpectrum.toPiLocalization_apply_apply

deleted theorem MaximalSpectrum.toPiLocalization_injective

deleted theorem MaximalSpectrum.toPiLocalization_not_surjective_of_infinite

deleted theorem PrimeSpectrum.finite_of_toPiLocalization_pi_surjective

deleted theorem PrimeSpectrum.finite_of_toPiLocalization_surjective

deleted theorem PrimeSpectrum.iInf_localization_eq_bot

deleted theorem PrimeSpectrum.isMaximal_of_toPiLocalization_surjective

deleted theorem PrimeSpectrum.mapPiLocalization_bijective

deleted theorem PrimeSpectrum.mapPiLocalization_comp

deleted theorem PrimeSpectrum.mapPiLocalization_id

deleted theorem PrimeSpectrum.mapPiLocalization_naturality

deleted def PrimeSpectrum.piLocalizationToMaximal

deleted def PrimeSpectrum.piLocalizationToMaximalEquiv

deleted theorem PrimeSpectrum.piLocalizationToMaximal_bijective

deleted theorem PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization

deleted theorem PrimeSpectrum.piLocalizationToMaximal_surjective

deleted def PrimeSpectrum.toPiLocalization

deleted theorem PrimeSpectrum.toPiLocalization_injective

deleted theorem PrimeSpectrum.toPiLocalization_not_surjective_of_infinite

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

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

added theorem MaximalSpectrum.finite_of_toPiLocalization_pi_surjective

added theorem MaximalSpectrum.finite_of_toPiLocalization_surjective

added theorem MaximalSpectrum.iInf_localization_eq_bot

added theorem MaximalSpectrum.mapPiLocalization_bijective

added theorem MaximalSpectrum.mapPiLocalization_comp

added theorem MaximalSpectrum.mapPiLocalization_id

added theorem MaximalSpectrum.mapPiLocalization_naturality

added def MaximalSpectrum.toPiLocalization

added theorem MaximalSpectrum.toPiLocalization_apply_apply

added theorem MaximalSpectrum.toPiLocalization_injective

added theorem MaximalSpectrum.toPiLocalization_not_surjective_of_infinite

added theorem PrimeSpectrum.finite_of_toPiLocalization_pi_surjective

added theorem PrimeSpectrum.finite_of_toPiLocalization_surjective

added theorem PrimeSpectrum.iInf_localization_eq_bot

added theorem PrimeSpectrum.isMaximal_of_toPiLocalization_surjective

added theorem PrimeSpectrum.mapPiLocalization_bijective

added theorem PrimeSpectrum.mapPiLocalization_comp

added theorem PrimeSpectrum.mapPiLocalization_id

added theorem PrimeSpectrum.mapPiLocalization_naturality

added def PrimeSpectrum.piLocalizationToMaximal

added def PrimeSpectrum.piLocalizationToMaximalEquiv

added theorem PrimeSpectrum.piLocalizationToMaximal_bijective

added theorem PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization

added theorem PrimeSpectrum.piLocalizationToMaximal_surjective

added def PrimeSpectrum.toPiLocalization

added theorem PrimeSpectrum.toPiLocalization_injective

added theorem PrimeSpectrum.toPiLocalization_not_surjective_of_infinite

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

deleted theorem PrimeSpectrum.localization_specComap_injective

deleted theorem PrimeSpectrum.localization_specComap_range

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

added theorem PrimeSpectrum.localization_specComap_injective

added theorem PrimeSpectrum.localization_specComap_range