RamifiedUnramifiedQuotient.lean

1 import PaperXI.RamificationPolyphase
2 import PaperXI.FiniteUnramifiedWeil
3 import Mathlib.GroupTheory.QuotientGroup.Basic
4 
5 /-! # Ramified pullbacks and their inertia-free degree quotient
6 
7 The residue--Frobenius pullback retains a decomposition-group coordinate and an
8 integer degree.  Its degree kernel is inertia.  This file proves the precise
9 first-isomorphism statement and compares the quotient with the integer-degree
10 unramified model only under an explicit degree-one Frobenius-lift hypothesis.
11 
12 It also proves the exact representation-theoretic information loss: a
13 representation pulled back only through integer degree kills every lower
14 ramification subgroup, so every ramification depth projector is the identity
15 and every positive detail projector is zero.
16 -/
17 
18 set_option autoImplicit false
19 noncomputable section
20 open scoped Classical BigOperators
21 
22 namespace PaperXI.RamifiedUnramifiedQuotient
23 
24 open PaperXI.ResidueWeil
25 open PaperXI.FiniteUnramifiedWeil
26 open PaperXI.ValuationConductor
27 open PaperXI.RamificationPolyphase
28 open PaperXI.FiniteAverage
29 open PaperXI.ValuationRamification
30 open ValuativeRel
31 
32 section FirstIsomorphism
33 
34 variable {D C : Type*} [Group D] [Group C]
35 variable (r : D →* C) (F : C)
36 
37 /-- The inertia subgroup of a residue--Frobenius pullback is its degree kernel. -/
38 abbrev Inertia : Subgroup (Pullback r F) := (degree r F).ker
39 
40 /-- Noether's first isomorphism theorem for the integer-degree map, without a
41 surjectivity assumption. -/
42 noncomputable def quotientEquivDegreeRange :
43     Pullback r F ⧸ Inertia r F ≃* (degree r F).range :=
44   QuotientGroup.quotientKerEquivRange (degree r F)
45 
46 /-- One degree-one lift generates every integral degree. -/
47 theorem degree_surjective_of_degree_one
48     (w₁ : Pullback r F)
49     (hw₁ : degree r F w₁ = Multiplicative.ofAdd (1 : ℤ)) :
50     Function.Surjective (degree r F) := by
51   intro n
52   refine ⟨w₁ ^ Multiplicative.toAdd n, ?_⟩
53   rw [map_zpow, hw₁]
54   apply Multiplicative.toAdd.injective
55   simp
56 
57 /-- A lift of the chosen residue Frobenius is exactly the hypothesis needed for
58 surjectivity of integer degree. -/
59 theorem degree_surjective_of_frobenius_mem_range
60     (hF : F ∈ r.range) : Function.Surjective (degree r F) := by
61   obtain ⟨w₁, hw₁⟩ := (exists_degree_one_iff r F).2 hF
62   exact degree_surjective_of_degree_one r F w₁ hw₁
63 
64 /-- With an actual degree-one Frobenius lift, quotienting by inertia gives the
65 full integer-degree group. -/
66 noncomputable def quotientEquivIntegerDegree
67     (hF : F ∈ r.range) : Pullback r F ⧸ Inertia r F ≃* Multiplicative ℤ :=
68   QuotientGroup.quotientKerEquivOfSurjective (degree r F)
69     (degree_surjective_of_frobenius_mem_range r F hF)
70 
71 @[simp]
72 theorem quotientEquivIntegerDegree_mk
73     (hF : F ∈ r.range) (w : Pullback r F) :
74     quotientEquivIntegerDegree r F hF (QuotientGroup.mk w) = degree r F w := by
75   change QuotientGroup.kerLift (degree r F) (QuotientGroup.mk w) = degree r F w
76   exact QuotientGroup.kerLift_mk (degree r F) w
77 
78 /-- Two degree-one Frobenius lifts differ by inertia. -/
79 theorem frobenius_lift_ratio_mem_inertia
80     {w₁ w₂ : Pullback r F}
81     (h₁ : degree r F w₁ = Multiplicative.ofAdd (1 : ℤ))
82     (h₂ : degree r F w₂ = Multiplicative.ofAdd (1 : ℤ)) :
83     w₁ * w₂⁻¹ ∈ Inertia r F := by
84   change degree r F (w₁ * w₂⁻¹) = 1
85   rw [map_mul, map_inv, h₁, h₂]
86   simp
87 
88 end FirstIsomorphism
89 
90 section CurrentDegreeModel
91 
92 variable {D C : Type*} [Group D] [Group C]
93 variable (r : D →* C) (F : C)
94 
95 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
96   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
97 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
98   [FiniteDimensional 𝓀[K] s]
99 
100 /-- Forget the ramified decomposition-group coordinate and retain only integer
101 degree in the current unramified Weil model. -/
102 noncomputable def degreeModelMap :
103     Pullback r F →* UnramifiedWeil K s :=
104   (degreeEquiv K s).symm.toMonoidHom.comp (degree r F)
105 
106 @[simp]
107 theorem degreeModelMap_degree (w : Pullback r F) :
108     degreeEquiv K s (degreeModelMap r F K s w) = degree r F w := by
109   simp [degreeModelMap]
110 
111 /-- The degree-only map kills exactly inertia. -/
112 theorem degreeModelMap_ker :
113     (degreeModelMap r F K s).ker = Inertia r F := by
114   ext w
115   simp [degreeModelMap]
116 
117 /-- Under a degree-one lift, the degree-only comparison is onto the current
118 integer-degree unramified model. -/
119 theorem degreeModelMap_surjective
120     (hF : F ∈ r.range) : Function.Surjective (degreeModelMap r F K s) := by
121   intro u
122   obtain ⟨w, hw⟩ := degree_surjective_of_frobenius_mem_range r F hF
123       ((degreeEquiv K s) u)
124   refine ⟨w, ?_⟩
125   apply (degreeEquiv K s).injective
126   simpa [degreeModelMap] using hw
127 
128 /-- The quotient by inertia is the current unramified degree model, under the
129 explicit degree-one lift hypothesis. -/
130 noncomputable def quotientEquivUnramified
131     (hF : F ∈ r.range) :
132     Pullback r F ⧸ Inertia r F ≃* UnramifiedWeil K s :=
133   (quotientEquivIntegerDegree r F hF).trans (degreeEquiv K s).symm
134 
135 @[simp]
136 theorem quotientEquivUnramified_mk_degree
137     (hF : F ∈ r.range) (w : Pullback r F) :
138     degreeEquiv K s
139         (quotientEquivUnramified r F K s hF (QuotientGroup.mk w)) =
140       degree r F w := by
141   simp [quotientEquivUnramified]
142 
143 /-- Every ramified Frobenius lift of degree one maps to the distinguished
144 geometric Frobenius lift of the unramified model. -/
145 theorem degreeModelMap_eq_geometricLift_of_degree_one
146     {w : Pullback r F}
147     (hw : degree r F w = Multiplicative.ofAdd (1 : ℤ)) :
148     degreeModelMap r F K s w = geometricLift K s := by
149   apply (degreeEquiv K s).injective
150   rw [degreeModelMap_degree, hw, degreeEquiv_apply, degree_geometricLift]
151 
152 section Representations
153 
154 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
155 
156 /-- Pull a representation of the inertia-free model back through integer
157 degree.  This deliberately forgets every ramification coordinate. -/
158 def pullbackDegreeRepresentation
159     (σ : Representation ℂ (UnramifiedWeil K s) V) :
160     Representation ℂ (Pullback r F) V :=
161   σ.comp (degreeModelMap r F K s)
162 
163 /-- A degree-only pullback is trivial on inertia. -/
164 theorem inertia_le_pullbackDegreeRepresentation_ker
165     (σ : Representation ℂ (UnramifiedWeil K s) V) :
166     Inertia r F ≤ (pullbackDegreeRepresentation r F K s σ).ker := by
167   intro w hw
168   change σ (degreeModelMap r F K s w) = 1
169   have hd : degree r F w = 1 := hw
170   apply LinearMap.ext
171   intro v
172   simp [degreeModelMap, hd]
173 
174 /-- Any representation trivial on inertia descends first to the quotient. -/
175 noncomputable def quotientRepresentation
176     (ρ : Representation ℂ (Pullback r F) V)
177     (hI : Inertia r F ≤ ρ.ker) :
178     Representation ℂ (Pullback r F ⧸ Inertia r F) V :=
179   QuotientGroup.lift (Inertia r F) ρ hI
180 
181 /-- Under a degree-one lift, an inertia-trivial representation descends to the
182 current unramified integer-degree model. -/
183 noncomputable def descendRepresentation
184     (hF : F ∈ r.range)
185     (ρ : Representation ℂ (Pullback r F) V)
186     (hI : Inertia r F ≤ ρ.ker) :
187     Representation ℂ (UnramifiedWeil K s) V :=
188   (quotientRepresentation r F ρ hI).comp
189     (quotientEquivUnramified r F K s hF).symm.toMonoidHom
190 
191 /-- Pulling the descended representation back recovers the original one. -/
192 theorem descendRepresentation_comp_degreeModelMap
193     (hF : F ∈ r.range)
194     (ρ : Representation ℂ (Pullback r F) V)
195     (hI : Inertia r F ≤ ρ.ker) :
196     (descendRepresentation r F K s hF ρ hI).comp
197         (degreeModelMap r F K s) = ρ := by
198   apply MonoidHom.ext
199   intro w
200   apply LinearMap.ext
201   intro v
202   let e := quotientEquivUnramified r F K s hF
203   have heU : e (QuotientGroup.mk w) = degreeModelMap r F K s w := by
204     apply (degreeEquiv K s).injective
205     rw [quotientEquivUnramified_mk_degree, degreeModelMap_degree]
206   have heQ : e.symm (degreeModelMap r F K s w) = QuotientGroup.mk w := by
207     rw [← heU]
208     exact e.symm_apply_apply _
209   change (quotientRepresentation r F ρ hI
210       (e.symm (degreeModelMap r F K s w))) v = ρ w v
211   rw [heQ]
212   rfl
213 
214 /-- Descent to the current degree model is unique. -/
215 theorem descendRepresentation_unique
216     (hF : F ∈ r.range)
217     (ρ : Representation ℂ (Pullback r F) V)
218     (hI : Inertia r F ≤ ρ.ker)
219     (σ : Representation ℂ (UnramifiedWeil K s) V)
220     (hσ : σ.comp (degreeModelMap r F K s) = ρ) :
221     σ = descendRepresentation r F K s hF ρ hI := by
222   apply MonoidHom.ext
223   intro u
224   apply LinearMap.ext
225   intro v
226   obtain ⟨w, rfl⟩ := degreeModelMap_surjective r F K s hF u
227   have hleft := congrArg (fun τ : Representation ℂ (Pullback r F) V => τ w v) hσ
228   have hright := congrArg
229     (fun τ : Representation ℂ (Pullback r F) V => τ w v)
230     (descendRepresentation_comp_degreeModelMap r F K s hF ρ hI)
231   exact hleft.trans hright.symm
232 
233 end Representations
234 end CurrentDegreeModel
235 
236 section PolyphaseCollapse
237 
238 variable (R D : Type*) [CommRing R] [IsLocalRing R]
239   [Group D] [Fintype D] [MulSemiringAction D R]
240 variable (F : RingAut (IsLocalRing.ResidueField R))
241 
242 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
243   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
244 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
245   [FiniteDimensional 𝓀[K] s]
246 
247 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
248 variable (σ : Representation ℂ (UnramifiedWeil K s) V)
249 
250 abbrev degreeOnlyRepresentation :
251     Representation ℂ (Pullback (residue R D) F) V :=
252   pullbackDegreeRepresentation (residue R D) F K s σ
253 
254 omit [Fintype D] in
255 /-- Every lower ramification element acts trivially after passing through the
256 degree-only quotient. -/
257 theorem degreeOnlyRepresentation_lift_eq_one
258     (i : ℕ) (g : lower R D i) :
259     degreeOnlyRepresentation R D F K s σ (lift R D F i g) = 1 := by
260   have hmap : degreeModelMap (residue R D) F K s (lift R D F i g) = 1 := by
261     apply (degreeEquiv K s).injective
262     rw [degreeModelMap_degree, lift_degree]
263     simp
264   change σ (degreeModelMap (residue R D) F K s (lift R D F i g)) = 1
265   rw [hmap]
266   exact map_one σ
267 
268 omit [Fintype D] in
269 /-- Every lower fixed space becomes the whole representation space after the
270 inertia quotient. -/
271 theorem degreeOnly_fixed_eq_top (i : ℕ) :
272     fixed R D F (degreeOnlyRepresentation R D F K s σ) i = ⊤ := by
273   apply top_unique
274   intro v _ g
275   change degreeOnlyRepresentation R D F K s σ (lift R D F i g) v = v
276   rw [degreeOnlyRepresentation_lift_eq_one]
277   rfl
278 
279 /-- Every depth averaging projector becomes the identity. -/
280 theorem degreeOnly_depthProjector_eq_id (i : ℕ) :
281     depthProjector (R := R) (D := D) (F := F)
282       (ρ := degreeOnlyRepresentation R D F K s σ) i = LinearMap.id := by
283   ext v
284   exact fixes _ (by
285     intro g
286     change degreeOnlyRepresentation R D F K s σ (lift R D F i g) v = v
287     rw [degreeOnlyRepresentation_lift_eq_one]
288     rfl)
289 
290 /-- Every positive ramification detail channel is erased by the inertia-free
291 quotient. -/
292 theorem degreeOnly_detailProjector_eq_zero (i : ℕ) :
293     detailProjector (R := R) (D := D) (F := F)
294       (ρ := degreeOnlyRepresentation R D F K s σ) i = 0 := by
295   unfold detailProjector
296   rw [degreeOnly_depthProjector_eq_id, degreeOnly_depthProjector_eq_id]
297   exact sub_self _
298 
299 /-- Every lower-numbering conductor summand vanishes after quotienting by
300 inertia. -/
301 theorem degreeOnly_summand_eq_zero (i : ℕ) :
302     summand R D F (degreeOnlyRepresentation R D F K s σ) i = 0 := by
303   unfold summand codimension
304   rw [degreeOnly_fixed_eq_top]
305   simp
306 
307 /-- The Swan conductor vanishes on the degree-only quotient. -/
308 theorem degreeOnly_swan_eq_zero :
309     swan R D F (degreeOnlyRepresentation R D F K s σ) = 0 := by
310   unfold swan
311   simp only [degreeOnly_summand_eq_zero, tsum_zero]
312 
313 /-- The Artin conductor vanishes on the degree-only quotient. -/
314 theorem degreeOnly_artin_eq_zero :
315     artin R D F (degreeOnlyRepresentation R D F K s σ) = 0 := by
316   unfold artin codimension
317   rw [degreeOnly_fixed_eq_top, degreeOnly_swan_eq_zero]
318   simp
319 
320 end PolyphaseCollapse
321 
322 end PaperXI.RamifiedUnramifiedQuotient

Back to source controls