RamificationPolyphase.lean

1 import PaperXI.ValuationConductor
2 import PaperXI.FiniteAverage
3 
4 /-! # Ramification polyphase projectors
5 
6 The lower ramification filtration gives a nested family of literal finite-group
7 averaging projectors.  Successive differences are the depth-detail channels.
8 This is a representation-theoretic multiresolution theorem; it does not assert
9 existence of an intrinsic wild-break decomposition beyond the supplied lower
10 filtration.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 open scoped Classical BigOperators
15 
16 namespace PaperXI.RamificationPolyphase
17 
18 open PaperXI.ResidueWeil
19 open PaperXI.ValuationRamification
20 open PaperXI.ValuationConductor
21 open PaperXI.FiniteAverage
22 
23 section AverageRestriction
24 
25 variable {G H V : Type*} [Group G] [Fintype G] [Group H] [Fintype H]
26 variable [AddCommGroup V] [Module ℂ V]
27 
28 /-- Averaging after one group operator does not change the average. -/
29 theorem average_comp_operator (ρ : Representation ℂ G V) (g : G) :
30     (average ρ).comp (ρ g) = average ρ := by
31   ext v
32   change average ρ (ρ g v) = average ρ v
33   rw [average_apply, average_apply]
34   congr 1
35   simp only [← Module.End.mul_apply, ← map_mul]
36   exact Function.Bijective.sum_comp (Group.mulRight_bijective g) (fun h => ρ h v)
37 
38 /-- Averaging over the ambient group after averaging over any mapped finite
39 subgroup gives the ambient average. -/
40 theorem average_comp_restricted_average (ρ : Representation ℂ G V) (f : H →* G) :
41     (average ρ).comp (average (ρ.comp f)) = average ρ := by
42   ext v
43   change average ρ (average (ρ.comp f) v) = average ρ v
44   rw [average_apply (ρ.comp f), map_smul, map_sum]
45   have hs : ∀ h : H, average ρ ((ρ.comp f) h v) = average ρ v := by
46     intro h
47     exact LinearMap.congr_fun (average_comp_operator ρ (f h)) v
48   simp_rw [hs]
49   rw [Finset.sum_const, Finset.card_univ, ← Nat.cast_smul_eq_nsmul ℂ, smul_smul,
50     inv_mul_cancel₀ (card_ne_zero (G := H)), one_smul]
51 
52 /-- Averaging over a mapped finite subgroup fixes the ambient average. -/
53 theorem restricted_average_comp_average (ρ : Representation ℂ G V) (f : H →* G) :
54     (average (ρ.comp f)).comp (average ρ) = average ρ := by
55   ext v
56   change average (ρ.comp f) (average ρ v) = average ρ v
57   exact fixes (ρ.comp f) (fun h => invariant ρ v (f h))
58 
59 end AverageRestriction
60 
61 section LowerFiltration
62 
63 variable (R D : Type*) [CommRing R] [IsLocalRing R] [Group D] [Fintype D] [MulSemiringAction D R]
64 variable (F : RingAut (IsLocalRing.ResidueField R))
65 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
66 variable (ρ : Representation ℂ (Pullback (residue R D) F) V)
67 
68 /-- Inclusion from a deeper lower group into a shallower lower group. -/
69 def lowerInclusion {i j : ℕ} (hij : i ≤ j) : lower R D j →* lower R D i where
70   toFun g := ⟨g.val, antitone R D hij g.property⟩
71   map_one' := rfl
72   map_mul' _ _ := rfl
73 
74 omit [Fintype D] in
75 @[simp] theorem lowerInclusion_val {i j : ℕ} (hij : i ≤ j)
76     (g : lower R D j) : (lowerInclusion (R := R) (D := D) hij g : D) = g := rfl
77 
78 omit [Fintype D] in
79 /-- Lower-group lifts commute with the canonical filtration inclusion. -/
80 theorem lift_lowerInclusion {i j : ℕ} (hij : i ≤ j) (g : lower R D j) :
81     lift R D F i (lowerInclusion (R := R) (D := D) hij g) = lift R D F j g := rfl
82 
83 /-- The literal averaging projector onto vectors fixed at depth `i`. -/
84 def depthProjector (i : ℕ) : Module.End ℂ V :=
85   average (ρ.comp (lift R D F i))
86 
87 /-- The range is the actual lower fixed space used by the conductor theory. -/
88 theorem depthProjector_range (i : ℕ) :
89     LinearMap.range (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i) = fixed R D F ρ i :=
90   range_eq _
91 
92 /-- Every depth projector is idempotent. -/
93 theorem depthProjector_idempotent (i : ℕ) :
94     (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i).comp (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i) =
95       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i :=
96   idempotent _
97 
98 /-- A shallower projector composed after a deeper projector is the shallower
99 projector. -/
100 theorem depthProjector_comp_of_le {i j : ℕ} (hij : i ≤ j) :
101     (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i).comp (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) j) =
102       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
103   let f := lowerInclusion (R := R) (D := D) hij
104   have hrep : (ρ.comp (lift R D F i)).comp f = ρ.comp (lift R D F j) := by
105     ext g v
106     rfl
107   change (average (ρ.comp (lift R D F i))).comp
108       (average (ρ.comp (lift R D F j))) = average (ρ.comp (lift R D F i))
109   rw [← hrep]
110   exact average_comp_restricted_average (ρ.comp (lift R D F i)) f
111 
112 /-- A deeper projector composed after a shallower projector is also the
113 shallower projector. -/
114 theorem depthProjector_comp_of_le_rev {i j : ℕ} (hij : i ≤ j) :
115     (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) j).comp (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i) =
116       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
117   let f := lowerInclusion (R := R) (D := D) hij
118   have hrep : (ρ.comp (lift R D F i)).comp f = ρ.comp (lift R D F j) := by
119     ext g v
120     rfl
121   change (average (ρ.comp (lift R D F j))).comp
122       (average (ρ.comp (lift R D F i))) = average (ρ.comp (lift R D F i))
123   rw [← hrep]
124   exact restricted_average_comp_average (ρ.comp (lift R D F i)) f
125 
126 /-- The detail channel revealed between depths `i` and `i+1`. -/
127 def detailProjector (i : ℕ) : Module.End ℂ V :=
128   depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i + 1) - depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i
129 
130 @[simp] theorem detailProjector_apply (i : ℕ) (v : V) :
131     detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i v =
132       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v - depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := rfl
133 
134 /-- Every ramification detail channel is itself an idempotent projector. -/
135 theorem detailProjector_idempotent (i : ℕ) :
136     (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i).comp
137         (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) =
138       detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
139   ext v
140   simp only [detailProjector_apply, LinearMap.comp_apply, map_sub]
141   have hQQ : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1)
142       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v) =
143       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v := by
144     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
145       (depthProjector_idempotent (R := R) (D := D) (F := F) (ρ := ρ) (i+1)) v
146   have hPQ : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i
147       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v) =
148       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
149     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
150       (depthProjector_comp_of_le (R := R) (D := D) (F := F) (ρ := ρ)
151         (Nat.le_succ i)) v
152   have hQP : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1)
153       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v) =
154       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
155     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
156       (depthProjector_comp_of_le_rev (R := R) (D := D) (F := F) (ρ := ρ)
157         (Nat.le_succ i)) v
158   have hPP : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i
159       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v) =
160       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
161     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
162       (depthProjector_idempotent (R := R) (D := D) (F := F) (ρ := ρ) i) v
163   rw [hQQ, hPQ, hQP, hPP]
164   abel
165 
166 /-- A detail vector is killed by the preceding coarse projector. -/
167 theorem depthProjector_detailProjector (i : ℕ) :
168     (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i).comp
169         (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) = 0 := by
170   ext v
171   simp only [detailProjector_apply, LinearMap.comp_apply, map_sub, LinearMap.zero_apply]
172   have hPQ : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i
173       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v) =
174       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
175     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
176       (depthProjector_comp_of_le (R := R) (D := D) (F := F) (ρ := ρ)
177         (Nat.le_succ i)) v
178   have hPP : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i
179       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v) =
180       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
181     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
182       (depthProjector_idempotent (R := R) (D := D) (F := F) (ρ := ρ) i) v
183   rw [hPQ, hPP, sub_self]
184 
185 /-- The next projector fixes its corresponding detail channel. -/
186 theorem depthProjector_succ_detailProjector (i : ℕ) :
187     (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1)).comp
188         (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) =
189       detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
190   ext v
191   simp only [detailProjector_apply, LinearMap.comp_apply, map_sub]
192   have hQQ : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1)
193       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v) =
194       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v := by
195     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
196       (depthProjector_idempotent (R := R) (D := D) (F := F) (ρ := ρ) (i+1)) v
197   have hQP : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1)
198       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v) =
199       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
200     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
201       (depthProjector_comp_of_le_rev (R := R) (D := D) (F := F) (ρ := ρ)
202         (Nat.le_succ i)) v
203   rw [hQQ, hQP]
204 
205 /-- A detail vector lies in the next fixed space. -/
206 theorem detailProjector_mem_next_fixed (i : ℕ) (v : V) :
207     detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i v ∈ fixed R D F ρ (i+1) := by
208   rw [← depthProjector_range]
209   refine ⟨detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i v, ?_⟩
210   simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
211     (depthProjector_succ_detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) v
212 
213 /-- The detail range is exactly the newly visible fixed space: fixed at depth
214 `i+1` and annihilated by the previous coarse projector. -/
215 theorem detailProjector_range (i : ℕ) :
216     LinearMap.range (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) =
217       fixed R D F ρ (i+1) ⊓ LinearMap.ker (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i) := by
218   ext v
219   constructor
220   · rintro ⟨x, rfl⟩
221     exact ⟨detailProjector_mem_next_fixed (R := R) (D := D) (F := F) (ρ := ρ) i x,
222       LinearMap.mem_ker.mpr (LinearMap.congr_fun
223         (depthProjector_detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) x)⟩
224   · rintro ⟨hvnext, hvker⟩
225     refine ⟨v, ?_⟩
226     rw [detailProjector_apply]
227     have hnext : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v = v :=
228       fixes _ hvnext
229     rw [hnext, LinearMap.mem_ker.mp hvker, sub_zero]
230 
231 /-- Distinct detail channels compose to zero. -/
232 theorem detailProjector_comp_eq_zero {i j : ℕ} (hij : i < j) :
233     (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i).comp
234         (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) j) = 0 := by
235   ext v
236   have hi1j : i + 1 ≤ j := hij
237   simp only [detailProjector_apply, LinearMap.comp_apply, map_sub, LinearMap.zero_apply]
238   have h11 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1)
239       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (j+1) v) =
240       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v := by
241     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
242       (depthProjector_comp_of_le (R := R) (D := D) (F := F) (ρ := ρ)
243         (Nat.succ_le_succ (Nat.le_of_lt hij))) v
244   have h01 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i
245       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (j+1) v) =
246       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
247     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
248       (depthProjector_comp_of_le (R := R) (D := D) (F := F) (ρ := ρ)
249         (Nat.le_trans (Nat.le_of_lt hij) (Nat.le_succ j))) v
250   have h10 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1)
251       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) j v) =
252       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v := by
253     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
254       (depthProjector_comp_of_le (R := R) (D := D) (F := F) (ρ := ρ) hi1j) v
255   have h00 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i
256       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) j v) =
257       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
258     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
259       (depthProjector_comp_of_le (R := R) (D := D) (F := F) (ρ := ρ)
260         (Nat.le_of_lt hij)) v
261   rw [h11, h01, h10, h00]
262   abel
263 
264 /-- Distinct detail channels compose to zero in the opposite order as well. -/
265 theorem detailProjector_comp_eq_zero_rev {i j : ℕ} (hij : i < j) :
266     (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) j).comp
267         (detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i) = 0 := by
268   ext v
269   have hi1j : i + 1 ≤ j := hij
270   simp only [detailProjector_apply, LinearMap.comp_apply, map_sub, LinearMap.zero_apply]
271   have h11 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (j+1)
272       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v) =
273       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v := by
274     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
275       (depthProjector_comp_of_le_rev (R := R) (D := D) (F := F) (ρ := ρ)
276         (Nat.succ_le_succ (Nat.le_of_lt hij))) v
277   have h10 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) j
278       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v) =
279       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (i+1) v := by
280     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
281       (depthProjector_comp_of_le_rev (R := R) (D := D) (F := F) (ρ := ρ) hi1j) v
282   have h01 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) (j+1)
283       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v) =
284       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
285     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
286       (depthProjector_comp_of_le_rev (R := R) (D := D) (F := F) (ρ := ρ)
287         (Nat.le_trans (Nat.le_of_lt hij) (Nat.le_succ j))) v
288   have h00 : depthProjector (R := R) (D := D) (F := F) (ρ := ρ) j
289       (depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v) =
290       depthProjector (R := R) (D := D) (F := F) (ρ := ρ) i v := by
291     simpa only [LinearMap.comp_apply] using LinearMap.congr_fun
292       (depthProjector_comp_of_le_rev (R := R) (D := D) (F := F) (ρ := ρ)
293         (Nat.le_of_lt hij)) v
294   rw [h11, h10, h01, h00]
295   abel
296 
297 /-- Finite telescoping reconstruction of a deeper fixed-space projector from
298 the inertia projector and the intervening detail channels. -/
299 theorem depthProjector_eq_zero_add_sum (n : ℕ) :
300     depthProjector (R := R) (D := D) (F := F) (ρ := ρ) n = depthProjector (R := R) (D := D) (F := F) (ρ := ρ) 0 +
301       ∑ i ∈ Finset.range n, detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
302   induction n with
303   | zero => simp
304   | succ n ih =>
305       rw [Finset.sum_range_succ, ← add_assoc, ← ih]
306       ext v
307       simp [detailProjector]
308 
309 /-- Once the lower filtration is trivial, the full identity decomposes into the
310 inertia-fixed channel plus finitely many depth details. -/
311 theorem identity_eq_inertia_add_details {N : ℕ} (hN : lower R D N = ⊥) :
312     (1 : Module.End ℂ V) = depthProjector (R := R) (D := D) (F := F) (ρ := ρ) 0 +
313       ∑ i ∈ Finset.range N, detailProjector (R := R) (D := D) (F := F) (ρ := ρ) i := by
314   rw [← depthProjector_eq_zero_add_sum (R := R) (D := D) (F := F) (ρ := ρ) N]
315   ext v
316   change v = depthProjector (R := R) (D := D) (F := F) (ρ := ρ) N v
317   symm
318   exact fixes _ (by
319     intro g
320     have hg : g = 1 := by simpa [hN] using g.property
321     subst g
322     simp)
323 
324 end LowerFiltration
325 
326 end PaperXI.RamificationPolyphase

Back to source controls