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`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/AlgebraicGeometry/Noetherian.lean

@@ -85,8 +85,8 @@ theorem isNoetherianRing_of_away : IsNoetherianRing R := by
   use N
   have hN : ∀ s : S, minN s ≤ N := fun s => Finset.le_sup s.prop
   intro n hn
-  rw [IsLocalization.ideal_eq_iInf_comap_map_away hS (I N),
-      IsLocalization.ideal_eq_iInf_comap_map_away hS (I n),
+  rw [IsLocalization.ideal_eq_iInf_under_map_away hS (I N),
+      IsLocalization.ideal_eq_iInf_under_map_away hS (I n),
       iInf_subtype', iInf_subtype']
   apply iInf_congr
   intro s

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -179,8 +179,8 @@ theorem mk_mem_carrier (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (.powers
     HomogeneousLocalization.mk z ∈ carrier x ↔ z.num.1 ∈ x.1.asHomogeneousIdeal := by
   rw [carrier, Ideal.mem_comap, HomogeneousLocalization.algebraMap_apply,
     HomogeneousLocalization.val_mk, Localization.mk_eq_mk', IsLocalization.mk'_eq_mul_mk'_one,
-    mul_comm, Ideal.unit_mul_mem_iff_mem, ← Ideal.mem_comap,
-    IsLocalization.comap_map_of_isPrime_disjoint (.powers f)]
+    mul_comm, Ideal.unit_mul_mem_iff_mem, ← Ideal.mem_under,
+    IsLocalization.under_map_of_isPrime_disjoint (.powers f)]
   · rfl
   · infer_instance
   · exact (disjoint_powers_iff_notMem_of_isPrime _).mpr x.2

Mathlib/RingTheory/DedekindDomain/Dvr.lean

@@ -72,13 +72,8 @@ theorem Ring.DimensionLEOne.localization {R : Type*} (Rₘ : Type*) [CommRing R]
   refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩
   have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
   rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
-  haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p) :=
-    ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩).2.1
-  haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P) :=
-    ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, hPm.isPrime⟩).2.1
-  have hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P := hpP'
-  refine h.not_lt_lt ⊥ (Ideal.comap _ _) (Ideal.comap _ _) ⟨?_, hlt⟩
-  exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0⟩
+  refine h.not_lt_lt ⊥ (p.under R) (P.under R) ⟨?_, hpP'⟩
+  exact IsLocalization.bot_lt_under_prime _ _ hM _ hp0⟩
 
 /-- The localization of a Dedekind domain is a Dedekind domain. -/
 theorem IsLocalization.isDedekindDomain [IsDedekindDomain A] {M : Submonoid A} (hM : M ≤ A⁰)

Mathlib/RingTheory/Etale/QuasiFinite.lean

@@ -175,7 +175,7 @@ lemma Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver
     rw [Ideal.disjoint_powers_iff_notMem_of_isPrime]
     contrapose H; exact Ideal.mul_mem_right s₃ _ (Ideal.pow_mem_of_mem _ H m hm0)
   have : q's.IsPrime := IsLocalization.isPrime_of_isPrime_disjoint (.powers s₂) _ _ ‹_› hq's
-  have : q's.LiesOver q' := ⟨(IsLocalization.comap_map_of_isPrime_disjoint _ _ ‹_› hq's).symm⟩
+  have : q's.LiesOver q' := ⟨(IsLocalization.under_map_of_isPrime_disjoint _ _ ‹_› hq's).symm⟩
   have : q's.LiesOver p := .trans _ q' _
   have := hs₁ (q's.comap (e.symm.toAlgHom.comp (IsScalarTower.toAlgHom _ _ _)).toRingHom)
     inferInstance (by
@@ -393,8 +393,8 @@ lemma Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq
   let Pf := P.map (algebraMap _ (Localization.Away f))
   have : Pf.IsPrime := IsLocalization.isPrime_of_isPrime_disjoint (.powers f) _ _ ‹_› (by
     rwa [Ideal.disjoint_powers_iff_notMem_of_isPrime])
-  have : Pf.LiesOver P := ⟨(IsLocalization.comap_map_of_isPrime_disjoint (.powers f) _ ‹_› (by
-    rwa [Ideal.disjoint_powers_iff_notMem_of_isPrime])).symm⟩
+  have : Pf.LiesOver P := ⟨(IsLocalization.under_map_of_isPrime_disjoint (.powers f) _ ‹_› (by
+    rwa [Ideal.disjoint_powers_iff_notMem _ (Ideal.IsPrime.isRadical ‹_›)])).symm⟩
   let φ : R' ⊗[R] S →ₐ[R'] Localization.Away f ⊗[R] S :=
     Algebra.TensorProduct.map (Algebra.ofId _ _) (.id _ _)
   let := φ.toAlgebra
@@ -410,7 +410,7 @@ lemma Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq
     change f ∉ P'.under _
     rwa [← P'.over_def P]
   have : P'f.IsPrime := IsLocalization.isPrime_of_isPrime_disjoint _ _ _ ‹_› hP'f
-  have : P'f.LiesOver P' := ⟨(IsLocalization.comap_map_of_isPrime_disjoint _ _ ‹_› hP'f).symm⟩
+  have : P'f.LiesOver P' := ⟨(IsLocalization.under_map_of_isPrime_disjoint _ _ ‹_› hP'f).symm⟩
   have : P'f.LiesOver P := .trans _ P' _
   have : P'f.LiesOver Pf := ⟨congr($(PrimeSpectrum.localization_comap_injective
       (Localization.Away f) (.powers f) (a₁ := ⟨Pf, ‹_›⟩)

Mathlib/RingTheory/Frobenius.lean

@@ -147,8 +147,7 @@ lemma isArithFrobAt_localize [Q.IsPrime] : H.localize.IsArithFrobAt (maximalIdea
   have h : Nat.card (R ⧸ (maximalIdeal _).comap (algebraMap R (Localization.AtPrime Q))) =
       Nat.card (R ⧸ Q.under R) := by
     congr 2
-    rw [IsScalarTower.algebraMap_eq R S (Localization.AtPrime Q), ← Ideal.comap_comap,
-      Localization.AtPrime.comap_maximalIdeal]
+    rw [← Ideal.under_def, ← Ideal.under_under (B := S), Localization.AtPrime.under_maximalIdeal]
   intro x
   obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq Q.primeCompl x
   simp only [localize, coe_mk, Localization.localRingHom_mk', RingHom.coe_coe, h,

Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean

@@ -43,7 +43,7 @@ lemma mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule
   rcases ass with ⟨hp, x, hx⟩
   constructor
   · refine (IsLocalization.isPrime_iff_isPrime_disjoint S _ _).mpr
-      ⟨hp, (IsLocalization.disjoint_comap_iff S R' p).mpr ?_⟩
+      ⟨hp, (IsLocalization.disjoint_under_iff S R' p).mpr ?_⟩
     by_contra eqtop
     simp [eqtop, Ideal.comap_top, Ideal.isPrime_iff] at hp
   · use f x
@@ -73,7 +73,7 @@ lemma mem_associatedPrimes_atPrime_of_mem_associatedPrimes
     associatedPrimes (Localization.AtPrime p) (LocalizedModule.AtPrime p M) := by
   apply mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule
     p.primeCompl (LocalizedModule.mkLinearMap p.primeCompl M)
-  simpa [Localization.AtPrime.comap_maximalIdeal] using ass
+  simpa [Localization.AtPrime.under_maximalIdeal] using ass
 
 @[deprecated (since := "2025-11-27")]
 alias mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes :=
@@ -112,7 +112,7 @@ lemma comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of
     apply hp.mem_of_pow_mem k
     rw [← map_pow]
     exact ((hp.under R).mul_mem_iff_mem_or_mem.mp mem).resolve_right
-      (Set.disjoint_left.mp ((IsLocalization.disjoint_comap_iff S R' p).mpr hp.1) (∏ a, g a).2)
+      (Set.disjoint_left.mp ((IsLocalization.disjoint_under_iff S R' p).mpr hp.1) (∏ a, g a).2)
 
 variable (R')
 
@@ -142,7 +142,7 @@ lemma minimalPrimes_annihilator_subset_associatedPrimes [IsNoetherianRing R] [Mo
   have ann_le : Module.annihilator R M ≤ Ideal.comap (algebraMap R Rₚ) q :=
     le_of_eq_of_le Submodule.annihilator_top.symm (IsAssociatedPrime.annihilator_le hq)
   have le : Ideal.comap (algebraMap R Rₚ) q ≤ p := by
-    have := (IsLocalization.disjoint_comap_iff p.primeCompl Rₚ q).mpr q_prime.ne_top
+    have := (IsLocalization.disjoint_under_iff p.primeCompl Rₚ q).mpr q_prime.ne_top
     simpa only [Ideal.primeCompl, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
       Set.disjoint_compl_left_iff_subset] using this
   simpa [Minimal.eq_of_le hp.out ⟨IsAssociatedPrime.isPrime hq, ann_le⟩ le] using hq

Mathlib/RingTheory/Ideal/GoingUp.lean

@@ -288,7 +288,7 @@ theorem exists_ideal_over_prime_of_isIntegral_of_isDomain [Algebra.IsIntegral R
   have Qₚ_max : IsMaximal (comap _ Qₚ) :=
     isMaximal_comap_of_isIntegral_of_isMaximal (R := Rₚ) (S := Sₚ) Qₚ
   refine ⟨comap (algebraMap S Sₚ) Qₚ, ⟨comap_isPrime _ Qₚ, ?_⟩⟩
-  convert Localization.AtPrime.comap_maximalIdeal (I := P)
+  convert Localization.AtPrime.under_maximalIdeal (I := P)
   rw [comap_comap, ← IsLocalRing.eq_maximalIdeal Qₚ_max,
     ← IsLocalization.map_comp (P := S) (Q := Sₚ) (g := algebraMap R S)
     (M := P.primeCompl) (T := Algebra.algebraMapSubmonoid S P.primeCompl) (S := Rₚ)

Mathlib/RingTheory/Ideal/Height.lean

@@ -326,9 +326,9 @@ lemma ringKrullDim_le_iff_isMaximal_height_le {R : Type*} [CommRing R] (n : With
   norm_cast
   exact Ideal.height_mono hle
 
-theorem IsLocalization.primeHeight_comap (S : Submonoid R) {A : Type*} [CommRing A] [Algebra R A]
+theorem IsLocalization.primeHeight_under (S : Submonoid R) {A : Type*} [CommRing A] [Algebra R A]
     [IsLocalization S A] (J : Ideal A) [J.IsPrime] :
-    (J.comap (algebraMap R A)).primeHeight = J.primeHeight := by
+    (J.under R).primeHeight = J.primeHeight := by
   rw [eq_comm, Ideal.primeHeight, Ideal.primeHeight, ← WithBot.coe_inj,
     Order.height_eq_krullDim_Iic, Order.height_eq_krullDim_Iic]
   let e := IsLocalization.orderIsoOfPrime S A
@@ -343,19 +343,25 @@ theorem IsLocalization.primeHeight_comap (S : Submonoid R) {A : Type*} [CommRing
         congrArg (fun I ↦ I.1) (e.right_inv ⟨_, I.1.2, H _ I.2⟩)
       map_rel_iff' {I₁ I₂} := @RelIso.map_rel_iff _ _ _ _ e ⟨_, I₁.1.2⟩ ⟨_, I₂.1.2⟩ }
 
-theorem IsLocalization.height_comap (S : Submonoid R) {A : Type*} [CommRing A] [Algebra R A]
-    [IsLocalization S A] (J : Ideal A) : (J.comap (algebraMap R A)).height = J.height := by
+@[deprecated (since := "2026-04-09")] alias IsLocalization.primeHeight_comap :=
+  IsLocalization.primeHeight_under
+
+theorem IsLocalization.height_under (S : Submonoid R) {A : Type*} [CommRing A] [Algebra R A]
+    [IsLocalization S A] (J : Ideal A) : (J.under R).height = J.height := by
   rw [Ideal.height, Ideal.height]
-  simp_rw [← IsLocalization.primeHeight_comap S, IsLocalization.minimalPrimes_comap S A,
+  simp_rw [← IsLocalization.primeHeight_under S, IsLocalization.minimalPrimes_comap S A,
     ← Ideal.height_eq_primeHeight, iInf_image]
 
+@[deprecated (since := "2026-04-09")] alias IsLocalization.height_comap :=
+  IsLocalization.height_under
+
 theorem IsLocalization.AtPrime.ringKrullDim_eq_height (I : Ideal R) [I.IsPrime] (A : Type*)
     [CommRing A] [Algebra R A] [IsLocalization.AtPrime A I] :
     ringKrullDim A = I.height := by
   have := IsLocalization.AtPrime.isLocalRing A I
   rw [← IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim,
-      ← IsLocalization.primeHeight_comap I.primeCompl,
-      ← IsLocalization.AtPrime.comap_maximalIdeal A I,
+      ← IsLocalization.primeHeight_under I.primeCompl,
+      ← IsLocalization.AtPrime.under_maximalIdeal A I,
       Ideal.height_eq_primeHeight]
 
 lemma IsLocalization.height_map_of_disjoint {S : Type*} [CommRing S] [Algebra R S] (M : Submonoid R)
@@ -364,7 +370,7 @@ lemma IsLocalization.height_map_of_disjoint {S : Type*} [CommRing S] [Algebra R
   let P := p.map (algebraMap R S)
   have : P.IsPrime := isPrime_of_isPrime_disjoint M S p ‹_› h
   have := isLocalization_isLocalization_atPrime_isLocalization (M := M) (Localization.AtPrime P) P
-  simp_rw [P, comap_map_of_isPrime_disjoint M S _ h] at this
+  simp_rw [P, under_map_of_isPrime_disjoint M S _ h] at this
   have := ringKrullDim_eq_of_ringEquiv (IsLocalization.algEquiv p.primeCompl
     (Localization.AtPrime P) (Localization.AtPrime p)).toRingEquiv
   rw [AtPrime.ringKrullDim_eq_height P, AtPrime.ringKrullDim_eq_height p] at this

Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

@@ -109,10 +109,10 @@ lemma Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes
   have := hp.1.1
   let f := algebraMap R (Localization.AtPrime p)
   have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
-  · rwa [← IsLocalization.height_comap p.primeCompl,
-      Localization.AtPrime.comap_maximalIdeal] at this
+  · rwa [← IsLocalization.height_under p.primeCompl,
+      Localization.AtPrime.under_maximalIdeal] at this
   · rwa [IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I,
-      Set.mem_preimage, Localization.AtPrime.comap_maximalIdeal]
+      Set.mem_preimage, Localization.AtPrime.under_maximalIdeal]
 
 theorem Ideal.map_height_le_one_of_mem_minimalPrimes {I p : Ideal R} {x : R}
     (hp : p ∈ (I ⊔ span {x}).minimalPrimes) : (p.map (Ideal.Quotient.mk I)).height ≤ 1 :=
@@ -198,8 +198,8 @@ nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
       simp_all
     | succ n =>
       wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
-      · rw [← Localization.AtPrime.comap_maximalIdeal (I := p)] at hp ⊢
-        rw [IsLocalization.height_comap p.primeCompl]
+      · rw [← Localization.AtPrime.under_maximalIdeal (I := p)] at hp ⊢
+        rw [IsLocalization.height_under p.primeCompl]
         rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
         exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
           inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩

Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

@@ -179,7 +179,7 @@ section
 variable {R : Type*} [CommSemiring R] (S : Submonoid R) (A : Type*) [CommSemiring A] [Algebra R A]
 
 theorem IsLocalization.minimalPrimes_map [IsLocalization S A] (J : Ideal R) :
-    (J.map (algebraMap R A)).minimalPrimes = Ideal.comap (algebraMap R A) ⁻¹' J.minimalPrimes := by
+    (J.map (algebraMap R A)).minimalPrimes = Ideal.under R ⁻¹' J.minimalPrimes := by
   ext p
   constructor
   · intro hp
@@ -191,22 +191,22 @@ theorem IsLocalization.minimalPrimes_map [IsLocalization S A] (J : Ideal R) :
     refine (Ideal.comap_mono <|
       hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_
     · exact IsLocalization.isPrime_of_isPrime_disjoint S A I hI.1 hI'
-    · exact IsLocalization.comap_map_of_isPrime_disjoint S A hI.1 hI'
+    · exact IsLocalization.under_map_of_isPrime_disjoint S A hI.1 hI'
   · intro hp
     refine ⟨⟨?_, Ideal.map_le_iff_le_comap.mpr hp.1.2⟩, ?_⟩
-    · rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_comap_iff S]
+    · rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_under_iff S]
       refine ⟨hp.1.1, ?_⟩
       rintro rfl
       exact hp.1.1.ne_top rfl
     · intro I hI e
-      rw [← IsLocalization.map_comap S A I, ← IsLocalization.map_comap S A p]
+      rw [← IsLocalization.map_under S A I, ← IsLocalization.map_under S A p]
       haveI := hI.1
       exact Ideal.map_mono (hp.2 ⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hI.2⟩
         (Ideal.comap_mono e))
 
 theorem IsLocalization.minimalPrimes_comap [IsLocalization S A] (J : Ideal A) :
     (J.comap (algebraMap R A)).minimalPrimes = Ideal.comap (algebraMap R A) '' J.minimalPrimes := by
-  conv_rhs => rw [← map_comap S A J, minimalPrimes_map S]
+  conv_rhs => rw [← map_under S A J, minimalPrimes_map S]
   refine (Set.image_preimage_eq_iff.mpr ?_).symm
   exact subset_trans (Ideal.minimalPrimes_comap_subset (algebraMap R A) J) (by simp)
 
@@ -217,12 +217,12 @@ theorem IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes
   have : IsLocalRing A := AtPrime.isLocalRing A q
   rw [← Ideal.sInf_minimalPrimes, IsLocalization.minimalPrimes_map q.primeCompl A I]
   refine le_antisymm (sInf_le ?_) (le_sInf fun J hJ ↦ ?_)
-  · rwa [Set.mem_preimage, AtPrime.map_eq_maximalIdeal q A, AtPrime.comap_maximalIdeal A q]
-  · rw [← IsLocalization.comap_le_comap_iff q.primeCompl A,
-      AtPrime.map_eq_maximalIdeal q A, AtPrime.comap_maximalIdeal A q]
+  · rwa [Set.mem_preimage, map_eq_maximalIdeal q A, under_maximalIdeal A q]
+  · rw [← IsLocalization.under_le_under_iff q.primeCompl A,
+      AtPrime.map_eq_maximalIdeal q A, AtPrime.under_maximalIdeal A q]
     apply hIq.2 hJ.1
     have := hJ.1.1.ne_top
-    rw [ne_eq, Ideal.comap_eq_top_iff, ← ne_eq, ← disjoint_comap_iff q.primeCompl A J] at this
+    rw [ne_eq, Ideal.comap_eq_top_iff, ← ne_eq, ← disjoint_under_iff q.primeCompl A J] at this
     exact Set.disjoint_compl_left_iff_subset.mp this
 
 end