CyclotomicInertiaBridge.lean

1 import PaperX.CyclotomicAbsoluteSamples
2 import Mathlib.RingTheory.Valuation.RamificationGroup
3 import Mathlib.NumberTheory.Padics.RingHoms
4 import Mathlib.Tactic
5 
6 /-! Actual valuation inertia fixes all roots of unity whose order is a unit in
7 its valuation ring. Consequently restriction to a cyclotomic field kills this
8 actual inertia subgroup. No quotient preimage is named an inertia subgroup. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperX.CyclotomicInertiaBridge
12 
13 section Local
14 variable {R : Type*} [CommRing R] [IsDomain R] [IsLocalRing R]
15 
16 /-- Reduction is injective on the n-th roots of unity when n is a unit. -/
17 theorem residue_injective_on_roots (n : ℕ) [NeZero n] (hn : IsUnit (n : R))
18     {x y : R} (hx : x ^ n = 1) (hy : y ^ n = 1)
19     (hres : IsLocalRing.residue R x = IsLocalRing.residue R y) : x = y := by
20   let s : R := ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
21   have hp : s * (x - y) = 0 := by
22     rw [show s = ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) from rfl,
23       geom_sum₂_mul, hx, hy, sub_self]
24   have hry : IsLocalRing.residue R y ≠ 0 := by
25     intro hz
26     have h := congrArg (IsLocalRing.residue R) hy
27     simp [hz, NeZero.ne n] at h
28   have hrs : IsLocalRing.residue R s =
29       (n : IsLocalRing.ResidueField R) * (IsLocalRing.residue R y) ^ (n - 1) := by
30     simp only [s, map_sum, map_mul, map_pow, hres]
31     rw [show (∑ i ∈ Finset.range n,
32       IsLocalRing.residue R y ^ i * IsLocalRing.residue R y ^ (n - 1 - i)) =
33       ∑ _i ∈ Finset.range n, IsLocalRing.residue R 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 hn0 : (n : IsLocalRing.ResidueField R) ≠ 0 := by
42     simpa only [map_natCast] using (IsLocalRing.residue_ne_zero_iff_isUnit (n : R)).mpr hn
43   have hs : s ≠ 0 := by
44     intro hz
45     have := mul_ne_zero hn0 (pow_ne_zero (n - 1) hry)
46     exact this (by simpa [hz] using hrs.symm)
47   exact sub_eq_zero.mp ((mul_eq_zero.mp hp).resolve_left hs)
48 end Local
49 
50 section Valuation
51 variable {L : Type*} [Field L]
52 
53 /-- Every root of unity belongs to any valuation subring of its field. -/
54 theorem root_mem_valuation (A : ValuationSubring L) (n : ℕ) [NeZero n]
55     {x : L} (hx : x ^ n = 1) : x ∈ A := by
56   have hx0 : x ≠ 0 := by
57     intro hz
58     simp [hz, NeZero.ne n] at hx
59   rcases A.mem_or_inv_mem x with h | h
60   · exact h
61   · have hinv : x⁻¹ ^ (n - 1) = x := by
62       rw [inv_pow_sub₀ hx0 (Nat.one_le_iff_ne_zero.mpr (NeZero.ne n)), hx]
63       simp
64     simpa [hinv] using A.toSubring.pow_mem h (n - 1)
65 
66 /-- The actual residue-action kernel fixes every n-th root when n is a unit. -/
67 theorem inertia_fixes_roots (K : Type*) [Field K] [Algebra K L]
68     (A : ValuationSubring L) (n : ℕ) [NeZero n] (hn : IsUnit (n : A))
69     {x : L} (hx : x ^ n = 1)
70     (σ : A.decompositionSubgroup K) (hσ : σ ∈ A.inertiaSubgroup K) :
71     (σ.val : L ≃ₐ[K] L) x = x := by
72   let z : A := ⟨x, root_mem_valuation A n hx⟩
73   have hz : z ^ n = 1 := Subtype.ext hx
74   have hres : IsLocalRing.residue A (σ • z) = IsLocalRing.residue A z := by
75     change MulSemiringAction.toRingAut (A.decompositionSubgroup K)
76       (IsLocalRing.ResidueField A) σ = 1 at hσ
77     exact congrArg (fun f : RingAut (IsLocalRing.ResidueField A) =>
78       f (IsLocalRing.residue A z)) hσ
79   have hp : (σ • z) ^ n = 1 := by
80     change (MulSemiringAction.toRingAut (A.decompositionSubgroup K) A σ z) ^ n = 1
81     rw [← map_pow, hz, map_one]
82   exact congrArg (fun a : A => (a : L)) (residue_injective_on_roots n hn hp hz hres)
83 /-- A decomposition element with arithmetic p-power residue action has that
84 same p-power action on all roots of order invertible in the valuation ring. -/
85 theorem decomposition_maps_roots_to_power (K : Type*) [Field K] [Algebra K L]
86     (A : ValuationSubring L) (n : ℕ) [NeZero n] (hn : IsUnit (n : A))
87     (p : ℕ) (σ : A.decompositionSubgroup K)
88     (hσ : ∀ z : A, IsLocalRing.residue A (σ • z) = (IsLocalRing.residue A z) ^ p)
89     {x : L} (hx : x ^ n = 1) : (σ.val : L ≃ₐ[K] L) x = x ^ p := by
90   let z : A := ⟨x, root_mem_valuation A n hx⟩
91   have hz : z ^ n = 1 := Subtype.ext hx
92   have hleft : (σ • z) ^ n = 1 := by
93     change (MulSemiringAction.toRingAut (A.decompositionSubgroup K) A σ z) ^ n = 1
94     rw [← map_pow, hz, map_one]
95   have hright : (z ^ p) ^ n = 1 := by rw [pow_right_comm, hz, one_pow]
96   have hres : IsLocalRing.residue A (σ • z) = IsLocalRing.residue A (z ^ p) := by
97     rw [map_pow]
98     exact hσ z
99   exact congrArg (fun a : A => (a : L))
100     (residue_injective_on_roots n hn hleft hright hres)
101 end Valuation
102 
103 section Cyclotomic
104 open NumberField PaperX.CyclotomicAbsoluteSamples
105 variable (n : ℕ) [NeZero n] (L : Type*) [Field L] [NumberField L]
106   [IsCyclotomicExtension {n} ℚ L]
107 
108 /-- Restriction of actual valuation inertia to the cyclotomic extension is
109 trivial when the root order is invertible in the valuation ring. -/
110 theorem restriction_eq_one_of_inertia
111     (A : ValuationSubring (AlgebraicClosure ℚ)) (hn : IsUnit (n : A))
112     (σ : A.decompositionSubgroup ℚ) (hσ : σ ∈ A.inertiaSubgroup ℚ) :
113     restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val) = 1 := by
114   have hζ := IsCyclotomicExtension.zeta_spec n ℚ L
115   have hfix : restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val) (IsCyclotomicExtension.zeta n ℚ L) =
116       IsCyclotomicExtension.zeta n ℚ L := by
117     apply (fieldEmbedding n L).injective
118     change fieldEmbedding n L ((restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val)) _) = _
119     rw [restrictionMap_commutes n L (show Field.absoluteGaloisGroup ℚ from σ.val)]
120     exact inertia_fixes_roots ℚ A n hn
121       (by rw [← map_pow, hζ.pow_eq_one, map_one]) σ hσ
122   apply AlgEquiv.coe_toAlgHom_injective
123   apply AlgHom.ext_of_adjoin_eq_top
124     (IsCyclotomicExtension.adjoin_primitive_root_eq_top hζ)
125   intro x hx
126   have hx' : x = IsCyclotomicExtension.zeta n ℚ L := Set.mem_singleton_iff.mp hx
127   subst x
128   exact hfix
129 
130 omit [NeZero n] in
131 /-- A valuation with residue characteristic p makes each integer coprime to p
132 a unit. This turns a prime-coprimality hypothesis into the local unit condition. -/
133 theorem order_isUnit_of_coprime
134     (A : ValuationSubring (AlgebraicClosure ℚ)) (p : ℕ) [Fact p.Prime]
135     [CharP (IsLocalRing.ResidueField A) p] (hp : p.Coprime n) : IsUnit (n : A) := by
136   apply (IsLocalRing.residue_ne_zero_iff_isUnit (n : A)).mp
137   rw [map_natCast, ne_eq, CharP.cast_eq_zero_iff]
138   exact (Nat.Prime.coprime_iff_not_dvd (Fact.out : p.Prime)).mp hp
139 
140 /-- Actual valuation inertia over a residue prime not dividing n acts trivially
141 on the chosen cyclotomic subfield of the algebraic closure. -/
142 theorem restriction_eq_one_of_coprime_inertia
143     (A : ValuationSubring (AlgebraicClosure ℚ)) (p : ℕ) [Fact p.Prime]
144     [CharP (IsLocalRing.ResidueField A) p] (hp : p.Coprime n)
145     (σ : A.decompositionSubgroup ℚ) (hσ : σ ∈ A.inertiaSubgroup ℚ) :
146     restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val) = 1 :=
147   restriction_eq_one_of_inertia n L A (order_isUnit_of_coprime n A p hp) σ hσ
148 /-- Recognition of a genuine arithmetic Frobenius element: its restriction
149 is exactly the finite cyclotomic sample proved in Block 25. This theorem assumes
150 the decomposition element and its residue action, but proves the comparison. -/
151 theorem restriction_eq_primePower_of_residue
152     (A : ValuationSubring (AlgebraicClosure ℚ)) (p : ℕ) (hp : p.Coprime n)
153     (hn : IsUnit (n : A)) (σ : A.decompositionSubgroup ℚ)
154     (hσ : ∀ z : A, IsLocalRing.residue A (σ • z) = (IsLocalRing.residue A z) ^ p) :
155     restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val) = PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp := by
156   have hζ := IsCyclotomicExtension.zeta_spec n ℚ L
157   have hfix : restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val) (IsCyclotomicExtension.zeta n ℚ L) =
158       PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp
159         (IsCyclotomicExtension.zeta n ℚ L) := by
160     apply (fieldEmbedding n L).injective
161     change fieldEmbedding n L ((restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val)) _) = _
162     rw [restrictionMap_commutes n L (show Field.absoluteGaloisGroup ℚ from σ.val),
163       PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism_apply n L p hp hζ.pow_eq_one,
164       map_pow]
165     exact decomposition_maps_roots_to_power ℚ A n hn p σ hσ
166       (by rw [← map_pow, hζ.pow_eq_one, map_one])
167   apply AlgEquiv.coe_toAlgHom_injective
168   apply AlgHom.ext_of_adjoin_eq_top
169     (IsCyclotomicExtension.adjoin_primitive_root_eq_top hζ)
170   intro x hx
171   have hx' : x = IsCyclotomicExtension.zeta n ℚ L := Set.mem_singleton_iff.mp hx
172   subst x
173   exact hfix
174 
175 /-- The cyclotomic Frobenius comparison at a prime whose residue characteristic
176 is p. Coprimality supplies the unit condition rather than assuming it separately. -/
177 theorem restriction_eq_primePower_of_coprime_residue
178     (A : ValuationSubring (AlgebraicClosure ℚ)) (p : ℕ) [Fact p.Prime]
179     [CharP (IsLocalRing.ResidueField A) p] (hp : p.Coprime n)
180     (σ : A.decompositionSubgroup ℚ)
181     (hσ : ∀ z : A, IsLocalRing.residue A (σ • z) = (IsLocalRing.residue A z) ^ p) :
182     restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val) = PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp :=
183   restriction_eq_primePower_of_residue n L A p hp (order_isUnit_of_coprime n A p hp) σ hσ
184 section Representations
185 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
186 variable (ρ : Representation K Gal(L/ℚ) V)
187 
188 /-- Every representation inflated from the cyclotomic field is unramified on
189 the actual valuation inertia away from primes dividing the root order. -/
190 theorem pullback_trivial_on_inertia
191     (A : ValuationSubring (AlgebraicClosure ℚ)) (p : ℕ) [Fact p.Prime]
192     [CharP (IsLocalRing.ResidueField A) p] (hp : p.Coprime n)
193     (σ : A.decompositionSubgroup ℚ) (hσ : σ ∈ A.inertiaSubgroup ℚ) :
194     (ρ.comp (restrictionMap n L)) (show Field.absoluteGaloisGroup ℚ from σ.val) = 1 := by
195   change ρ (restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val)) = 1
196   rw [restriction_eq_one_of_coprime_inertia n L A p hp σ hσ, map_one]
197 
198 /-- The entire inflated linear action at a genuine decomposition Frobenius is
199 the finite cyclotomic action. The Frobenius element remains supplied. -/
200 theorem pullback_on_arithmeticFrobenius
201     (A : ValuationSubring (AlgebraicClosure ℚ)) (p : ℕ) [Fact p.Prime]
202     [CharP (IsLocalRing.ResidueField A) p] (hp : p.Coprime n)
203     (σ : A.decompositionSubgroup ℚ)
204     (hσ : ∀ z : A, IsLocalRing.residue A (σ • z) = (IsLocalRing.residue A z) ^ p) :
205     (ρ.comp (restrictionMap n L)) (show Field.absoluteGaloisGroup ℚ from σ.val) =
206       ρ (PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp) := by
207   change ρ (restrictionMap n L (show Field.absoluteGaloisGroup ℚ from σ.val)) = _
208   rw [restriction_eq_primePower_of_coprime_residue n L A p hp σ hσ]
209 
210 /-- The trace comparison follows from equality of the full linear operators. -/
211 theorem pullback_character_on_arithmeticFrobenius
212     (A : ValuationSubring (AlgebraicClosure ℚ)) (p : ℕ) [Fact p.Prime]
213     [CharP (IsLocalRing.ResidueField A) p] (hp : p.Coprime n)
214     (σ : A.decompositionSubgroup ℚ)
215     (hσ : ∀ z : A, IsLocalRing.residue A (σ • z) = (IsLocalRing.residue A z) ^ p) :
216     Representation.character (ρ.comp (restrictionMap n L)) (show Field.absoluteGaloisGroup ℚ from σ.val) =
217       ρ.character (PaperX.CyclotomicPrimeCoverage.primePowerAutomorphism n L p hp) := by
218   exact congrArg (LinearMap.trace K V)
219     (pullback_on_arithmeticFrobenius n L ρ A p hp σ hσ)
220 end Representations
221 end Cyclotomic
222 
223 /-- The unit condition is essential even in a genuine characteristic-zero DVR:
224 1 and -1 in Z₂ are distinct square roots with identical residues. -/
225 theorem twoAdic_distinct_roots_same_residue :
226     ∃ x y : PadicInt 2, x ^ 2 = 1 ∧ y ^ 2 = 1 ∧ x ≠ y ∧
227       IsLocalRing.residue (PadicInt 2) x = IsLocalRing.residue (PadicInt 2) y := by
228   refine ⟨1, -1, by norm_num, by norm_num, by norm_num, ?_⟩
229   apply (PadicInt.residueField (p := 2)).injective
230   simp only [map_one, map_neg]
231   change (1 : ZMod 2) = -1
232   decide
233 
234 /-- The root order 2 in that boundary example is not a unit of Z₂. -/
235 theorem twoAdic_order_not_unit : ¬ IsUnit (2 : PadicInt 2) := by
236   exact PadicInt.p_nonunit (p := 2)
237 
238 
239 end PaperX.CyclotomicInertiaBridge

Back to source controls