CyclotomicPrimeCoverage.lean

1 import PaperX.ProfiniteSeparation
2 import Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
3 import Mathlib.NumberTheory.LSeries.PrimesInAP
4 
5 /-! Actual prime coverage of the cyclotomic Galois group, with any fixed finite
6 set of rational primes removed. The arithmetic prime-existence input is Mathlib's
7 proved Dirichlet theorem, not a supplied coverage predicate. The sample is an
8 actual automorphism of the cyclotomic number field. Its membership in the
9 decomposition group and its p-power action on the residue field are proved
10 below, giving the arithmetic Frobenius convention explicitly. -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperX.CyclotomicPrimeCoverage
14 open NumberField
15 
16 variable (n : ℕ) [NeZero n]
17 
18 /-- A rational prime coprime to the conductor, outside the prescribed finite set. -/
19 def PermittedPrime (forbidden : Finset ℕ) :=
20   {p : ℕ // p.Prime ∧ p.Coprime n ∧ p ∉ forbidden}
21 
22 /-- The actual residue of a permitted prime in the group of units. -/
23 def primeResidue (forbidden : Finset ℕ) (p : PermittedPrime n forbidden) : (ZMod n)ˣ :=
24   ZMod.unitOfCoprime p.val p.property.2.1
25 
26 /-- Dirichlet's theorem allows every unit residue while avoiding any finite set
27 and retaining an arbitrary strict lower bound. -/
28 theorem exists_prime_with_residue (forbidden : Finset ℕ) (u : (ZMod n)ˣ) (B : ℕ) :
29     ∃ p : PermittedPrime n forbidden, B < p.val ∧ primeResidue n forbidden p = u := by
30   classical
31   obtain ⟨p, hpgt, hp, hres⟩ := Nat.forall_exists_prime_gt_and_eq_mod u.isUnit
32     (max B (forbidden.sup id))
33   have hc : p.Coprime n := (ZMod.isUnit_iff_coprime p n).mp (hres ▸ u.isUnit)
34   have hn : p ∉ forbidden := by
35     intro hm
36     have hle : p ≤ forbidden.sup id := Finset.le_sup (f := id) hm
37     exact (not_lt_of_ge (hle.trans (le_max_right _ _))) hpgt
38   refine ⟨⟨p, hp, hc, hn⟩, (le_max_left _ _).trans_lt hpgt, ?_⟩
39   apply Units.ext
40   exact hres
41 
42 theorem primeResidue_surjective (forbidden : Finset ℕ) :
43     Function.Surjective (primeResidue n forbidden) := by
44   intro u
45   obtain ⟨p, _, hp⟩ := exists_prime_with_residue n forbidden u 0
46   exact ⟨p, hp⟩
47 
48 variable (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K]
49 
50 /-- The actual cyclotomic automorphism whose root-of-unity exponent is p. -/
51 def primePowerAutomorphism (p : ℕ) (hp : p.Coprime n) : Gal(K/ℚ) :=
52   (IsCyclotomicExtension.Rat.galEquivZMod n K).symm (ZMod.unitOfCoprime p hp)
53 
54 /-- Prime-indexed automorphisms of the actual cyclotomic number field. -/
55 def primeSample (forbidden : Finset ℕ) (p : PermittedPrime n forbidden) : Gal(K/ℚ) :=
56   primePowerAutomorphism n K p.val p.property.2.1
57 
58 @[simp] theorem galEquiv_primePowerAutomorphism (p : ℕ) (hp : p.Coprime n) :
59     IsCyclotomicExtension.Rat.galEquivZMod n K (primePowerAutomorphism n K p hp) =
60       ZMod.unitOfCoprime p hp := by
61   exact (IsCyclotomicExtension.Rat.galEquivZMod n K).apply_symm_apply _
62 
63 /-- This is a theorem about actual field elements, not a name assigned to the sample. -/
64 theorem primePowerAutomorphism_apply (p : ℕ) (hp : p.Coprime n)
65     {x : K} (hx : x ^ n = 1) : primePowerAutomorphism n K p hp x = x ^ p := by
66   rw [IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq n K _ hx,
67     galEquiv_primePowerAutomorphism, ZMod.coe_unitOfCoprime]
68   apply pow_eq_pow_of_modEq _ hx
69   apply (ZMod.natCast_eq_natCast_iff _ _ n).mp
70   simp
71 
72 /-- Every actual cyclotomic automorphism is represented by a permitted prime,
73 even after imposing an arbitrary lower bound. -/
74 theorem exists_prime_with_automorphism (forbidden : Finset ℕ) (σ : Gal(K/ℚ)) (B : ℕ) :
75     ∃ p : PermittedPrime n forbidden, B < p.val ∧ primeSample n K forbidden p = σ := by
76   obtain ⟨p, hB, hp⟩ := exists_prime_with_residue n forbidden
77     (IsCyclotomicExtension.Rat.galEquivZMod n K σ) B
78   refine ⟨p, hB, ?_⟩
79   apply (IsCyclotomicExtension.Rat.galEquivZMod n K).injective
80   rw [primeSample, galEquiv_primePowerAutomorphism]
81   exact hp
82 
83 theorem primeSample_surjective (forbidden : Finset ℕ) :
84     Function.Surjective (primeSample n K forbidden) := by
85   intro σ
86   obtain ⟨p, _, hp⟩ := exists_prime_with_automorphism n K forbidden σ 0
87   exact ⟨p, hp⟩
88 
89 /-- All open normal quotient classes are covered. This is derived from actual
90 prime surjectivity for this fixed cyclotomic extension. -/
91 theorem primeSample_quotientCoverage (forbidden : Finset ℕ) :
92     PaperX.ProfiniteSeparation.QuotientCoverage (primeSample n K forbidden) := by
93   intro H σ
94   obtain ⟨p, hp⟩ := primeSample_surjective n K forbidden σ
95   refine ⟨p, 1, ?_⟩
96   simp [hp]
97 
98 section Residue
99 open scoped Pointwise
100 variable (p : ℕ) [Fact (Nat.Prime p)] (P : Ideal (𝓞 K)) [P.IsMaximal]
101   [P.LiesOver (Ideal.span {(p : ℤ)})] (hp : p.Coprime n)
102 attribute [local instance] Ideal.Quotient.field
103 
104 /-- The sampled automorphism belongs to the actual decomposition group at every
105 prime of the cyclotomic field above p. -/
106 theorem primePowerAutomorphism_mem_stabilizer :
107     primePowerAutomorphism n K p hp ∈ MulAction.stabilizer Gal(K/ℚ) P := by
108   have hmem : ZMod.unitOfCoprime p hp ∈
109       (IsCyclotomicExtension.Rat.galEquivZMod n K).mapSubgroup
110         (MulAction.stabilizer Gal(K/ℚ) P) := by
111     rw [IsCyclotomicExtension.Rat.galEquivZMod_stabilizer n K p P hp]
112     exact Subgroup.mem_zpowers _
113   exact Subgroup.mem_map_equiv.mp hmem
114 
115 /-- The arithmetic Frobenius condition is proved on every integral element:
116 reduction of the sampled action equals the p-power residue-field action. -/
117 theorem primePowerAutomorphism_residue (x : 𝓞 K) :
118     Ideal.Quotient.mk P (primePowerAutomorphism n K p hp • x) =
119       (Ideal.Quotient.mk P x) ^ p := by
120   have : CharP (ℤ ⧸ Ideal.span {(p : ℤ)}) p := ringChar.of_eq <| Int.ringChar_idealQuot p
121   have : CharP (𝓞 K ⧸ P) p :=
122     charP_of_injective_algebraMap
123       (algebraMap (ℤ ⧸ Ideal.span {(p : ℤ)}) (𝓞 K ⧸ P)).injective p
124   let σ := primePowerAutomorphism n K p hp
125   let f := ((Ideal.Quotient.mk P).comp
126     (MulSemiringAction.toRingHom Gal(K/ℚ) (𝓞 K) σ)).toIntAlgHom
127   let g := ((frobenius (𝓞 K ⧸ P) p).comp (Ideal.Quotient.mk P)).toIntAlgHom
128   have hζ := IsCyclotomicExtension.zeta_spec n ℚ K
129   have hfg : f = g := by
130     apply AlgHom.ext_of_adjoin_eq_top
131       (IsCyclotomicExtension.Rat.adjoin_singleton_eq_top hζ)
132     intro z hz
133     have hz' : z = hζ.toInteger := Set.mem_singleton_iff.mp hz
134     subst z
135     change Ideal.Quotient.mk P (σ • hζ.toInteger) =
136       (Ideal.Quotient.mk P hζ.toInteger) ^ p
137     rw [IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq n K σ
138       hζ.toInteger_isPrimitiveRoot.pow_eq_one]
139     simp only [σ, galEquiv_primePowerAutomorphism, ZMod.coe_unitOfCoprime,
140       ZMod.val_natCast, map_pow]
141     exact (pow_eq_pow_mod p
142       (by simp [← map_pow, hζ.toInteger_isPrimitiveRoot.pow_eq_one])).symm
143   exact DFunLike.congr_fun hfg x
144 
145 /-- Both defining properties of arithmetic Frobenius are obtained for the
146 actual prime and its actual residue field. -/
147 theorem primePowerAutomorphism_arithmeticFrobenius :
148     primePowerAutomorphism n K p hp ∈ MulAction.stabilizer Gal(K/ℚ) P ∧
149       ∀ x : 𝓞 K, Ideal.Quotient.mk P (primePowerAutomorphism n K p hp • x) =
150         (Ideal.Quotient.mk P x) ^ p :=
151   ⟨primePowerAutomorphism_mem_stabilizer n K p P hp,
152     primePowerAutomorphism_residue n K p P hp⟩
153 /-- The actual arithmetic prime is unramified in the cyclotomic extension. -/
154 theorem permitted_prime_ramificationIdx (hcop : p.Coprime n) :
155     Ideal.ramificationIdx P ℤ = 1 :=
156   IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd p K P
157     ((Nat.Prime.coprime_iff_not_dvd (Fact.out : p.Prime)).mp hcop)
158 
159 /-- Unramifiedness and the arithmetic Frobenius action are proved together. -/
160 theorem primePowerAutomorphism_unramified_arithmeticFrobenius :
161     Ideal.ramificationIdx P ℤ = 1 ∧
162       primePowerAutomorphism n K p hp ∈ MulAction.stabilizer Gal(K/ℚ) P ∧
163       ∀ x : 𝓞 K, Ideal.Quotient.mk P (primePowerAutomorphism n K p hp • x) =
164         (Ideal.Quotient.mk P x) ^ p :=
165   ⟨permitted_prime_ramificationIdx n K p P hp,
166     primePowerAutomorphism_arithmeticFrobenius n K p P hp⟩
167 end Residue
168 
169 end PaperX.CyclotomicPrimeCoverage

Back to source controls