Commit 2025-01-23 19:32 ab9317ed

View on Github →

feat(RingTheory/Artinian): rewrite results using spectra types instead of sets (#20828) Rewrite results about artinian rings using MaximalSpectrum and PrimeSpectrum instead of sets {I | I.IsMaximal} and {I | I.IsPrime}.

Estimated changes

Modified Mathlib/RingTheory/Artinian/Instances.lean

Modified Mathlib/RingTheory/Artinian/Module.lean

deleted theorem IsArtinianRing.maximal_ideals_finite

added def IsArtinianRing.primeSpectrumEquivMaximalSpectrum

added theorem IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal

added theorem IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal

added theorem IsArtinianRing.primeSpectrum_asIdeal_range_eq

deleted theorem IsArtinianRing.primeSpectrum_finite

added theorem IsArtinianRing.setOf_isMaximal_finite

added theorem IsArtinianRing.setOf_isPrime_finite

deleted theorem IsArtinianRing.subtype_isMaximal_finite

Modified Mathlib/RingTheory/Etale/Field.lean

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

added def MaximalSpectrum.equivSubtype

added theorem MaximalSpectrum.range_asIdeal

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

added theorem PrimeSpectrum.nilradical_eq_iInf

added theorem PrimeSpectrum.range_asIdeal

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