NormalizerDictionary110.lean

1 import PaperXI.ActualCharacterIdentification61
2 import PaperXI.ActualCharacterResidue61
3 import PaperXI.ActualCuspidalCandidate105
4 
5 /-! Conditional character-normalizer dictionary, followed by literal instances.
6 No canonical simple-stratum group is introduced or identified by assumption. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.NormalizerDictionary110
10 
11 section Groups
12 variable {G : Type*} [Group G]
13 variable (N U₀ U₁ J₁ B : Subgroup G) (I : Set G)
14 
15 /-- Cancellation inside U₁ identifies the normalizer intersection from support. -/
16 theorem inf_eq_of_support
17     (hJ : J₁ ≤ U₁) (hJN : J₁ ≤ N)
18     (hNI : ∀ g, g ∈ N → g ∈ I)
19     (hI : ∀ g, g ∈ I → ∃ a : J₁, ∃ b : B, ∃ c : J₁,
20       (a : G) * (b : G) * (c : G) = g)
21     (hBU : B ⊓ U₁ ≤ J₁) : N ⊓ U₁ = J₁ := by
22   apply le_antisymm
23   · intro g hg
24     obtain ⟨a, b, c, he⟩ := hI g (hNI g hg.1)
25     have hb : (b : G) = (a : G)⁻¹ * g * (c : G)⁻¹ := by
26       rw [← he]
27       group
28     have hbU : (b : G) ∈ U₁ := by
29       rw [hb]
30       exact U₁.mul_mem (U₁.mul_mem (U₁.inv_mem (hJ a.property)) hg.2)
31         (U₁.inv_mem (hJ c.property))
32     rw [← he]
33     exact J₁.mul_mem (J₁.mul_mem a.property (hBU ⟨b.property, hbU⟩)) c.property
34   · exact le_inf hJN hJ
35 
36 /-- The compact intersection is the join of its integral centralizer and J₁. -/
37 theorem compact_eq_sup_of_support
38     (hU : U₁ ≤ U₀) (hJ : J₁ ≤ U₁) (hJN : J₁ ≤ N)
39     (hNI : ∀ g, g ∈ N → g ∈ I)
40     (hI : ∀ g, g ∈ I → ∃ a : J₁, ∃ b : B, ∃ c : J₁,
41       (a : G) * (b : G) * (c : G) = g)
42     (hB₀ : B ⊓ U₀ ≤ N) : N ⊓ U₀ = (B ⊓ U₀) ⊔ J₁ := by
43   apply le_antisymm
44   · intro g hg
45     obtain ⟨a, b, c, he⟩ := hI g (hNI g hg.1)
46     have hb : (b : G) = (a : G)⁻¹ * g * (c : G)⁻¹ := by
47       rw [← he]
48       group
49     have hbU : (b : G) ∈ U₀ := by
50       rw [hb]
51       exact U₀.mul_mem (U₀.mul_mem (U₀.inv_mem (hU (hJ a.property))) hg.2)
52         (U₀.inv_mem (hU (hJ c.property)))
53     rw [← he]
54     exact ((B ⊓ U₀) ⊔ J₁).mul_mem
55       (((B ⊓ U₀) ⊔ J₁).mul_mem (Subgroup.mem_sup_right a.property)
56         (Subgroup.mem_sup_left ⟨b.property, hbU⟩))
57       (Subgroup.mem_sup_right c.property)
58   · exact sup_le (le_inf hB₀ inf_le_right) (le_inf hJN (hJ.trans hU))
59 
60 /-- U₁ normal in U₀ implies its normalizer intersection is normal in the compact part. -/
61 theorem compact_le_normalizer_inf (hnormal : U₀ ≤ Subgroup.normalizer (U₁ : Set G)) :
62     N ⊓ U₀ ≤ Subgroup.normalizer ((N ⊓ U₁ : Subgroup G) : Set G) :=
63   (inf_le_inf N.le_normalizer hnormal).trans Subgroup.inf_normalizer_le_normalizer_inf
64 
65 /-- After the dictionary equality, normalization of J₁ requires no extra arithmetic axiom. -/
66 theorem compact_le_normalizer_of_inf_eq
67     (hnormal : U₀ ≤ Subgroup.normalizer (U₁ : Set G)) (he : N ⊓ U₁ = J₁) :
68     N ⊓ U₀ ≤ Subgroup.normalizer (J₁ : Set G) := by
69   rw [← he]
70   exact compact_le_normalizer_inf N U₀ U₁ hnormal
71 
72 /-- A product presentation follows from U₁ normality and the support dictionary. -/
73 theorem mem_compact_iff_product
74     (hU : U₁ ≤ U₀) (hJ : J₁ ≤ U₁) (hJN : J₁ ≤ N)
75     (hNI : ∀ g, g ∈ N → g ∈ I)
76     (hI : ∀ g, g ∈ I → ∃ a : J₁, ∃ b : B, ∃ c : J₁,
77       (a : G) * (b : G) * (c : G) = g)
78     (hBU : B ⊓ U₁ ≤ J₁) (hB₀ : B ⊓ U₀ ≤ N)
79     (hnormal : U₀ ≤ Subgroup.normalizer (U₁ : Set G)) (g : G) :
80     g ∈ N ⊓ U₀ ↔ ∃ b : (B ⊓ U₀ : Subgroup G), ∃ j : J₁, (b : G) * (j : G) = g := by
81   have he := inf_eq_of_support N U₁ J₁ B I hJ hJN hNI hI hBU
82   have hn := compact_le_normalizer_of_inf_eq N U₀ U₁ J₁ hnormal he
83   constructor
84   · intro hg
85     obtain ⟨a, b, c, habc⟩ := hI g (hNI g hg.1)
86     have hb : (b : G) = (a : G)⁻¹ * g * (c : G)⁻¹ := by
87       rw [← habc]
88       group
89     have hbU : (b : G) ∈ U₀ := by
90       rw [hb]
91       exact U₀.mul_mem (U₀.mul_mem (U₀.inv_mem (hU (hJ a.property))) hg.2)
92         (U₀.inv_mem (hU (hJ c.property)))
93     have hbN : (b : G) ∈ N := hB₀ ⟨b.property, hbU⟩
94     have hbinv : (b : G)⁻¹ ∈ Subgroup.normalizer (J₁ : Set G) :=
95       hn ⟨N.inv_mem hbN, U₀.inv_mem hbU⟩
96     have hj : (b : G)⁻¹ * (a : G) * (b : G) * (c : G) ∈ J₁ := by
97       apply J₁.mul_mem _ c.property
98       simpa only [inv_inv] using
99         (Subgroup.mem_normalizer_iff.mp hbinv (a : G)).mp a.property
100     refine ⟨⟨b, ⟨b.property, hbU⟩⟩, ⟨_, hj⟩, ?_⟩
101     change (b : G) * ((b : G)⁻¹ * (a : G) * (b : G) * (c : G)) = g
102     rw [← habc]
103     group
104   · rintro ⟨b, j, rfl⟩
105     exact ⟨N.mul_mem (hB₀ b.property) (hJN j.property),
106       U₀.mul_mem b.property.2 (hU (hJ j.property))⟩
107 
108 end Groups
109 
110 section Actual
111 open Matrix ValuativeRel ActualCharacterType61 ActualELatticeTopology60
112 open ActualELatticeNormalizer59 ActualELatticeTypeGroup59 LatticeCongruenceTopology60
113 open ActualELatticeResidue59
114 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
115   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
116   [IsNonarchimedeanLocalField E] [Algebra F E]
117 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
118   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
119   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
120 
121 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
122 /-- Actual U₁ normality is proved from the original chain, independently of hmodel. -/
123 theorem chainGroup_le_normalizer_congruence :
124     chainGroup F E m n e ≤ Subgroup.normalizer (matrixCongruence F E m n e : Set (GL n F)) := by
125   intro g hg
126   apply Subgroup.mem_normalizer_iff.mpr
127   intro x
128   change coordinateAut e x ∈ firstCongruence (latticeChain F E m) ↔
129     coordinateAut e (g * x * g⁻¹) ∈ firstCongruence (latticeChain F E m)
130   rw [map_mul, map_mul, map_inv]
131   exact Subgroup.mem_normalizer_iff.mp
132     (stabilizer_normalizes_firstCongruence (latticeChain F E m) hg) (coordinateAut e x)
133 
134 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
135 /-- The actual first subgroup's ambient image is literally N(theta) intersect U₁. -/
136 theorem firstSubgroup_ambient_image :
137     (firstSubgroup F E m n e D θ).map (compactGroup F E m n e D θ).subtype =
138       CharacterNormalizer61.normalizer D θ ⊓ matrixCongruence F E m n e := by
139   rw [firstSubgroup, Subgroup.subgroupOf_map_subtype]
140   change matrixCongruence F E m n e ⊓
141     (CharacterNormalizer61.normalizer D θ ⊓ chainGroup F E m n e) = _
142   apply le_antisymm
143   · exact fun _ h => ⟨h.2.1, h.1⟩
144   · exact fun _ h => ⟨h.2, h.1, matrixCongruence_le_chainGroup F E m n e h.2⟩
145 
146 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
147 /-- The embedding used in ActualIntersection108 has this same literal ambient range. -/
148 theorem firstSubgroup_embedding_range :
149     ((compactGroup F E m n e D θ).subtype.comp
150       (firstSubgroup F E m n e D θ).subtype).range =
151       CharacterNormalizer61.normalizer D θ ⊓ matrixCongruence F E m n e := by
152   rw [MonoidHom.range_comp, Subgroup.range_subtype]
153   exact firstSubgroup_ambient_image F E m n e D θ
154 
155 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
156 /-- Actual first-subgroup normality follows from chain congruence, without a residue model. -/
157 theorem firstSubgroup_normal : (firstSubgroup F E m n e D θ).Normal := by
158   apply Subgroup.normal_subgroupOf_iff_le_normalizer_inf.mpr
159   change compactGroup F E m n e D θ ≤ Subgroup.normalizer
160     (matrixCongruence F E m n e ⊓ compactGroup F E m n e D θ : Set (GL n F))
161   have hn := compact_le_normalizer_inf (CharacterNormalizer61.normalizer D θ)
162     (chainGroup F E m n e) (matrixCongruence F E m n e)
163     (chainGroup_le_normalizer_congruence F E m n e)
164   rw [← firstSubgroup_ambient_image F E m n e D θ,
165     firstSubgroup, Subgroup.subgroupOf_map_subtype] at hn
166   exact hn
167 
168 /-- The literal integral centralizer in the same ambient matrix coordinates. -/
169 def integralCentralizer : Subgroup (GL n F) :=
170   (ActualELatticeResidue59.integralImage F E m).comap (coordinateAut e).toMonoidHom
171 
172 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
173 /-- The actual lattice type is exactly its integral centralizer joined with U₁. -/
174 theorem matrixType_eq_integral_sup :
175     matrixType F E m n e = integralCentralizer F E m n e ⊔ matrixCongruence F E m n e := by
176   change ((ActualELatticeResidue59.integralImage F E m ⊔
177     ActualELatticeTypeGroup59.congruence F E m).comap (coordinateAut e).toMonoidHom) = _
178   exact (coordinateAut e).comapSubgroup.map_sup _ _
179 
180 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
181 /-- Integral centralizer matrices preserve the original full periodic chain. -/
182 theorem integralCentralizer_le_chainGroup :
183     integralCentralizer F E m n e ≤ chainGroup F E m n e := by
184   intro g hg
185   obtain ⟨b, hb⟩ := hg
186   change ActualELatticeResidue59.integralMatrix F E m b = coordinateAut e g at hb
187   change coordinateAut e g ∈ chainStabilizer (latticeChain F E m)
188   rw [← hb]
189   exact integralMatrix_mem_stabilizer F E m b
190 
191 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [IsNonarchimedeanLocalField E] [Nonempty n] in
192 /-- The existing integral pair-normalization premise supplies actual B₀≤N(theta). -/
193 theorem integralCentralizer_le_character_normalizer
194     (hB : ∀ b : GL m 𝒪[E], (coordinateAut e).symm
195       (ActualELatticeResidue59.integralMatrix F E m b) ∈ CharacterNormalizer61.normalizer D θ) :
196     integralCentralizer F E m n e ≤ CharacterNormalizer61.normalizer D θ := by
197   intro g hg
198   obtain ⟨b, hb⟩ := hg
199   have he : g = (coordinateAut e).symm (ActualELatticeResidue59.integralMatrix F E m b) := by
200     apply (coordinateAut e).injective
201     rw [MulEquiv.apply_symm_apply]
202     exact hb.symm
203   rw [he]
204   exact hB b
205 
206 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
207   [Fintype n] [DecidableEq n] [Nonempty n] in
208 /-- An extension-linear matrix preserves the chain exactly when it and its inverse are integral. -/
209 theorem restrict_mem_chain_iff (g : GL m E) :
210     restrictScalarMatrix F E m g ∈ chainStabilizer (latticeChain F E m) ↔
211     g ∈ ActualIntegralGeneralLinear.integralSubgroup E m := by
212   have single_mem (j : m) : Pi.single j (1 : E) ∈ integralLattice E m := by
213     intro i
214     simp only [Pi.single_apply]
215     split_ifs <;> simp
216   have entries (a : GL m E)
217       (ha : restrictScalarMatrix F E m a ∈ chainStabilizer (latticeChain F E m)) :
218       ∀ i j, a i j ∈ (valuation E).integer := by
219     intro i j
220     have hv := (ha 0 (Pi.single j 1)).mpr (by simpa using single_mem j)
221     rw [latticeChain_zero] at hv
222     have hi := hv i
223     simpa [restrictScalarMatrix_apply, Matrix.mulVec, dotProduct, Pi.single_apply] using hi
224   constructor
225   · intro hg
226     apply (ActualIntegralGeneralLinear.mem_integralSubgroup E m g).mpr
227     refine ⟨entries g hg, entries g⁻¹ ?_⟩
228     simpa only [map_inv] using (chainStabilizer (latticeChain F E m)).inv_mem hg
229   · rintro ⟨u, rfl⟩
230     exact integralMatrix_mem_stabilizer F E m u
231 
232 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
233 /-- The full literal field centralizer intersects the chain group in its integral image. -/
234 theorem centralizer_inf_chain :
235     (ActualCuspidalCandidate105.centralizerMap F E m n e).range ⊓
236       chainGroup F E m n e = integralCentralizer F E m n e := by
237   ext g
238   constructor
239   · rintro ⟨⟨y, hy⟩, h0⟩
240     have hcoord : restrictScalarMatrix F E m y = coordinateAut e g := by
241       have h := congrArg (coordinateAut e) hy
242       change coordinateAut e ((coordinateAut e).symm (restrictScalarMatrix F E m y)) =
243         coordinateAut e g at h
244       rwa [MulEquiv.apply_symm_apply] at h
245     have hy0 : restrictScalarMatrix F E m y ∈ chainStabilizer (latticeChain F E m) := by
246       rw [hcoord]
247       exact h0
248     obtain ⟨u, hu⟩ := (restrict_mem_chain_iff F E m y).mp hy0
249     change coordinateAut e g ∈ integralImage F E m
250     refine ⟨u, ?_⟩
251     change restrictScalarMatrix F E m (ActualIntegralGeneralLinear.embedding E m u) =
252       coordinateAut e g
253     rw [hu, hcoord]
254   · intro hg
255     obtain ⟨u, hu⟩ := hg
256     change integralMatrix F E m u = coordinateAut e g at hu
257     constructor
258     · refine ⟨ActualIntegralGeneralLinear.embedding E m u, ?_⟩
259       apply (coordinateAut e).injective
260       change coordinateAut e ((coordinateAut e).symm
261         (restrictScalarMatrix F E m (ActualIntegralGeneralLinear.embedding E m u))) =
262         coordinateAut e g
263       rw [MulEquiv.apply_symm_apply]
264       exact hu
265     · change coordinateAut e g ∈ chainStabilizer (latticeChain F E m)
266       rw [← hu]
267       exact integralMatrix_mem_stabilizer F E m u
268 
269 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
270 /-- Its intersection with full chain congruence is the explicit transported residue kernel. -/
271 theorem centralizer_inf_congruence :
272     (ActualCuspidalCandidate105.centralizerMap F E m n e).range ⊓
273       matrixCongruence F E m n e =
274     (ActualResidueGeneralLinear.reduction E m).ker.map
275       ((ActualCuspidalCandidate105.centralizerMap F E m n e).comp
276         (ActualIntegralGeneralLinear.embedding E m)) := by
277   ext g
278   constructor
279   · intro hg
280     have h0 : g ∈ integralCentralizer F E m n e := by
281       rw [← centralizer_inf_chain F E m n e]
282       exact ⟨hg.1, matrixCongruence_le_chainGroup F E m n e hg.2⟩
283     obtain ⟨u, hu⟩ := h0
284     change integralMatrix F E m u = coordinateAut e g at hu
285     have hu1 : integralMatrix F E m u ∈ ActualELatticeTypeGroup59.congruence F E m := by
286       rw [hu]
287       exact hg.2
288     refine ⟨u, (integralMatrix_mem_congruence_iff F E m u).mp hu1, ?_⟩
289     apply (coordinateAut e).injective
290     change coordinateAut e ((coordinateAut e).symm
291       (restrictScalarMatrix F E m (ActualIntegralGeneralLinear.embedding E m u))) =
292       coordinateAut e g
293     rw [MulEquiv.apply_symm_apply]
294     exact hu
295   · rintro ⟨u, hu, hug⟩
296     constructor
297     · exact ⟨ActualIntegralGeneralLinear.embedding E m u, hug⟩
298     · have hcoord : integralMatrix F E m u = coordinateAut e g := by
299         have h := congrArg (coordinateAut e) hug
300         change coordinateAut e ((coordinateAut e).symm
301           (restrictScalarMatrix F E m (ActualIntegralGeneralLinear.embedding E m u))) =
302           coordinateAut e g at h
303         rwa [MulEquiv.apply_symm_apply] at h
304       change coordinateAut e g ∈ ActualELatticeTypeGroup59.congruence F E m
305       rw [← hcoord]
306       exact (integralMatrix_mem_congruence_iff F E m u).mpr hu
307 
308 variable (J₁ B : Subgroup (GL n F))
309 variable (hJ : J₁ ≤ matrixCongruence F E m n e)
310   (hJN : J₁ ≤ CharacterNormalizer61.normalizer D θ)
311   (hθsupport : ∀ g : GL n F,
312     NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
313     ∃ a : J₁, ∃ b : B, ∃ c : J₁, (a : GL n F) * (b : GL n F) * (c : GL n F) = g)
314 include hJ hJN hθsupport
315 
316 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
317 /-- The actual image dictionary uses the proved normalizer-to-character-support implication. -/
318 theorem actual_first_eq
319     (hBU : B ⊓ matrixCongruence F E m n e ≤ J₁) :
320     (firstSubgroup F E m n e D θ).map (compactGroup F E m n e D θ).subtype = J₁ := by
321   rw [firstSubgroup_ambient_image F E m n e D θ]
322   exact inf_eq_of_support (CharacterNormalizer61.normalizer D θ)
323     (matrixCongruence F E m n e) J₁ B
324     {g | NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g}
325     hJ hJN (fun _ hg => CharacterNormalizer61.character_intertwinedAt D θ hg) hθsupport hBU
326 
327 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
328 /-- The image dictionary also identifies the subgroup inside the original compact carrier. -/
329 theorem actual_first_subgroup_eq
330     (hBU : B ⊓ matrixCongruence F E m n e ≤ J₁) :
331     firstSubgroup F E m n e D θ = J₁.subgroupOf (compactGroup F E m n e D θ) := by
332   have hJC : J₁ ≤ compactGroup F E m n e D θ :=
333     le_inf hJN (hJ.trans (matrixCongruence_le_chainGroup F E m n e))
334   apply Subgroup.map_injective (compactGroup F E m n e D θ).subtype_injective
335   rw [actual_first_eq F E m n e D θ J₁ B hJ hJN hθsupport hBU,
336     Subgroup.map_subgroupOf_eq_of_le hJC]
337 
338 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
339 /-- Compact-group equality is derived from support and integral centralizer normalization. -/
340 theorem actual_compact_eq_sup
341     (hB₀ : B ⊓ chainGroup F E m n e ≤ CharacterNormalizer61.normalizer D θ) :
342     compactGroup F E m n e D θ = (B ⊓ chainGroup F E m n e) ⊔ J₁ :=
343   compact_eq_sup_of_support (CharacterNormalizer61.normalizer D θ)
344     (chainGroup F E m n e) (matrixCongruence F E m n e) J₁ B
345     {g | NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g}
346     (matrixCongruence_le_chainGroup F E m n e) hJ hJN
347     (fun _ hg => CharacterNormalizer61.character_intertwinedAt D θ hg) hθsupport hB₀
348 
349 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m] [Nonempty n] in
350 /-- The support dictionary and actual U₁ normality yield the compact product formula. -/
351 theorem actual_compact_product
352     (hBU : B ⊓ matrixCongruence F E m n e ≤ J₁)
353     (hB₀ : B ⊓ chainGroup F E m n e ≤ CharacterNormalizer61.normalizer D θ)
354     (g : GL n F) :
355     g ∈ compactGroup F E m n e D θ ↔
356       ∃ b : (B ⊓ chainGroup F E m n e : Subgroup (GL n F)),
357       ∃ j : J₁, (b : GL n F) * (j : GL n F) = g :=
358   mem_compact_iff_product (CharacterNormalizer61.normalizer D θ)
359     (chainGroup F E m n e) (matrixCongruence F E m n e) J₁ B
360     {g | NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g}
361     (matrixCongruence_le_chainGroup F E m n e) hJ hJN
362     (fun _ hg => CharacterNormalizer61.character_intertwinedAt D θ hg) hθsupport hBU hB₀
363     (chainGroup_le_normalizer_congruence F E m n e) g
364 
365 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
366 /-- The lattice-product containment hmodel follows once the actual integral factor is identified. -/
367 theorem actual_model_le
368     (hB₀ : B ⊓ chainGroup F E m n e ≤ CharacterNormalizer61.normalizer D θ)
369     (hBtype : B ⊓ chainGroup F E m n e ≤ matrixType F E m n e) :
370     compactGroup F E m n e D θ ≤ matrixType F E m n e := by
371   rw [actual_compact_eq_sup F E m n e D θ J₁ B hJ hJN hθsupport hB₀]
372   apply sup_le hBtype
373   exact hJ.trans (fun _ hg =>
374     (show ActualELatticeTypeGroup59.congruence F E m ≤ typeGroup F E m from le_sup_right) hg)
375 
376 omit hθsupport [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
377 /-- Specializing the centralizer removes the extra lattice-model containment premise. -/
378 theorem actual_model_from_centralizer
379     (hθcentralizer : ∀ g : GL n F,
380       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
381       ∃ a : J₁, ∃ b : (ActualCuspidalCandidate105.centralizerMap F E m n e).range,
382       ∃ c : J₁, (a : GL n F) * (b : GL n F) * (c : GL n F) = g)
383     (hB : ∀ b : GL m 𝒪[E], (coordinateAut e).symm (integralMatrix F E m b) ∈
384       CharacterNormalizer61.normalizer D θ) :
385     compactGroup F E m n e D θ ≤ matrixType F E m n e := by
386   apply actual_model_le F E m n e D θ J₁
387     (ActualCuspidalCandidate105.centralizerMap F E m n e).range hJ hJN hθcentralizer
388   · rw [centralizer_inf_chain F E m n e]
389     exact integralCentralizer_le_character_normalizer F E m n e D θ hB
390   · rw [centralizer_inf_chain F E m n e, matrixType_eq_integral_sup F E m n e]
391     exact le_sup_left
392 
393 omit hθsupport [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
394 /-- The remaining intersection hypothesis is only containment of the concrete residue kernel. -/
395 theorem actual_first_from_residue
396     (hθcentralizer : ∀ g : GL n F,
397       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
398       ∃ a : J₁, ∃ b : (ActualCuspidalCandidate105.centralizerMap F E m n e).range,
399       ∃ c : J₁, (a : GL n F) * (b : GL n F) * (c : GL n F) = g)
400     (hresidue : (ActualResidueGeneralLinear.reduction E m).ker.map
401       ((ActualCuspidalCandidate105.centralizerMap F E m n e).comp
402         (ActualIntegralGeneralLinear.embedding E m)) ≤ J₁) :
403     firstSubgroup F E m n e D θ = J₁.subgroupOf (compactGroup F E m n e D θ) := by
404   apply actual_first_subgroup_eq F E m n e D θ J₁
405     (ActualCuspidalCandidate105.centralizerMap F E m n e).range hJ hJN hθcentralizer
406   rw [centralizer_inf_congruence F E m n e]
407   exact hresidue
408 
409 omit hθsupport [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
410 /-- Canonical support expressed through J₁ gives the existing candidate's compact support bound. -/
411 theorem character_support_compact
412     (hθcentralizer : ∀ g : GL n F,
413       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
414       ∃ a : J₁, ∃ b : (ActualCuspidalCandidate105.centralizerMap F E m n e).range,
415       ∃ c : J₁, (a : GL n F) * (b : GL n F) * (c : GL n F) = g)
416     (g : GL n F)
417     (hg : NormalizerIntertwining60.IntertwinedAt D
418       (MonomialInduction.scalarRepresentation θ) g) :
419     ∃ j₁ j₂ : compactGroup F E m n e D θ, ∃ y : GL m E,
420       g = (j₁ : GL n F) * ActualCuspidalCandidate105.centralizerMap F E m n e y *
421         (j₂ : GL n F) := by
422   have hJC : J₁ ≤ compactGroup F E m n e D θ :=
423     le_inf hJN (hJ.trans (matrixCongruence_le_chainGroup F E m n e))
424   obtain ⟨a, b, c, he⟩ := hθcentralizer g hg
425   obtain ⟨y, hy⟩ := b.property
426   refine ⟨⟨a, hJC a.property⟩, ⟨c, hJC c.property⟩, y, ?_⟩
427   change g = (a : GL n F) * ActualCuspidalCandidate105.centralizerMap F E m n e y * (c : GL n F)
428   rw [hy]
429   exact he.symm
430 
431 end Actual
432 end PaperXI.NormalizerDictionary110

Back to source controls