CyclotomicIntegralFrobenius.lean

1 import PaperX.CyclotomicAbsoluteSamples
2 import Mathlib.RingTheory.IntegralClosure.Algebra.Basic
3 import Mathlib.Tactic
4 
5 /-! Arithmetic Frobenius recognition in the actual integral closure of the
6 integers in the algebraic closure of the rationals. Reduction is injective on
7 roots of order prime to the residue characteristic. The ideal inertia subgroup
8 therefore acts trivially on the corresponding cyclotomic field. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.CyclotomicIntegralFrobenius
12 open NumberField PaperX.CyclotomicAbsoluteSamples
13 open scoped Pointwise
14 
15 section Roots
16 variable {R S : Type*} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S]
17 
18 /-- Any ring homomorphism is injective on roots whose order remains nonzero in
19 the target domain. The ambient homomorphism need not be injective. -/
20 theorem map_injective_on_roots (f : R →+* S) (n : ℕ) [NeZero n] (hn : (n : S) ≠ 0)
21     {x y : R} (hx : x ^ n = 1) (hy : y ^ n = 1) (hres : f x = f y) : x = y := by
22   let s : R := ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
23   have hp : s * (x - y) = 0 := by
24     rw [show s = ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) from rfl,
25       geom_sum₂_mul, hx, hy, sub_self]
26   have hry : f y ≠ 0 := by
27     intro hz
28     have h := congrArg f hy
29     simp [hz, NeZero.ne n] at h
30   have hrs : f s = (n : S) * (f y) ^ (n - 1) := by
31     simp only [s, map_sum, map_mul, map_pow, hres]
32     rw [show (∑ i ∈ Finset.range n, f y ^ i * f y ^ (n - 1 - i)) =
33       ∑ _i ∈ Finset.range n, f y ^ (n - 1) from ?_]
34     simp
35     apply Finset.sum_congr rfl
36     intro i hi
37     rw [← pow_add]
38     congr 1
39     have hi' := Finset.mem_range.mp hi
40     omega
41   have hs : s ≠ 0 := by
42     intro hz
43     have h := mul_ne_zero hn (pow_ne_zero (n - 1) hry)
44     exact h (by simpa [hz] using hrs.symm)
45   exact sub_eq_zero.mp ((mul_eq_zero.mp hp).resolve_left hs)
46 end Roots
47 
48 abbrev AbsoluteGroup := Gal(AlgebraicClosure ℚ/ℚ)
49 
50 abbrev AbsoluteIntegers := integralClosure ℤ (AlgebraicClosure ℚ)
51 
52 section Absolute
53 variable (Q : Ideal AbsoluteIntegers) [Q.IsMaximal]
54 attribute [local instance] Ideal.Quotient.field
55 
56 /-- A root of unity is an actual element of the integral closure. -/
57 theorem root_isIntegral (n : ℕ) [NeZero n] {x : AlgebraicClosure ℚ} (hx : x ^ n = 1) :
58     IsIntegral ℤ x :=
59   IsIntegral.of_pow (NeZero.pos n) (hx ▸ isIntegral_one)
60 
61 /-- A p-power residue action determines the p-power action on roots whose order
62 is nonzero in the residue field. -/
63 theorem maps_roots_to_power (n : ℕ) [NeZero n] (hn : (n : AbsoluteIntegers ⧸ Q) ≠ 0)
64     (p : ℕ) (γ : AbsoluteGroup)
65     (hγ : ∀ z : AbsoluteIntegers, Ideal.Quotient.mk Q (γ • z) =
66       (Ideal.Quotient.mk Q z) ^ p)
67     {x : AlgebraicClosure ℚ} (hx : x ^ n = 1) : γ x = x ^ p := by
68   let z : AbsoluteIntegers := ⟨x, root_isIntegral n hx⟩
69   have hz : z ^ n = 1 := Subtype.ext hx
70   have hleft : (γ • z) ^ n = 1 := by
71     change (MulSemiringAction.toRingAut (AbsoluteGroup) AbsoluteIntegers γ z) ^ n = 1
72     rw [← map_pow, hz, map_one]
73   have hright : (z ^ p) ^ n = 1 := by rw [pow_right_comm, hz, one_pow]
74   have hres : Ideal.Quotient.mk Q (γ • z) = Ideal.Quotient.mk Q (z ^ p) := by
75     rw [map_pow]
76     exact hγ z
77   exact congrArg (fun a : AbsoluteIntegers => (a : AlgebraicClosure ℚ))
78     (map_injective_on_roots (Ideal.Quotient.mk Q) n hn hleft hright hres)
79 
80 /-- Coprimality makes the root order nonzero in the actual residue field over p. -/
81 theorem order_nonzero_in_quotient (n p : ℕ) [Fact p.Prime]
82     [Q.LiesOver (Ideal.span {(p : ℤ)})] (hp : p.Coprime n) :
83     (n : AbsoluteIntegers ⧸ Q) ≠ 0 := by
84   let : CharP (ℤ ⧸ Ideal.span {(p : ℤ)}) p := ringChar.of_eq <| Int.ringChar_idealQuot p
85   let : CharP (AbsoluteIntegers ⧸ Q) p :=
86     charP_of_injective_algebraMap
87       (algebraMap (ℤ ⧸ Ideal.span {(p : ℤ)}) (AbsoluteIntegers ⧸ Q)).injective p
88   rw [ne_eq, CharP.cast_eq_zero_iff]
89   exact (Nat.Prime.coprime_iff_not_dvd (Fact.out : p.Prime)).mp hp
90 end Absolute
91 
92 section Cyclotomic
93 variable (n : ℕ) [NeZero n] (L : Type*) [Field L] [NumberField L]
94   [IsCyclotomicExtension {n} ℚ L]
95 variable (Q : Ideal AbsoluteIntegers) [Q.IsMaximal] (p : ℕ) [Fact p.Prime]
96   [Q.LiesOver (Ideal.span {(p : ℤ)})] (hp : p.Coprime n)
97 
98 /-- An actual absolute-Galois p-power residue action restricts to the arithmetic
99 cyclotomic Frobenius. Existence of the element is a separate theorem. -/
100 theorem restriction_eq_primePower_of_residue (γ : AbsoluteGroup)
101     (hγ : ∀ z : AbsoluteIntegers, Ideal.Quotient.mk Q (γ • z) =
102       (Ideal.Quotient.mk Q z) ^ p) :
103     restrictionMap n L γ = PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp := by
104   have hζ := IsCyclotomicExtension.zeta_spec n ℚ L
105   have hfix : restrictionMap n L γ (IsCyclotomicExtension.zeta n ℚ L) =
106       PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp
107         (IsCyclotomicExtension.zeta n ℚ L) := by
108     apply (fieldEmbedding n L).injective
109     change fieldEmbedding n L ((restrictionMap n L γ) _) = _
110     rw [restrictionMap_commutes n L γ,
111       PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism_apply n L p hp hζ.pow_eq_one,
112       map_pow]
113     exact maps_roots_to_power Q n (order_nonzero_in_quotient Q n p hp) p γ hγ
114       (by rw [← map_pow, hζ.pow_eq_one, map_one])
115   apply AlgEquiv.coe_toAlgHom_injective
116   apply AlgHom.ext_of_adjoin_eq_top
117     (IsCyclotomicExtension.adjoin_primitive_root_eq_top hζ)
118   intro x hx
119   have hx' : x = IsCyclotomicExtension.zeta n ℚ L := Set.mem_singleton_iff.mp hx
120   subst x
121   exact hfix
122 
123 include hp in
124 /-- The actual ideal inertia subgroup, defined by trivial residue action, is
125 killed by restriction to the cyclotomic field away from its root order. -/
126 theorem restriction_eq_one_of_inertia (γ : AbsoluteGroup)
127     (hγ : γ ∈ Q.inertia (AbsoluteGroup)) : restrictionMap n L γ = 1 := by
128   have hζ := IsCyclotomicExtension.zeta_spec n ℚ L
129   have hfix : restrictionMap n L γ (IsCyclotomicExtension.zeta n ℚ L) =
130       IsCyclotomicExtension.zeta n ℚ L := by
131     apply (fieldEmbedding n L).injective
132     change fieldEmbedding n L ((restrictionMap n L γ) _) = _
133     rw [restrictionMap_commutes n L γ]
134     simpa using maps_roots_to_power Q n (order_nonzero_in_quotient Q n p hp) 1 γ
135       (fun z => by simpa using (Ideal.Quotient.eq.mpr (hγ z)))
136       (by rw [← map_pow, hζ.pow_eq_one, map_one])
137   apply AlgEquiv.coe_toAlgHom_injective
138   apply AlgHom.ext_of_adjoin_eq_top
139     (IsCyclotomicExtension.adjoin_primitive_root_eq_top hζ)
140   intro x hx
141   have hx' : x = IsCyclotomicExtension.zeta n ℚ L := Set.mem_singleton_iff.mp hx
142   subst x
143   exact hfix
144 section Representations
145 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
146 variable (ρ : Representation K Gal(L/ℚ) V)
147 
148 include hp in
149 /-- Every representation pulled back from the cyclotomic field kills the actual
150 ideal inertia at primes not dividing the root order. -/
151 theorem pullback_trivial_on_inertia (γ : AbsoluteGroup)
152     (hγ : γ ∈ Q.inertia AbsoluteGroup) :
153     (ρ.comp (restrictionMap n L)) γ = 1 := by
154   change ρ (restrictionMap n L γ) = 1
155   rw [restriction_eq_one_of_inertia n L Q p hp γ hγ, map_one]
156 
157 /-- The full linear action at an actual p-power residue element is the finite
158 cyclotomic Frobenius action. -/
159 theorem pullback_on_arithmeticFrobenius (γ : AbsoluteGroup)
160     (hγ : ∀ z : AbsoluteIntegers, Ideal.Quotient.mk Q (γ • z) =
161       (Ideal.Quotient.mk Q z) ^ p) :
162     (ρ.comp (restrictionMap n L)) γ =
163       ρ (PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp) := by
164   change ρ (restrictionMap n L γ) = _
165   rw [restriction_eq_primePower_of_residue n L Q p hp γ hγ]
166 
167 /-- The character comparison follows from equality of the complete actions. -/
168 theorem pullback_character_on_arithmeticFrobenius (γ : AbsoluteGroup)
169     (hγ : ∀ z : AbsoluteIntegers, Ideal.Quotient.mk Q (γ • z) =
170       (Ideal.Quotient.mk Q z) ^ p) :
171     Representation.character (ρ.comp (restrictionMap n L)) γ =
172       ρ.character (PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp) := by
173   exact congrArg (LinearMap.trace K V)
174     (pullback_on_arithmeticFrobenius n L Q p hp ρ γ hγ)
175 end Representations
176 end Cyclotomic
177 end PaperX.CyclotomicIntegralFrobenius

Back to source controls