FiniteUnramifiedWeil.lean

1 import PaperXI.ResidueFrobeniusAttachment
2 import PaperXI.ResidueDegreeBaseChange
3 import Mathlib.RepresentationTheory.Irreducible
4 
5 /-! # Finite unramified Weil quotient of the constructed local field -/
6 
7 set_option autoImplicit false
8 noncomputable section
9 
10 namespace PaperXI.FiniteUnramifiedWeil
11 
12 open PaperXI.LocalFieldResidueExtension
13 open PaperXI.IntegerRingComparison
14 open PaperXI.ResidueWeil
15 open PaperXI.ResidueDegreeBaseChange
16 open ValuativeRel
17 open scoped Classical
18 
19 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
20   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
21 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
22   [FiniteDimensional 𝓀[K] s]
23 
24 /-- The integer-degree unramified Weil model attached to the actual residue
25 Galois group and geometric Frobenius. -/
26 abbrev UnramifiedWeil :=
27   Pullback (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
28 
29 /-- Its degree is an exact group equivalence with the infinite cyclic group. -/
30 noncomputable def degreeEquiv :
31     UnramifiedWeil K s ≃* Multiplicative ℤ where
32   toFun := degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
33   invFun n :=
34     ⟨((geometricFrobenius K s) ^ Multiplicative.toAdd n, n), rfl⟩
35   left_inv w := by
36     apply Subtype.ext
37     apply Prod.ext
38     · exact w.property.symm
39     · rfl
40   right_inv n := rfl
41   map_mul' _ _ := rfl
42 
43 @[simp]
44 theorem degreeEquiv_apply (w : UnramifiedWeil K s) :
45     degreeEquiv K s w = degree (MonoidHom.id (ResidueGalois K s))
46       (geometricFrobenius K s) w :=
47   rfl
48 
49 /-- Projection is exactly the geometric Frobenius power prescribed by degree. -/
50 theorem projection_eq_geometric_zpow_degree (w : UnramifiedWeil K s) :
51     projection (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w =
52       geometricFrobenius K s ^ Multiplicative.toAdd
53         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) := by
54   exact w.property
55 
56 /-- The degree map is bijective; this model retains the full integer degree. -/
57 theorem degree_bijective : Function.Bijective
58     (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)) :=
59   (degreeEquiv K s).bijective
60 
61 /-- Inertia in the unramified Weil model is trivial. -/
62 theorem inertia_eq_bot :
63     (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)).ker = ⊥ := by
64   exact (MonoidHom.ker_eq_bot_iff _).2 (degreeEquiv K s).injective
65 
66 /-- The canonical degree-one lift of geometric Frobenius. -/
67 noncomputable def geometricLift : UnramifiedWeil K s :=
68   (degreeEquiv K s).symm (Multiplicative.ofAdd 1)
69 
70 @[simp]
71 theorem degree_geometricLift :
72     degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
73       (geometricLift K s) = Multiplicative.ofAdd 1 :=
74   (degreeEquiv K s).apply_symm_apply _
75 
76 @[simp]
77 theorem projection_geometricLift :
78     projection (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
79       (geometricLift K s) = geometricFrobenius K s := by
80   rw [projection_eq_geometric_zpow_degree, degree_geometricLift]
81   simp
82 
83 /-- The inverse lift is arithmetic Frobenius and has degree minus one. -/
84 noncomputable def arithmeticLift : UnramifiedWeil K s :=
85   (geometricLift K s)⁻¹
86 
87 @[simp]
88 theorem degree_arithmeticLift :
89     degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
90       (arithmeticLift K s) = Multiplicative.ofAdd (-1 : ℤ) := by
91   rw [arithmeticLift, map_inv, degree_geometricLift]
92   rfl
93 
94 @[simp]
95 theorem projection_arithmeticLift :
96     projection (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
97       (arithmeticLift K s) = arithmeticFrobenius K s := by
98   rw [arithmeticLift, map_inv, projection_geometricLift]
99   simp [geometricFrobenius]
100 
101 
102 /-- Every element of the integer-degree model is the corresponding integral
103 power of the distinguished geometric-Frobenius lift. -/
104 theorem eq_geometricLift_zpow_degree (w : UnramifiedWeil K s) :
105     w = geometricLift K s ^ Multiplicative.toAdd
106       (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) := by
107   calc
108     w = (degreeEquiv K s).symm ((degreeEquiv K s) w) :=
109       ((degreeEquiv K s).symm_apply_apply w).symm
110     _ = (degreeEquiv K s).symm (Multiplicative.ofAdd 1) ^
111         Multiplicative.toAdd ((degreeEquiv K s) w) :=
112       MonoidHom.apply_mint (UnramifiedWeil K s)
113         (degreeEquiv K s).symm.toMonoidHom ((degreeEquiv K s) w)
114     _ = geometricLift K s ^ Multiplicative.toAdd
115         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) := rfl
116 
117 /-- The geometric-Frobenius lift generates the whole unramified Weil model. -/
118 theorem geometricLift_zpowers_eq_top :
119     Subgroup.zpowers (geometricLift K s) = ⊤ := by
120   rw [Subgroup.eq_top_iff']
121   intro w
122   rw [Subgroup.mem_zpowers_iff]
123   exact ⟨Multiplicative.toAdd
124     (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w),
125       (eq_geometricLift_zpow_degree K s w).symm⟩
126 
127 /-- The integer-degree unramified Weil model is commutative. -/
128 instance unramifiedWeil_isMulCommutative : IsMulCommutative (UnramifiedWeil K s) :=
129   ⟨⟨fun a b => by
130     apply (degreeEquiv K s).injective
131     exact mul_comm _ _⟩⟩
132 
133 open scoped IsMulCommutative in
134 /-- Every finite-dimensional irreducible complex representation of this
135 unramified model is one-dimensional. -/
136 theorem irreducible_finrank_eq_one {V : Type*} [AddCommGroup V] [Module ℂ V]
137     [FiniteDimensional ℂ V]
138     (ρ : Representation ℂ (UnramifiedWeil K s) V) [Representation.IsIrreducible ρ] :
139     Module.finrank ℂ V = 1 := by
140   exact Representation.IsIrreducible.finrank_eq_one_of_isMulCommutative ρ
141 
142 
143 /-- Projection from the infinite-degree model onto the residue Galois group is surjective. -/
144 theorem projection_surjective : Function.Surjective
145     (projection (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)) := by
146   intro σ
147   have hσ : σ ∈ Subgroup.zpowers (geometricFrobenius K s) := by
148     rw [geometricFrobenius_zpowers_eq_top K s]
149     trivial
150   obtain ⟨m, hm⟩ := Subgroup.mem_zpowers_iff.mp hσ
151   refine ⟨⟨(σ, Multiplicative.ofAdd m), ?_⟩, rfl⟩
152   change σ = geometricFrobenius K s ^ m
153   exact hm.symm
154 
155 /-- The projection kernel consists exactly of degrees divisible by the residue degree. -/
156 theorem projection_ker_eq_period :
157     (projection (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)).ker =
158       periodSubgroup (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
159         (ResidueDegree K s) := by
160   ext w
161   constructor
162   · intro hw
163     change projection (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w = 1 at hw
164     have hpow : geometricFrobenius K s ^ Multiplicative.toAdd
165         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) = 1 := by
166       rw [← projection_eq_geometric_zpow_degree K s]
167       exact hw
168     have hd : (orderOf (geometricFrobenius K s) : ℤ) ∣ Multiplicative.toAdd
169         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) :=
170       (orderOf_dvd_iff_zpow_eq_one).2 hpow
171     apply (mem_periodSubgroup _ _ _ _).2
172     simpa only [geometricFrobenius_order_eq_fieldDegree K s] using hd
173   · intro hw
174     have hd : (ResidueDegree K s : ℤ) ∣ Multiplicative.toAdd
175         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) :=
176       (mem_periodSubgroup _ _ _ _).1 hw
177     have hd' : (orderOf (geometricFrobenius K s) : ℤ) ∣ Multiplicative.toAdd
178         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) := by
179       simpa only [geometricFrobenius_order_eq_fieldDegree K s] using hd
180     have hpow : geometricFrobenius K s ^ Multiplicative.toAdd
181         (degree (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w) = 1 :=
182       (orderOf_dvd_iff_zpow_eq_one).1 hd'
183     change projection (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s) w = 1
184     rw [projection_eq_geometric_zpow_degree K s]
185     exact hpow
186 
187 /-- Quotienting the infinite-degree model by one residue period gives the actual
188 residue Galois group. -/
189 noncomputable def finiteResidueQuotientEquiv :
190     UnramifiedWeil K s ⧸
191       periodSubgroup (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
192         (ResidueDegree K s) ≃* ResidueGalois K s :=
193   (quotientEquiv (MonoidHom.id (ResidueGalois K s)) (geometricFrobenius K s)
194       (ResidueDegree K s) ⟨geometricFrobenius K s, rfl⟩).trans
195     (geometricCycleEquiv K s)
196 
197 
198 end PaperXI.FiniteUnramifiedWeil

Back to source controls