UnramifiedFrobeniusUniqueness.lean

1 import Mathlib.NumberTheory.NumberField.Discriminant.Different
2 import Mathlib.NumberTheory.RamificationInertia.Galois
3 import Mathlib.NumberTheory.NumberField.Basic
4 import Mathlib.RingTheory.Ideal.Int
5 import Mathlib.FieldTheory.Galois.IsGaloisGroup
6 
7 /-! Genuine unramifiedness in a finite normal number field implies trivial
8 inertia and uniqueness of the arithmetic Frobenius action at a chosen prime.
9 The arithmetic hypothesis is ramification index one, not a renamed assertion
10 that inertia acts trivially. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperX.UnramifiedFrobeniusUniqueness
14 open NumberField
15 open scoped Pointwise
16 
17 variable (L : Type*) [Field L] [NumberField L] [Normal ℚ L]
18   (p : ℕ) [hp : Fact p.Prime]
19   (P : Ideal (𝓞 L)) [P.IsMaximal] [P.LiesOver (Ideal.span {(p : ℤ)})]
20 
21 include p hp in
22 /-- The cardinality of the actual inertia subgroup is the actual ramification
23 index over the integers. -/
24 theorem inertia_card_eq_ramificationIdx :
25     Nat.card (P.inertia Gal(L/ℚ)) = Ideal.ramificationIdx P ℤ := by
26   let : (Ideal.span {(p : ℤ)}).IsMaximal := Int.ideal_span_isMaximal_of_prime p
27   let : IsGalois ℚ L := { }
28   let : IsGaloisGroup Gal(L/ℚ) ℤ (𝓞 L) :=
29     IsGaloisGroup.of_isFractionRing Gal(L/ℚ) ℤ (𝓞 L) ℚ L
30   rw [Ideal.card_inertia_eq_ramificationIdxIn (Ideal.span {(p : ℤ)}) P,
31     Ideal.ramificationIdxIn_eq_ramificationIdx (Ideal.span {(p : ℤ)}) P Gal(L/ℚ)]
32 
33 include p hp in
34 /-- An unramified prime has trivial actual inertia. -/
35 theorem inertia_eq_bot (he : Ideal.ramificationIdx P ℤ = 1) :
36     P.inertia Gal(L/ℚ) = ⊥ := by
37   have hc : Nat.card (P.inertia Gal(L/ℚ)) = 1 :=
38     (inertia_card_eq_ramificationIdx L p P).trans he
39   exact (Subgroup.eq_bot_iff_card _).mpr hc
40 
41 include p hp in
42 /-- The commutative-algebra notion of unramifiedness gives the same conclusion. -/
43 theorem inertia_eq_bot_of_isUnramifiedAt [Algebra.IsUnramifiedAt ℤ P] :
44     P.inertia Gal(L/ℚ) = ⊥ := by
45   exact inertia_eq_bot L p P (Ideal.ramificationIdx_eq_one P ℤ)
46 
47 include hp in
48 /-- Unramifiedness makes the action of the decomposition group on the actual
49 residue extension faithful. -/
50 theorem stabilizerHom_injective (he : Ideal.ramificationIdx P ℤ = 1) :
51     Function.Injective (Ideal.Quotient.stabilizerHom P (Ideal.span {(p : ℤ)}) Gal(L/ℚ)) := by
52   apply (MonoidHom.ker_eq_bot_iff _).mp
53   rw [Ideal.Quotient.ker_stabilizerHom]
54   apply le_antisymm ?_ bot_le
55   intro σ hσ
56   apply Subgroup.mem_bot.mpr
57   apply Subtype.ext
58   apply Subgroup.mem_bot.mp
59   rw [← inertia_eq_bot L p P he]
60   exact Ideal.coe_mem_inertia.mpr hσ
61 
62 include p hp in
63 /-- Two stabilizing automorphisms with the same actual residue action coincide
64 at an unramified prime. -/
65 theorem eq_of_residue_eq (he : Ideal.ramificationIdx P ℤ = 1)
66     (σ τ : Gal(L/ℚ))
67     (hσ : σ ∈ MulAction.stabilizer Gal(L/ℚ) P)
68     (hτ : τ ∈ MulAction.stabilizer Gal(L/ℚ) P)
69     (hres : ∀ x : 𝓞 L, Ideal.Quotient.mk P (σ • x) = Ideal.Quotient.mk P (τ • x)) :
70     σ = τ := by
71   apply congrArg Subtype.val
72     (stabilizerHom_injective L p P he (a₁ := ⟨σ, hσ⟩) (a₂ := ⟨τ, hτ⟩) ?_)
73   apply AlgEquiv.ext
74   intro z
75   obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective z
76   exact hres x
77 
78 /-- Arithmetic Frobenius at a fixed unramified prime is unique as an actual
79 field automorphism, with the p-power residue convention. -/
80 theorem arithmeticFrobenius_unique (he : Ideal.ramificationIdx P ℤ = 1)
81     (σ τ : Gal(L/ℚ))
82     (hσ : σ ∈ MulAction.stabilizer Gal(L/ℚ) P)
83     (hτ : τ ∈ MulAction.stabilizer Gal(L/ℚ) P)
84     (hσp : ∀ x : 𝓞 L, Ideal.Quotient.mk P (σ • x) = (Ideal.Quotient.mk P x) ^ p)
85     (hτp : ∀ x : 𝓞 L, Ideal.Quotient.mk P (τ • x) = (Ideal.Quotient.mk P x) ^ p) :
86     σ = τ := by
87   exact eq_of_residue_eq L p P he σ τ hσ hτ (fun x => (hσp x).trans (hτp x).symm)
88 
89 /-- A fixed finite set of rational primes, computed from the nonzero field
90 discriminant, contains every prime that ramifies in this number field. -/
91 def discriminantPrimes : Finset ℕ := (NumberField.discr L).natAbs.primeFactors
92 
93 omit [Normal ℚ L] in
94 /-- Outside the discriminant primes, the rational prime does not divide the
95 integer discriminant. -/
96 theorem not_dvd_discr_of_not_mem (h : p ∉ discriminantPrimes L) :
97     ¬ (p : ℤ) ∣ NumberField.discr L := by
98   intro hd
99   exact h (Nat.mem_primeFactors.mpr ⟨hp.out, Int.natCast_dvd.mp hd,
100     Int.natAbs_ne_zero.mpr (NumberField.discr_ne_zero L)⟩)
101 
102 omit [Normal ℚ L] in
103 /-- Discriminant nondivisibility supplies actual local unramifiedness. -/
104 theorem isUnramifiedAt_of_not_dvd_discr (hd : ¬ (p : ℤ) ∣ NumberField.discr L) :
105     Algebra.IsUnramifiedAt ℤ P := by
106   exact (NumberField.not_dvd_discr_iff_forall_liesOver L (𝓞 L)
107     (Int.prime_iff_natAbs_prime.mpr (by simpa using hp.out))).mp hd P inferInstance inferInstance
108 
109 omit [Normal ℚ L] in
110 /-- Every prime above a rational prime outside this fixed finite set is
111 unramified in the commutative-algebra sense. -/
112 theorem isUnramifiedAt_of_not_mem (h : p ∉ discriminantPrimes L) :
113     Algebra.IsUnramifiedAt ℤ P :=
114   isUnramifiedAt_of_not_dvd_discr L p P (not_dvd_discr_of_not_mem L p h)
115 
116 /-- The same explicit finite set controls the actual inertia subgroups. -/
117 theorem inertia_eq_bot_of_not_mem (h : p ∉ discriminantPrimes L) :
118     P.inertia Gal(L/ℚ) = ⊥ := by
119   let : Algebra.IsUnramifiedAt ℤ P := isUnramifiedAt_of_not_mem L p P h
120   exact inertia_eq_bot_of_isUnramifiedAt L p P
121 
122 /-- Outside the explicit discriminant set, arithmetic Frobenius at any chosen
123 prime above p is unique among actual stabilizing field automorphisms. -/
124 theorem arithmeticFrobenius_unique_of_not_mem (h : p ∉ discriminantPrimes L)
125     (σ τ : Gal(L/ℚ))
126     (hσ : σ ∈ MulAction.stabilizer Gal(L/ℚ) P)
127     (hτ : τ ∈ MulAction.stabilizer Gal(L/ℚ) P)
128     (hσp : ∀ x : 𝓞 L, Ideal.Quotient.mk P (σ • x) = (Ideal.Quotient.mk P x) ^ p)
129     (hτp : ∀ x : 𝓞 L, Ideal.Quotient.mk P (τ • x) = (Ideal.Quotient.mk P x) ^ p) :
130     σ = τ := by
131   let : Algebra.IsUnramifiedAt ℤ P := isUnramifiedAt_of_not_mem L p P h
132   exact arithmeticFrobenius_unique L p P (Ideal.ramificationIdx_eq_one P ℤ)
133     σ τ hσ hτ hσp hτp
134 
135 omit [Normal ℚ L] in
136 /-- Only finitely many rational primes admit a ramified prime above them. -/
137 theorem finite_ramified_primes :
138     Set.Finite {q : ℕ | q.Prime ∧ ∃ Q : Ideal (𝓞 L), Q.IsMaximal ∧
139       Q.LiesOver (Ideal.span {(q : ℤ)}) ∧ Ideal.ramificationIdx Q ℤ ≠ 1} := by
140   apply (discriminantPrimes L).finite_toSet.subset
141   intro q hq
142   rcases hq with ⟨hq, Q, hQ, hQP, hram⟩
143   let : Fact q.Prime := ⟨hq⟩
144   let : Q.IsMaximal := hQ
145   let : Q.LiesOver (Ideal.span {(q : ℤ)}) := hQP
146   by_contra h
147   let : Algebra.IsUnramifiedAt ℤ Q := isUnramifiedAt_of_not_mem L q Q h
148   exact hram (Ideal.ramificationIdx_eq_one Q ℤ)
149 
150 end PaperX.UnramifiedFrobeniusUniqueness

Back to source controls