feat(RingTheory/Localization/AtPrime): bijection between prime ideals (#29322)

Let `R ⊆ S` be an extension of rings and `p` be a prime ideal of `R`. Denote by `Rₚ` the localization of `R` at the complement of `p` and by `Sₚ` the localization of `S` at the (image) of the complement of `p`.

In this PR, we study the extension `Rₚ ⊆ Sₚ` and the relation between the (nonzero) prime ideals of `Sₚ` and the prime ideals of `S` above `p`. In particular, we prove that (under suitable conditions) they are in bijection. In a following PR #27706, we prove that the residual degree and ramification index are preserved by this bijection.

Note. The new file `RingTheory.Localization.AtPrime.Extension` is imported in `RingTheory.Trace.Quotient` because one function from the latter was moved to the former, but the plan is eventually to move the isomorphisms proved in `RingTheory.Trace.Quotient` to `RingTheory.Localization.AtPrime.Basic` and `RingTheory.Localization.AtPrime.Extension` where they belong. This will be done in #27706.

Author: xroblot

Mathlib.lean

@@ -5851,6 +5851,7 @@ import Mathlib.RingTheory.Localization.Algebra
 import Mathlib.RingTheory.Localization.AsSubring
 import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.RingTheory.Localization.AtPrime.Basic
+import Mathlib.RingTheory.Localization.AtPrime.Extension
 import Mathlib.RingTheory.Localization.Away.AdjoinRoot
 import Mathlib.RingTheory.Localization.Away.Basic
 import Mathlib.RingTheory.Localization.Away.Lemmas

Mathlib/RingTheory/DedekindDomain/Instances.lean

@@ -189,6 +189,10 @@ instance [NoZeroSMulDivisors S T] : NoZeroSMulDivisors Sₚ Tₚ :=
     algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul _ <|
       Ideal.primeCompl_le_nonZeroDivisors P
 
+instance [Algebra.IsIntegral R S] : Algebra.IsIntegral Rₚ Sₚ :=
+  Algebra.isIntegral_def.mpr <| (algebraMap_eq_map_map_submonoid P.primeCompl S Rₚ Sₚ ▸
+    isIntegral_localization : (algebraMap Rₚ Sₚ).IsIntegral)
+
 variable [NoZeroSMulDivisors R T]
 
 instance : IsScalarTower Rₚ Sₚ Tₚ := by

Mathlib/RingTheory/Ideal/Maps.lean

@@ -671,6 +671,14 @@ lemma comap_map_eq_self_iff_of_isPrime {S : Type*} [CommSemiring S] {f : R →+*
   · rintro ⟨q, hq, rfl⟩
     simp
 
+/--
+For a maximal ideal `p` of `R`, `p` extended to `S` and restricted back to `R` is `p` if
+its image in `S` is not equal to `⊤`.
+-/
+theorem comap_map_eq_self_of_isMaximal (f : R →+* S) {p : Ideal R} [hP' : p.IsMaximal]
+    (hP : Ideal.map f p ≠ ⊤) : (map f p).comap f = p :=
+  (IsCoatom.le_iff_eq hP'.out (comap_ne_top _ hP)).mp <| le_comap_map
+
 end CommRing
 
 end MapAndComap

Mathlib/RingTheory/Ideal/Over.lean

@@ -176,6 +176,48 @@ theorem LiesOver.trans [𝔓.LiesOver P] [P.LiesOver p] : 𝔓.LiesOver p where
 theorem LiesOver.tower_bot [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P] : P.LiesOver p where
   over := by rw [𝔓.over_def p, 𝔓.over_def P, under_under]
 
+/--
+Consider the following commutative diagram of ring maps
+```
+A → B
+↓   ↓
+C → D
+```
+and let `P` be an ideal of `B`. The image in `C` of the ideal of `A` under `P` is included
+in the ideal of `C` under the image of `P` in `D`.
+-/
+theorem map_under_le_under_map {C D : Type*} [CommSemiring C] [Semiring D] [Algebra A C]
+    [Algebra C D] [Algebra A D] [Algebra B D] [IsScalarTower A C D] [IsScalarTower A B D] :
+    map (algebraMap A C) (under A P) ≤ under C (map (algebraMap B D) P) := by
+  apply le_comap_of_map_le
+  rw [map_map, ← IsScalarTower.algebraMap_eq, map_le_iff_le_comap,
+    IsScalarTower.algebraMap_eq A B D, ← comap_comap]
+  exact comap_mono <| le_comap_map
+
+/--
+Consider the following commutative diagram of ring maps
+```
+A → B
+↓   ↓
+C → D
+```
+and let `P` be an ideal of `B`. Assume that the image in `C` of the ideal of `A` under `P`
+is maximal and that the image of `P` in `D` is not equal to `D`, then the image in `C` of the
+ideal of `A` under `P` is equal to the ideal of `C` under the image of `P` in `D`.
+-/
+theorem under_map_eq_map_under {C D : Type*} [CommSemiring C] [Semiring D] [Algebra A C]
+    [Algebra C D] [Algebra A D] [Algebra B D] [IsScalarTower A C D] [IsScalarTower A B D]
+    (h₁ : (map (algebraMap A C) (under A P)).IsMaximal) (h₂ : map (algebraMap B D) P ≠ ⊤) :
+    under C (map (algebraMap B D) P) = map (algebraMap A C) (under A P) :=
+  (IsCoatom.le_iff_eq (isMaximal_def.mp h₁) (comap_ne_top (algebraMap C D) h₂)).mp <|
+    map_under_le_under_map P
+
+theorem disjoint_primeCompl_of_liesOver [p.IsPrime] [hPp : 𝔓.LiesOver p] :
+  Disjoint ((Algebra.algebraMapSubmonoid C p.primeCompl) : Set C) (𝔓 : Set C) := by
+  rw [liesOver_iff, under_def, SetLike.ext'_iff, coe_comap] at hPp
+  simpa only [Algebra.algebraMapSubmonoid, primeCompl, hPp, ← le_compl_iff_disjoint_left]
+    using Set.subset_compl_comm.mp (by simp)
+
 variable (B)
 
 instance under_liesOver_of_liesOver [𝔓.LiesOver p] : (𝔓.under B).LiesOver p :=

Mathlib/RingTheory/Localization/AtPrime/Basic.lean

@@ -163,6 +163,10 @@ theorem comap_maximalIdeal (h : IsLocalRing S := isLocalRing S I) :
     (IsLocalRing.maximalIdeal S).comap (algebraMap R S) = I :=
   Ideal.ext fun x => by simpa only [Ideal.mem_comap] using to_map_mem_maximal_iff _ I x
 
+theorem liesOver_maximalIdeal (h : IsLocalRing S := isLocalRing S I) :
+    (IsLocalRing.maximalIdeal S).LiesOver I :=
+  (Ideal.liesOver_iff _ _).mpr (comap_maximalIdeal _ _).symm
+
 theorem isUnit_mk'_iff (x : R) (y : I.primeCompl) : IsUnit (mk' S x y) ↔ x ∈ I.primeCompl :=
   ⟨fun h hx => mk'_mem_iff.mpr ((to_map_mem_maximal_iff S I x).mpr hx) h, fun h =>
     isUnit_iff_exists_inv.mpr ⟨mk' S ↑y ⟨x, h⟩, mk'_mul_mk'_eq_one ⟨x, h⟩ y⟩⟩
@@ -305,6 +309,8 @@ end AtPrime
 
 end Localization
 
+section
+
 variable (q : Ideal R) [q.IsPrime] (M : Submonoid R) {S : Type*} [CommSemiring S] [Algebra R S]
   [IsLocalization.AtPrime S q]
 
@@ -329,3 +335,27 @@ lemma IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes
     fun ⦃x⦄ a ↦ a⟩, fun i ↦ Subtype.ext <| PrimeSpectrum.ext <|
     (minimalPrimes_eq_minimals (R := R) ▸ hp).eq_of_le i.1.2 i.2⟩
   (IsLocalization.AtPrime.primeSpectrumOrderIso S p).subsingleton
+
+end
+
+namespace IsLocalization.AtPrime
+
+open Algebra IsLocalRing Ideal IsLocalization IsLocalization.AtPrime
+
+variable (p : Ideal R) [p.IsPrime] (Rₚ : Type*) [CommSemiring Rₚ] [Algebra R Rₚ]
+  [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Sₚ : Type*) [CommSemiring Sₚ] [Algebra S Sₚ]
+  [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [Algebra Rₚ Sₚ]
+  (P : Ideal S)
+
+theorem isPrime_map_of_liesOver [P.IsPrime] [P.LiesOver p] : (P.map (algebraMap S Sₚ)).IsPrime :=
+  isPrime_of_isPrime_disjoint _ _ _ inferInstance (Ideal.disjoint_primeCompl_of_liesOver P p)
+
+theorem map_eq_maximalIdeal : p.map (algebraMap R Rₚ) = maximalIdeal Rₚ := by
+  convert congr_arg (Ideal.map (algebraMap R Rₚ)) (comap_maximalIdeal Rₚ p).symm
+  rw [map_comap p.primeCompl]
+
+theorem comap_map_of_isMaximal [P.IsMaximal] [P.LiesOver p] :
+    Ideal.comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) P) = P :=
+  comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).ne_top
+
+end IsLocalization.AtPrime

Mathlib/RingTheory/Localization/AtPrime/Extension.lean

@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2025 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+import Mathlib.RingTheory.DedekindDomain.Dvr
+
+/-!
+# Primes in an extension of localization at prime
+
+Let `R ⊆ S` be an extension of Dedekind domains and `p` be a prime ideal of `R`. Let `Rₚ` be the
+localization of `R` at the complement of `p` and `Sₚ` the localization of `S` at the (image)
+of the complement of `p`.
+
+In this file, we study the relation between the (nonzero) prime ideals of `Sₚ` and the prime
+ideals of `S` above `p`. In particular, we prove that (under suitable conditions) they are in
+bijection.
+
+# Main definitions and results
+
+- `IsLocalization.AtPrime.mem_primesOver_of_isPrime`: The nonzero prime ideals of `Sₚ` are
+  primes over the maximal ideal of `Rₚ`.
+
+- `IsDedekindDomain.primesOverEquivPrimesOver`: the order-preserving bijection between the primes
+  over `p` in `S` and the primes over the maximal ideal of `Rₚ` in `Sₚ`.
+
+-/
+
+open Algebra IsLocalRing Ideal Localization.AtPrime
+
+variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime]
+  (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ]
+  (Sₚ : Type*) [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ]
+  [Algebra Rₚ Sₚ] (P : Ideal S) [hPp : P.LiesOver p]
+
+namespace IsLocalization.AtPrime
+
+/--
+The nonzero prime ideals of `Sₚ` are prime ideals over the maximal ideal of `Rₚ`.
+See `Localization.AtPrime.primesOverEquivPrimesOver` for the bijection between the prime ideals
+of `Sₚ` over the maximal ideal of `Rₚ` and the primes ideals of `S` above `p`.
+-/
+theorem mem_primesOver_of_isPrime {Q : Ideal Sₚ} [Q.IsMaximal] [Algebra.IsIntegral Rₚ Sₚ] :
+    Q ∈ (maximalIdeal Rₚ).primesOver Sₚ := by
+  refine ⟨inferInstance, ?_⟩
+  rw [liesOver_iff, ← eq_maximalIdeal]
+  exact IsMaximal.under Rₚ Q
+
+theorem liesOver_comap_of_liesOver {T : Type*} [CommRing T] [Algebra R T] [Algebra Rₚ T]
+    [Algebra S T] [IsScalarTower R S T] [IsScalarTower R Rₚ T] (Q : Ideal T)
+    [Q.LiesOver (maximalIdeal Rₚ)] : (comap (algebraMap S T) Q).LiesOver p := by
+  have : Q.LiesOver p := by
+    have : (maximalIdeal Rₚ).LiesOver p := liesOver_maximalIdeal Rₚ p _
+    exact LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p
+  exact comap_liesOver Q p <| IsScalarTower.toAlgHom R S T
+
+variable [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ]
+
+include p in
+theorem liesOver_map_of_liesOver [P.IsPrime] :
+    (P.map (algebraMap S Sₚ)).LiesOver (IsLocalRing.maximalIdeal Rₚ) := by
+  rw [liesOver_iff, eq_comm, ← map_eq_maximalIdeal p, over_def P p]
+  exact under_map_eq_map_under _
+    (over_def P p ▸ map_eq_maximalIdeal p Rₚ ▸ maximalIdeal.isMaximal Rₚ)
+    (isPrime_map_of_liesOver S p Sₚ P).ne_top
+
+end IsLocalization.AtPrime
+namespace IsDedekindDomain
+
+open IsLocalization AtPrime
+
+variable [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [IsDedekindDomain S]
+  [NoZeroSMulDivisors R S]
+
+/--
+For `R ⊆ S` an extension of Dedekind domains and `p` a prime ideal of `R`, the bijection
+between the primes of `S` over `p` and the primes over the maximal ideal of `Rₚ` in `Sₚ` where
+`Rₚ` and `Sₚ` are resp. the localizations of `R` and `S` at the complement of `p`.
+-/
+noncomputable def primesOverEquivPrimesOver (hp : p ≠ ⊥) :
+    p.primesOver S ≃o (maximalIdeal Rₚ).primesOver Sₚ where
+  toFun P := ⟨map (algebraMap S Sₚ) P.1, isPrime_map_of_liesOver S p Sₚ P.1,
+    liesOver_map_of_liesOver p Rₚ Sₚ P.1⟩
+  map_rel_iff' {Q Q'} := by
+    refine ⟨fun h ↦ ?_, fun h ↦ map_mono h⟩
+    have : Q'.1.IsMaximal :=
+      (primesOver.isPrime p Q').isMaximal (ne_bot_of_mem_primesOver hp Q'.prop)
+    simpa [comap_map_of_isMaximal S p] using le_comap_of_map_le h
+  invFun Q := ⟨comap (algebraMap S Sₚ) Q.1, IsPrime.under S Q.1,
+    liesOver_comap_of_liesOver p Rₚ Q.1⟩
+  left_inv P := by
+    have : P.val.IsMaximal := Ring.DimensionLEOne.maximalOfPrime
+        (ne_bot_of_mem_primesOver hp P.prop) (primesOver.isPrime p P)
+    exact SetCoe.ext <| IsLocalization.AtPrime.comap_map_of_isMaximal S p Sₚ P.1
+  right_inv Q := SetCoe.ext <| map_comap (algebraMapSubmonoid S p.primeCompl) Sₚ Q
+
+@[simp]
+theorem primesOverEquivPrimesOver_apply (hp : p ≠ ⊥) (P : p.primesOver S) :
+    primesOverEquivPrimesOver p Rₚ Sₚ hp P = Ideal.map (algebraMap S Sₚ) P := rfl
+
+@[simp]
+theorem primesOverEquivPrimesOver_symm_apply (hp : p ≠ ⊥) (Q : (maximalIdeal Rₚ).primesOver Sₚ) :
+    ((primesOverEquivPrimesOver p Rₚ Sₚ hp).symm Q).1 = Ideal.comap (algebraMap S Sₚ) Q := rfl
+
+end IsDedekindDomain

Mathlib/RingTheory/Trace/Quotient.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Riccardo Brasca
 -/
-
 import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.LocalRing.Quotient
@@ -87,12 +86,6 @@ def equivQuotMaximalIdealOfIsLocalization : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal
     rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
     exact s.prop
 
-lemma IsLocalization.AtPrime.map_eq_maximalIdeal :
-    p.map (algebraMap R Rₚ) = maximalIdeal Rₚ := by
-  convert congr_arg (Ideal.map (algebraMap R Rₚ))
-    (IsLocalization.AtPrime.comap_maximalIdeal Rₚ p).symm
-  rw [map_comap p.primeCompl]
-
 local notation "pS" => Ideal.map (algebraMap R S) p
 local notation "pSₚ" => Ideal.map (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ)