Commit 2026-05-12 12:43 52e99ade

View on Github →

chore(RingTheory/Localization/AtPrime/Basic): use under instead of comap (algebraMap R S) (#37840) This PR switches over from comap (algebraMap R S) to under.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Noetherian.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/RingTheory/DedekindDomain/Dvr.lean

Modified Mathlib/RingTheory/Etale/QuasiFinite.lean

Modified Mathlib/RingTheory/Frobenius.lean

Modified Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean

Modified Mathlib/RingTheory/Ideal/GoingUp.lean

Modified Mathlib/RingTheory/Ideal/Height.lean

deleted theorem IsLocalization.height_comap

added theorem IsLocalization.height_under

deleted theorem IsLocalization.primeHeight_comap

added theorem IsLocalization.primeHeight_under

Modified Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.mem_under

Modified Mathlib/RingTheory/IntegralClosure/GoingDown.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/KrullDimension/Polynomial.lean

Modified Mathlib/RingTheory/LocalProperties/Injective.lean

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

deleted theorem IsLocalization.AtPrime.comap_map_eq_map

deleted theorem IsLocalization.AtPrime.comap_map_of_isMaximal

deleted theorem IsLocalization.AtPrime.comap_maximalIdeal

deleted theorem IsLocalization.AtPrime.comap_maximalIdeal_pow

added theorem IsLocalization.AtPrime.under_map_eq_map

added theorem IsLocalization.AtPrime.under_map_of_isMaximal

added theorem IsLocalization.AtPrime.under_maximalIdeal

added theorem IsLocalization.AtPrime.under_maximalIdeal_pow

deleted theorem Localization.AtPrime.comap_maximalIdeal

deleted theorem Localization.AtPrime.eq_maximalIdeal_iff_comap_eq

added theorem Localization.AtPrime.eq_maximalIdeal_iff_under_eq

added theorem Localization.AtPrime.under_maximalIdeal

Modified Mathlib/RingTheory/Localization/AtPrime/Extension.lean

Modified Mathlib/RingTheory/Localization/Ideal.lean

deleted theorem IsLocalization.bot_lt_comap_prime

added theorem IsLocalization.bot_lt_under_prime

deleted theorem IsLocalization.comap_le_comap_iff

deleted theorem IsLocalization.comap_map_of_isPrimary_disjoint

deleted theorem IsLocalization.comap_map_of_isPrime_disjoint

deleted theorem IsLocalization.disjoint_comap_iff

added theorem IsLocalization.disjoint_under_iff

deleted theorem IsLocalization.ideal_eq_iInf_comap_map_away

added theorem IsLocalization.ideal_eq_iInf_under_map_away

deleted theorem IsLocalization.map_comap

added theorem IsLocalization.map_under

added theorem IsLocalization.under_le_under_iff

added theorem IsLocalization.under_map_of_isPrimary_disjoint

added theorem IsLocalization.under_map_of_isPrime_disjoint

Modified Mathlib/RingTheory/QuasiFinite/Basic.lean

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