Skip to content

Commit 8ea945b

Browse files
xroblotxroblot
committed
feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization (leanprover-community#27706)
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 prove that the bijection between the (nonzero) prime ideals of `Sₚ` and the prime ideals of `S` above `p` preserves the residual degree and the ramification index.
1 parent 63e9909 commit 8ea945b

3 files changed

Lines changed: 192 additions & 9 deletions

File tree

‎Mathlib/NumberTheory/RamificationInertia/Basic.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Anne Baanen
55
-/
66
module
77

8+
public import Mathlib.Algebra.GroupWithZero.Torsion
89
public import Mathlib.LinearAlgebra.Dimension.DivisionRing
910
public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
1011
public import Mathlib.RingTheory.Finiteness.Quotient
@@ -114,6 +115,10 @@ theorem ramificationIdx_bot : ramificationIdx f ⊥ P = 0 :=
114115
theorem ramificationIdx_of_not_le (h : ¬map f p ≤ P) : ramificationIdx f p P = 0 :=
115116
ramificationIdx_spec (by simp) (by simpa using h)
116117

118+
theorem ramificationIdx_bot' (hp : p ≠ ⊥) (hf : Function.Injective f) :
119+
ramificationIdx f p ⊥ = 0 :=
120+
ramificationIdx_of_not_le <| le_bot_iff.not.mpr <| (map_eq_bot_iff_of_injective hf).not.mpr hp
121+
117122
theorem ramificationIdx_ne_zero {e : ℕ} (he : e ≠ 0) (hle : map f p ≤ P ^ e)
118123
(hnle : ¬map f p ≤ P ^ (e + 1)) : ramificationIdx f p P ≠ 0 := by
119124
rwa [ramificationIdx_spec hle hnle]
@@ -190,6 +195,15 @@ lemma ramificationIdx_eq_one_of_map_localization
190195
· exact hp this
191196
· exact IsLocalization.injective _ hp'
192197

198+
theorem ramificationIdx_map_self_eq_one [IsDedekindDomain S] (h₁ : map f p ≠ ⊤) (h₂ : map f p ≠ ⊥) :
199+
ramificationIdx f p (map f p) = 1 := by
200+
refine ramificationIdx_spec (by simp) fun h ↦ ?_
201+
have : map f p ^ 1 = (map f p) ^ 2 := by
202+
rw [pow_one]
203+
exact le_antisymm h <| pow_le_self two_ne_zero
204+
have := IsMulTorsionFree.pow_right_injective₀ (by rwa [one_eq_top]) h₂ this
205+
simp_all
206+
193207
namespace IsDedekindDomain
194208

195209
variable [IsDedekindDomain S]

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -434,6 +434,24 @@ def equivQuotMaximalIdeal : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ := by
434434
rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
435435
exact s.prop
436436

437+
@[simp]
438+
theorem equivQuotMaximalIdeal_apply_mk (x : R) :
439+
equivQuotMaximalIdeal p Rₚ (Ideal.Quotient.mk _ x) =
440+
(Ideal.Quotient.mk _ (algebraMap R Rₚ x)) := rfl
441+
442+
@[simp]
443+
theorem equivQuotMaximalIdeal_symm_apply_mk (x : R) (s : p.primeCompl) :
444+
(equivQuotMaximalIdeal p Rₚ).symm (Ideal.Quotient.mk _ (IsLocalization.mk' Rₚ x s)) =
445+
(Ideal.Quotient.mk p x) * (Ideal.Quotient.mk p s)⁻¹ := by
446+
have h₁ : Ideal.Quotient.mk p ↑s ≠ 0 := by
447+
simpa [ne_eq, Ideal.Quotient.eq_zero_iff_mem] using Ideal.mem_primeCompl_iff.mp s.prop
448+
have h₂ : equivQuotMaximalIdeal p Rₚ (Ideal.Quotient.mk p ↑s) ≠ 0 := by
449+
rwa [RingEquiv.map_ne_zero_iff]
450+
rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
451+
inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotMaximalIdeal_apply_mk, ← map_mul,
452+
mk'_spec, Ideal.Quotient.mk_algebraMap, equivQuotMaximalIdeal_apply_mk,
453+
Ideal.Quotient.mk_algebraMap]
454+
437455
@[deprecated (since := "2025-11-13")] alias _root_.equivQuotMaximalIdealOfIsLocalization :=
438456
equivQuotMaximalIdeal
439457

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

Lines changed: 160 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Xavier Roblot
55
-/
66
module
77

8-
public import Mathlib.RingTheory.DedekindDomain.Dvr
8+
public import Mathlib.NumberTheory.RamificationInertia.Basic
99

1010
/-!
1111
# Primes in an extension of localization at prime
@@ -16,15 +16,24 @@ of the complement of `p`.
1616
1717
In this file, we study the relation between the (nonzero) prime ideals of `Sₚ` and the prime
1818
ideals of `S` above `p`. In particular, we prove that (under suitable conditions) they are in
19-
bijection.
19+
bijection and that the residual degree and ramification index are preserved by this bijection.
2020
2121
## Main definitions and results
2222
2323
- `IsLocalization.AtPrime.mem_primesOver_of_isPrime`: The nonzero prime ideals of `Sₚ` are
2424
primes over the maximal ideal of `Rₚ`.
2525
26-
- `IsDedekindDomain.primesOverEquivPrimesOver`: the order-preserving bijection between the primes
27-
over `p` in `S` and the primes over the maximal ideal of `Rₚ` in `Sₚ`.
26+
- `IsLocalization.AtPrime.equivQuotientMapOfIsMaximal`: `S ⧸ P ≃+* Sₚ ⧸ P·Sₚ` where
27+
`P` is a maximal ideal of `S` above `p`.
28+
29+
- `IsDedekindDomain.primesOverEquivPrimesOver`: the bijection between the primes over
30+
`p` in `S` and the primes over the maximal ideal of `Rₚ` in `Sₚ`.
31+
32+
- `IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq`: the bijection
33+
`primesOverEquivPrimesOver` preserves the inertia degree.
34+
35+
- `IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq`: the bijection
36+
`primesOverEquivPrimesOver` preserves the ramification index.
2837
2938
-/
3039

@@ -58,23 +67,148 @@ theorem liesOver_comap_of_liesOver {T : Type*} [CommRing T] [Algebra R T] [Algeb
5867
exact LiesOver.trans Q (IsLocalRing.maximalIdeal Rₚ) p
5968
exact comap_liesOver Q p <| IsScalarTower.toAlgHom R S T
6069

61-
variable [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ]
62-
6370
include p in
64-
theorem liesOver_map_of_liesOver [P.IsPrime] :
71+
theorem liesOver_map_of_liesOver [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ]
72+
[P.IsPrime] :
6573
(P.map (algebraMap S Sₚ)).LiesOver (IsLocalRing.maximalIdeal Rₚ) := by
6674
rw [liesOver_iff, eq_comm, ← map_eq_maximalIdeal p, over_def P p]
6775
exact under_map_eq_map_under _
6876
(over_def P p ▸ map_eq_maximalIdeal p Rₚ ▸ maximalIdeal.isMaximal Rₚ)
6977
(isPrime_map_of_liesOver S p Sₚ P).ne_top
7078

79+
attribute [local instance] Ideal.Quotient.field
80+
81+
include p in
82+
theorem exists_algebraMap_quot_eq_of_mem_quot [P.IsMaximal]
83+
(x : Sₚ ⧸ P.map (algebraMap S Sₚ)) :
84+
∃ a, (algebraMap S (Sₚ ⧸ P.map (algebraMap S Sₚ))) a = x := by
85+
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
86+
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (algebraMapSubmonoid S p.primeCompl) x
87+
obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := P) (Ideal.Quotient.mk P s)⁻¹
88+
simp only [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), Quotient.algebraMap_eq, RingHom.comp_apply]
89+
use x * s'
90+
rw [← sub_eq_zero, ← map_sub, Quotient.eq_zero_iff_mem]
91+
have h₀ : (P.map (algebraMap S Sₚ)).IsPrime := isPrime_map_of_liesOver S p Sₚ P
92+
have h₁ : s.1 ∉ P := (Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.prop
93+
have h₂ : algebraMap S Sₚ s ∉ Ideal.map (algebraMap S Sₚ) P := by
94+
rwa [← mem_comap, comap_map_eq_self_of_isMaximal _ h₀.ne_top]
95+
refine (h₀.mem_or_mem ?_).resolve_left h₂
96+
rw [mul_sub, mul_mk'_eq_mk'_of_mul, mk'_mul_cancel_left, ← map_mul, ← map_sub, ← mem_comap,
97+
comap_map_eq_self_of_isMaximal _ IsPrime.ne_top', ← Ideal.Quotient.eq, map_mul, map_mul, hs,
98+
mul_comm, inv_mul_cancel_right₀ (Quotient.eq_zero_iff_mem.not.mpr h₁)]
99+
100+
/--
101+
The isomorphism `S ⧸ P ≃+* Sₚ ⧸ P·Sₚ`, where `Sₚ` is the localization of `S` at the (image) of
102+
the complement of `p` and `P` is a maximal ideal of `S` above `p`.
103+
Note that this isomorphism makes the obvious diagram involving `R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ`
104+
commute, see `IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply`.
105+
-/
106+
noncomputable def equivQuotientMapOfIsMaximal [p.IsPrime] [P.IsMaximal] :
107+
S ⧸ P ≃+* Sₚ ⧸ P.map (algebraMap S Sₚ) :=
108+
(Ideal.quotEquivOfEq (by
109+
rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ _), ← RingHom.comap_ker, Quotient.algebraMap_eq,
110+
mk_ker,
111+
comap_map_eq_self_of_isMaximal _ (isPrime_map_of_liesOver S p Sₚ P).ne_top])).trans
112+
(RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ _))
113+
fun x ↦ exists_algebraMap_quot_eq_of_mem_quot p Sₚ P x)
114+
115+
@[simp]
116+
theorem equivQuotientMapOfIsMaximal_apply_mk [P.IsMaximal] (x : S) :
117+
equivQuotientMapOfIsMaximal p Sₚ P (Ideal.Quotient.mk _ x) =
118+
(Ideal.Quotient.mk _ (algebraMap S Sₚ x)) := rfl
119+
120+
@[simp]
121+
theorem equivQuotientMapOfIsMaximal_symm_apply_mk [P.IsMaximal] (x : S)
122+
(s : algebraMapSubmonoid S p.primeCompl) :
123+
(equivQuotientMapOfIsMaximal p Sₚ P).symm (Ideal.Quotient.mk _ (mk' _ x s)) =
124+
(Ideal.Quotient.mk _ x) * (Ideal.Quotient.mk _ s.val)⁻¹ := by
125+
have : (Ideal.map (algebraMap S Sₚ) P).IsPrime := isPrime_map_of_liesOver S p Sₚ P
126+
have h₁ : Ideal.Quotient.mk P ↑s ≠ 0 :=
127+
Quotient.eq_zero_iff_mem.not.mpr <|
128+
(Set.disjoint_left.mp <| disjoint_primeCompl_of_liesOver P p) s.prop
129+
have h₂ : equivQuotientMapOfIsMaximal p Sₚ P (Ideal.Quotient.mk P ↑s) ≠ 0 := by
130+
rwa [RingEquiv.map_ne_zero_iff]
131+
rw [RingEquiv.symm_apply_eq, ← mul_left_inj' h₂, map_mul, mul_assoc, ← map_mul,
132+
inv_mul_cancel₀ h₁, map_one, mul_one, equivQuotientMapOfIsMaximal_apply_mk,
133+
← map_mul, mk'_spec, Quotient.mk_algebraMap, equivQuotientMapOfIsMaximal_apply_mk,
134+
Quotient.mk_algebraMap]
135+
136+
variable [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ]
137+
138+
/--
139+
The following diagram where the vertical maps are the algebra maps and the horizontal maps are
140+
`Localization.AtPrime.equivQuotMaximalIdeal.symm` and
141+
`Localization.AtPrime.equivQuotientMapOfIsMaximal.symm` commutes:
142+
```
143+
Rₚ ⧸ 𝓂 ──▶ R ⧸ p
144+
│ │
145+
Sₚ ⧸ 𝒫 ──▶ S ⧸ P
146+
```
147+
Here, `𝓂` denotes the maximal ideal of `Rₚ` and `𝒫` the image of `P` in `Sₚ`.
148+
Note that result is stated in that direction since this is the formulation needed for the proof
149+
of `Localization.AtPrime.inertiaDeg_map_eq_inertiaDeg`.
150+
-/
151+
theorem algebraMap_equivQuotMaximalIdeal_symm_apply [p.IsMaximal] [P.IsMaximal]
152+
[(P.map (algebraMap S Sₚ)).LiesOver (maximalIdeal Rₚ)] (x : Rₚ ⧸ maximalIdeal Rₚ) :
153+
algebraMap (R ⧸ p) (S ⧸ P) ((equivQuotMaximalIdeal p Rₚ).symm x) =
154+
(equivQuotientMapOfIsMaximal p Sₚ P).symm
155+
(algebraMap (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ P.map (algebraMap S Sₚ)) x) := by
156+
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
157+
obtain ⟨x, s, rfl⟩ := mk'_surjective p.primeCompl x
158+
simp [equivQuotMaximalIdeal_symm_apply_mk, map_mul, Quotient.algebraMap_mk_of_liesOver,
159+
IsLocalization.algebraMap_mk' S Rₚ Sₚ]
160+
161+
-- Lean thinks that the instance [p.IsPrime] is not necessary here, but it is needed
162+
-- for the definition of `Rₚ`.
163+
set_option linter.unusedSectionVars false in
164+
@[simp]
165+
theorem equivQuotientMapMaximalIdeal_apply_mk [p.IsMaximal] (x : S) :
166+
equivQuotientMapMaximalIdeal S p Rₚ Sₚ (Ideal.Quotient.mk _ x) =
167+
(Ideal.Quotient.mk _ (algebraMap S Sₚ x)) := rfl
168+
169+
theorem inertiaDeg_map_eq_inertiaDeg [p.IsMaximal] [P.IsMaximal]
170+
[(Ideal.map (algebraMap S Sₚ) P).LiesOver (maximalIdeal Rₚ)] :
171+
(maximalIdeal Rₚ).inertiaDeg (P.map (algebraMap S Sₚ)) = p.inertiaDeg P := by
172+
rw [inertiaDeg_algebraMap, inertiaDeg_algebraMap]
173+
refine Algebra.finrank_eq_of_equiv_equiv (equivQuotMaximalIdeal p Rₚ).symm
174+
(equivQuotientMapOfIsMaximal p Sₚ P).symm ?_
175+
ext x
176+
exact algebraMap_equivQuotMaximalIdeal_symm_apply p Rₚ Sₚ P x
177+
178+
theorem ramificationIdx_map_eq_ramificationIdx [NoZeroSMulDivisors R S] [NoZeroSMulDivisors R Rₚ]
179+
[NoZeroSMulDivisors R Sₚ] [NoZeroSMulDivisors S Sₚ] [NoZeroSMulDivisors Rₚ Sₚ]
180+
[IsDedekindDomain S] [IsDedekindDomain Rₚ] [IsDedekindDomain Sₚ] (hp : p ≠ ⊥) [P.IsPrime] :
181+
(maximalIdeal Rₚ).ramificationIdx (algebraMap Rₚ Sₚ) (P.map (algebraMap S Sₚ)) =
182+
p.ramificationIdx (algebraMap R S) P := by
183+
have h₁ : maximalIdeal Rₚ ≠ ⊥ := by
184+
rw [← map_eq_maximalIdeal p]
185+
exact map_ne_bot_of_ne_bot hp
186+
have : (P.map (algebraMap S Sₚ)).IsPrime := isPrime_map_of_liesOver S p Sₚ P
187+
by_cases hP : P = ⊥
188+
· simp_rw [hP, Ideal.map_bot, ramificationIdx_bot' hp
189+
(FaithfulSMul.algebraMap_injective _ _),
190+
ramificationIdx_bot' h₁ (FaithfulSMul.algebraMap_injective Rₚ Sₚ)]
191+
have h₂ : Ideal.map (algebraMap Rₚ Sₚ) (maximalIdeal Rₚ) ≤ P.map (algebraMap S Sₚ) := by
192+
rw [map_le_iff_le_comap]
193+
exact le_of_eq <| (liesOver_iff _ _).mp <| liesOver_map_of_liesOver p Rₚ Sₚ P
194+
have h_main := (ramificationIdx_algebra_tower
195+
(map_ne_bot_of_ne_bot h₁) (map_ne_bot_of_ne_bot hp) h₂).symm.trans
196+
(ramificationIdx_algebra_tower (map_ne_bot_of_ne_bot hP)
197+
(map_ne_bot_of_ne_bot hp) le_rfl)
198+
rwa [ramificationIdx_map_self_eq_one IsPrime.ne_top' (map_ne_bot_of_ne_bot hP), mul_one,
199+
← map_eq_maximalIdeal p, ramificationIdx_map_self_eq_one _ (map_ne_bot_of_ne_bot hp), one_mul,
200+
map_eq_maximalIdeal p] at h_main
201+
rw [map_eq_maximalIdeal]
202+
exact IsPrime.ne_top'
203+
71204
end IsLocalization.AtPrime
205+
72206
namespace IsDedekindDomain
73207

74208
open IsLocalization AtPrime
75209

76-
variable [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [IsDedekindDomain S]
77-
[NoZeroSMulDivisors R S]
210+
variable [IsDedekindDomain S] [NoZeroSMulDivisors R S] [Algebra R Sₚ] [IsScalarTower R S Sₚ]
211+
[IsScalarTower R Rₚ Sₚ]
78212

79213
/--
80214
For `R ⊆ S` an extension of Dedekind domains and `p` a prime ideal of `R`, the bijection
@@ -106,4 +240,21 @@ theorem primesOverEquivPrimesOver_apply (hp : p ≠ ⊥) (P : p.primesOver S) :
106240
theorem primesOverEquivPrimesOver_symm_apply (hp : p ≠ ⊥) (Q : (maximalIdeal Rₚ).primesOver Sₚ) :
107241
((primesOverEquivPrimesOver p Rₚ Sₚ hp).symm Q).1 = Ideal.comap (algebraMap S Sₚ) Q := rfl
108242

243+
theorem primesOverEquivPrimesOver_inertiagDeg_eq [p.IsMaximal] (hp : p ≠ ⊥) (P : p.primesOver S) :
244+
(maximalIdeal Rₚ).inertiaDeg (primesOverEquivPrimesOver p Rₚ Sₚ hp P : Ideal Sₚ) =
245+
p.inertiaDeg P.val := by
246+
have : NeZero p := ⟨hp⟩
247+
have : P.val.IsMaximal := Ring.DimensionLEOne.maximalOfPrime
248+
(ne_bot_of_mem_primesOver (NeZero.ne _) P.prop) inferInstance
249+
have : (P.1.map (algebraMap S Sₚ)).LiesOver (maximalIdeal Rₚ) := liesOver_map_of_liesOver p _ _ _
250+
exact inertiaDeg_map_eq_inertiaDeg p _ _ _
251+
252+
theorem primesOverEquivPrimesOver_ramificationIdx_eq (hp : p ≠ ⊥) [NoZeroSMulDivisors R Rₚ]
253+
[NoZeroSMulDivisors R Sₚ] [NoZeroSMulDivisors S Sₚ] [NoZeroSMulDivisors Rₚ Sₚ]
254+
[IsDedekindDomain Rₚ] [IsDedekindDomain Sₚ] (P : p.primesOver S) :
255+
(maximalIdeal Rₚ).ramificationIdx (algebraMap Rₚ Sₚ)
256+
(primesOverEquivPrimesOver p Rₚ Sₚ hp P : Ideal Sₚ) =
257+
p.ramificationIdx (algebraMap R S) P.val :=
258+
ramificationIdx_map_eq_ramificationIdx p _ _ _ hp
259+
109260
end IsDedekindDomain

0 commit comments

Comments
 (0)