OpenSubgroupSmoothInduction.lean

1 import PaperXI.SmoothDegreeQuotient
2 import Mathlib.RepresentationTheory.FiniteIndex
3 import Mathlib.Topology.Algebra.OpenSubgroup
4 import Mathlib.Algebra.BigOperators.Finprod
5 
6 /-!
7 # Smooth induction from an open subgroup, with no finite-index hypothesis
8 
9 The target is the actual algebraic induced representation `Representation.ind`.
10 For an open subgroup and a smooth inducing action, its finite-sum vectors are
11 smooth even when the subgroup has infinite index. This is an existence step
12 towards compact induction, not an irreducibility or local-factor theorem.
13 -/
14 set_option autoImplicit false
15 noncomputable section
16 namespace PaperXI.OpenSubgroupSmoothInduction
17 
18 open Representation PaperXI.SmoothDegreeQuotient
19 
20 variable {k G V : Type*} [Field k] [Group G]
21   [TopologicalSpace G] [IsTopologicalGroup G]
22   [AddCommGroup V] [Module k V]
23 
24 /-- Smooth vectors in any algebraic representation form a linear subspace. -/
25 def smoothSubmodule (ρ : Representation k G V) : Submodule k V where
26   carrier := {v | IsOpen (vectorStabilizer ρ v : Set G)}
27   zero_mem' := by
28     change IsOpen (vectorStabilizer ρ 0 : Set G)
29     have h : (vectorStabilizer ρ 0 : Set G) = Set.univ := by
30       ext g
31       simp
32     rw [h]
33     exact isOpen_univ
34   add_mem' := by
35     intro v w hv hw
36     apply Subgroup.isOpen_mono (H₁ := vectorStabilizer ρ v ⊓ vectorStabilizer ρ w)
37       _ (hv.inter hw)
38     intro g hg
39     change ρ g (v + w) = v + w
40     rw [map_add, hg.1, hg.2]
41   smul_mem' := by
42     intro a v hv
43     apply Subgroup.isOpen_mono (H₁ := vectorStabilizer ρ v) _ hv
44     intro g hg
45     change ρ g (a • v) = a • v
46     rw [map_smul, hg]
47 
48 @[simp] theorem mem_smoothSubmodule (ρ : Representation k G V) (v : V) :
49     v ∈ smoothSubmodule ρ ↔ IsOpen (vectorStabilizer ρ v : Set G) := Iff.rfl
50 
51 variable (H : Subgroup G) (σ : Representation k H V)
52 
53 local instance : DecidableRel (QuotientGroup.rightRel H) := Classical.decRel _
54 
55 omit [TopologicalSpace G] [IsTopologicalGroup G] in
56 /-- The actual coinvariant relation, with the subgroup action kept explicit. -/
57 theorem mk_subgroup (h : H) (g : G) (v : V) :
58     IndV.mk H.subtype σ ((h : G)⁻¹ * g) v = IndV.mk H.subtype σ g (σ h v) := by
59   have hh := Coinvariants.mk_inv_tmul
60     ((Representation.leftRegular k G).comp H.subtype)
61     σ (MonoidAlgebra.single g 1) v h
62   simpa using hh
63 
64 /-- Each elementary induced vector has an open conjugate stabilizer. -/
65 theorem mk_smooth (hH : IsOpen (H : Set G)) (hσ : IsSmooth σ) (g : G) (v : V) :
66     IsOpen (vectorStabilizer (ind H.subtype σ) (IndV.mk H.subtype σ g v) : Set G) := by
67   let U := (vectorStabilizer σ v).map H.subtype
68   have hU : IsOpen (U : Set G) := hH.isOpenMap_subtype_val _ (hσ v)
69   let C := U.comap (MulAut.conj g).toMonoidHom
70   have hC : IsOpen (C : Set G) :=
71     hU.preimage ((continuous_const.mul continuous_id).mul continuous_const)
72   apply Subgroup.isOpen_mono (H₁ := C) _ hC
73   intro t ht
74   obtain ⟨h, hh, he⟩ := ht
75   have he' : (h : G) = g * t * g⁻¹ := he
76   have hgt : g * t⁻¹ = (h : G)⁻¹ * g := by
77     rw [he']
78     group
79   change ind H.subtype σ t (IndV.mk H.subtype σ g v) = _
80   rw [ind_mk, hgt, mk_subgroup, hh]
81 
82 /-- Genuine algebraic induction from an open subgroup preserves smoothness,
83 without requiring finite index or a common open kernel for the inducing action. -/
84 theorem ind_isSmooth (hH : IsOpen (H : Set G)) (hσ : IsSmooth σ) :
85     IsSmooth (ind H.subtype σ) := by
86   let S := smoothSubmodule (ind H.subtype σ)
87   have hq : S.mkQ = 0 := by
88     apply IndV.hom_ext
89     intro g
90     ext v
91     exact (Submodule.Quotient.mk_eq_zero S).mpr (mk_smooth H σ hH hσ g v)
92   intro v
93   change v ∈ S
94   apply (Submodule.Quotient.mk_eq_zero S).mp
95   exact LinearMap.congr_fun hq v
96 
97 omit [TopologicalSpace G] [IsTopologicalGroup G] in
98 /-- The genuine induced vector is sent to its covariant function on `G`.
99 This Mathlib construction does not require finite index. -/
100 def functionModel : IndV H.subtype σ →ₗ[k] coindV H.subtype σ := by
101   classical
102   exact Rep.indToCoind (Rep.of σ)
103 
104 omit [TopologicalSpace G] [IsTopologicalGroup G] in
105 @[simp] theorem functionModel_mk (g x : G) (v : V) :
106     (functionModel H σ (IndV.mk H.subtype σ g v)).val x =
107       Rep.indToCoindAux (Rep.of σ) g v x := by
108   classical
109   simp [functionModel, Rep.indToCoind]
110   rfl
111 
112 omit [TopologicalSpace G] [IsTopologicalGroup G] in
113 /-- Evaluation on the supporting coset recovers the original coefficient. -/
114 @[simp] theorem functionModel_mk_self (g : G) (v : V) :
115     (functionModel H σ (IndV.mk H.subtype σ g v)).val g = v := by
116   classical
117   rw [functionModel_mk]
118   exact Rep.indToCoindAux_self (A := Rep.of σ) g v
119 
120 omit [TopologicalSpace G] [IsTopologicalGroup G] in
121 /-- The inducing space embeds into actual induction at every group element. -/
122 theorem mk_injective (g : G) : Function.Injective (IndV.mk H.subtype σ g) := by
123   intro v w hvw
124   have h := congrArg (fun z => (functionModel H σ z).val g) hvw
125   simpa only [functionModel_mk_self] using h
126 
127 omit [TopologicalSpace G] [IsTopologicalGroup G] in
128 /-- Nonzero inducing vectors remain nonzero in the actual induced module. -/
129 theorem mk_ne_zero (g : G) {v : V} (hv : v ≠ 0) : IndV.mk H.subtype σ g v ≠ 0 := by
130   intro h
131   apply hv
132   apply mk_injective H σ g
133   simpa using h
134 
135 omit [TopologicalSpace G] [IsTopologicalGroup G] in
136 theorem ind_nontrivial [Nontrivial V] : Nontrivial (IndV H.subtype σ) :=
137   (mk_injective H σ 1).nontrivial
138 
139 /-- Covariant functions with support in finitely many right cosets of `H`. -/
140 def finiteCosetSupport : Submodule k (coindV H.subtype σ) := by
141   classical
142   exact
143     { carrier := {f | ∃ s : Finset G, ∀ x, f.val x ≠ 0 →
144           ∃ g ∈ s, (QuotientGroup.rightRel H).r x g}
145       zero_mem' := by
146         refine ⟨∅, ?_⟩
147         intro x hx
148         exact (hx rfl).elim
149       add_mem' := by
150         rintro f f' ⟨s, hs⟩ ⟨s', hs'⟩
151         refine ⟨s ∪ s', ?_⟩
152         intro x hx
153         change f.val x + f'.val x ≠ 0 at hx
154         by_cases hf : f.val x = 0
155         · obtain ⟨g, hg, hr⟩ := hs' x (by simpa only [hf, zero_add] using hx)
156           exact ⟨g, Finset.mem_union_right s hg, hr⟩
157         · obtain ⟨g, hg, hr⟩ := hs x hf
158           exact ⟨g, Finset.mem_union_left s' hg, hr⟩
159       smul_mem' := by
160         rintro a f ⟨s, hs⟩
161         refine ⟨s, ?_⟩
162         intro x hx
163         apply hs x
164         intro hf
165         apply hx
166         change a • f.val x = 0
167         rw [hf, smul_zero] }
168 
169 omit [TopologicalSpace G] [IsTopologicalGroup G] in
170 /-- The image of each actual induced vector has finite support modulo `H`.
171 This is support on the right-coset space `H\G`, without a finite-index assumption. -/
172 theorem functionModel_finite_support (z : IndV H.subtype σ) :
173     ∃ s : Finset G, ∀ x, (functionModel H σ z).val x ≠ 0 →
174       ∃ g ∈ s, (QuotientGroup.rightRel H).r x g := by
175   classical
176   let S := finiteCosetSupport H σ
177   have hq : S.mkQ ∘ₗ functionModel H σ = 0 := by
178     apply IndV.hom_ext
179     intro g
180     ext v
181     apply (Submodule.Quotient.mk_eq_zero S).mpr
182     refine ⟨{g}, ?_⟩
183     intro x hx
184     refine ⟨g, Finset.mem_singleton_self g, ?_⟩
185     by_contra hr
186     apply hx
187     rw [functionModel_mk]
188     exact Rep.indToCoindAux_of_not_rel (A := Rep.of σ) g x v hr
189   have hz := LinearMap.congr_fun hq z
190   exact (Submodule.Quotient.mk_eq_zero S).mp hz
191 
192 omit [TopologicalSpace G] [IsTopologicalGroup G] in
193 /-- The literal image of the nonzero-value support in the right-coset quotient is finite. -/
194 theorem functionModel_finite_quotient_support (z : IndV H.subtype σ) :
195     Set.Finite ((Quotient.mk (QuotientGroup.rightRel H)) ''
196       Function.support (functionModel H σ z).val) := by
197   obtain ⟨s, hs⟩ := functionModel_finite_support H σ z
198   apply (s.finite_toSet.image (Quotient.mk (QuotientGroup.rightRel H))).subset
199   rintro q ⟨x, hx, rfl⟩
200   obtain ⟨g, hg, hr⟩ := hs x hx
201   exact ⟨g, hg, (Quotient.sound hr).symm⟩
202 
203 omit [IsTopologicalGroup G] in
204 /-- The support image in the actual topological right-coset quotient is compact. -/
205 theorem functionModel_compact_quotient_support (z : IndV H.subtype σ) :
206     IsCompact ((Quotient.mk (QuotientGroup.rightRel H)) ''
207       Function.support (functionModel H σ z).val) :=
208   (functionModel_finite_quotient_support H σ z).isCompact
209 
210 omit [TopologicalSpace G] [IsTopologicalGroup G] in
211 /-- The covariant-function construction respects the actual ambient group actions. -/
212 def functionIntertwiner : IntertwiningMap (ind H.subtype σ) (coind H.subtype σ) where
213   toLinearMap := functionModel H σ
214   isIntertwining' t := by
215     apply IndV.hom_ext
216     intro g
217     ext v x
218     change (functionModel H σ (ind H.subtype σ t (IndV.mk H.subtype σ g v))).val x =
219       (functionModel H σ (IndV.mk H.subtype σ g v)).val (x * t)
220     rw [ind_mk, functionModel_mk, functionModel_mk]
221     exact Rep.indToCoindAux_fst_mul_inv (A := Rep.of σ) g t x v
222 
223 omit [TopologicalSpace G] [IsTopologicalGroup G] in
224 /-- Evaluation is a coefficient-extracting linear map on actual induced vectors. -/
225 def evaluate (x : G) : IndV H.subtype σ →ₗ[k] V :=
226   (LinearMap.proj x) ∘ₗ (coindV H.subtype σ).subtype ∘ₗ functionModel H σ
227 
228 omit [TopologicalSpace G] [IsTopologicalGroup G] in
229 @[simp] theorem evaluate_mk_self (g : G) (v : V) :
230     evaluate H σ g (IndV.mk H.subtype σ g v) = v := functionModel_mk_self H σ g v
231 
232 omit [TopologicalSpace G] [IsTopologicalGroup G] in
233 theorem evaluate_mk_of_not_rel (g x : G) (v : V)
234     (h : ¬ (QuotientGroup.rightRel H).r x g) :
235     evaluate H σ x (IndV.mk H.subtype σ g v) = 0 := by
236   change (functionModel H σ (IndV.mk H.subtype σ g v)).val x = 0
237   rw [functionModel_mk]
238   exact Rep.indToCoindAux_of_not_rel (A := Rep.of σ) g x v h
239 
240 omit [TopologicalSpace G] [IsTopologicalGroup G] in
241 /-- Distinct right cosets supply linearly independent vectors in actual induction.
242 This prevents finite packet dimensions from being assigned to arbitrary-index induction. -/
243 theorem mk_linearIndependent {I : Type*} (r : I → G)
244     (hr : Pairwise fun i j => ¬ (QuotientGroup.rightRel H).r (r i) (r j))
245     {v : V} (hv : v ≠ 0) :
246     LinearIndependent k (fun i => IndV.mk H.subtype σ (r i) v) := by
247   classical
248   apply linearIndependent_iff'.mpr
249   intro s c hc i hi
250   have he := congrArg (evaluate H σ (r i)) hc
251   simp only [map_sum, map_smul, map_zero] at he
252   have hs : (∑ j ∈ s, c j • evaluate H σ (r i) (IndV.mk H.subtype σ (r j) v)) =
253       c i • v := by
254     rw [Finset.sum_eq_single i]
255     · rw [evaluate_mk_self]
256     · intro j _ hji
257       rw [evaluate_mk_of_not_rel H σ (r j) (r i) v (hr hji.symm), smul_zero]
258     · exact fun h => (h hi).elim
259   rw [hs] at he
260   exact (smul_eq_zero.mp he).resolve_right hv
261 
262 omit [TopologicalSpace G] [IsTopologicalGroup G] in
263 /-- One coset contributes an induced vector independently of its representative. -/
264 def cosetComponent (f : coindV H.subtype σ) (q : Quotient (QuotientGroup.rightRel H)) :
265     IndV H.subtype σ :=
266   Quotient.liftOn q (fun g => IndV.mk H.subtype σ g (f.val g))
267     fun g₁ g₂ ⟨s, (hs : _ * _ = _)⟩ =>
268       (Submodule.Quotient.eq _).2 <| Coinvariants.mem_ker_of_eq s
269         (MonoidAlgebra.single g₂ 1 ⊗ₜ[k] f.val g₂) _ <| by
270           have := f.property s g₂
271           simp_all
272 
273 omit [TopologicalSpace G] [IsTopologicalGroup G] in
274 @[simp] theorem cosetComponent_mk (f : coindV H.subtype σ) (g : G) :
275     cosetComponent H σ f (Quotient.mk (QuotientGroup.rightRel H) g) =
276       IndV.mk H.subtype σ g (f.val g) := rfl
277 
278 omit [TopologicalSpace G] [IsTopologicalGroup G] in
279 theorem cosetComponent_add (f f' : coindV H.subtype σ)
280     (q : Quotient (QuotientGroup.rightRel H)) :
281     cosetComponent H σ (f + f') q = cosetComponent H σ f q + cosetComponent H σ f' q := by
282   induction q using Quotient.inductionOn with | h g =>
283   exact map_add (IndV.mk H.subtype σ g) (f.val g) (f'.val g)
284 
285 omit [TopologicalSpace G] [IsTopologicalGroup G] in
286 theorem cosetComponent_smul (a : k) (f : coindV H.subtype σ)
287     (q : Quotient (QuotientGroup.rightRel H)) :
288     cosetComponent H σ (a • f) q = a • cosetComponent H σ f q := by
289   induction q using Quotient.inductionOn with | h g =>
290   exact map_smul (IndV.mk H.subtype σ g) a (f.val g)
291 
292 omit [TopologicalSpace G] [IsTopologicalGroup G] in
293 theorem cosetComponent_finite (f : finiteCosetSupport H σ) :
294     Function.HasFiniteSupport (cosetComponent H σ f.val) := by
295   obtain ⟨s, hs⟩ := f.property
296   apply (s.finite_toSet.image (Quotient.mk (QuotientGroup.rightRel H))).subset
297   rintro q hq
298   induction q using Quotient.inductionOn with | h g =>
299   have hfg : f.val.val g ≠ 0 := by
300     intro hz
301     apply hq
302     change IndV.mk H.subtype σ g (f.val.val g) = 0
303     rw [hz, map_zero]
304   obtain ⟨g', hg', hr⟩ := hs g hfg
305   exact ⟨g', hg', (Quotient.sound hr).symm⟩
306 
307 omit [TopologicalSpace G] [IsTopologicalGroup G] in
308 /-- Finite-support covariant functions reconstruct actual induced vectors. -/
309 def reconstruct : finiteCosetSupport H σ →ₗ[k] IndV H.subtype σ where
310   toFun f := ∑ᶠ q, cosetComponent H σ f.val q
311   map_add' f f' := by
312     change (∑ᶠ q, cosetComponent H σ (f.val + f'.val) q) = _
313     simp_rw [cosetComponent_add]
314     exact finsum_add_distrib (cosetComponent_finite H σ f) (cosetComponent_finite H σ f')
315   map_smul' a f := by
316     change (∑ᶠ q, cosetComponent H σ (a • f.val) q) = _
317     simp_rw [cosetComponent_smul]
318     exact (smul_finsum' a (cosetComponent_finite H σ f)).symm
319 
320 omit [TopologicalSpace G] [IsTopologicalGroup G] in
321 /-- The function map with its proved finite-support codomain. -/
322 def compactModel : IndV H.subtype σ →ₗ[k] finiteCosetSupport H σ :=
323   (functionModel H σ).codRestrict _ (functionModel_finite_support H σ)
324 
325 omit [TopologicalSpace G] [IsTopologicalGroup G] in
326 theorem reconstruct_compactModel :
327     reconstruct H σ ∘ₗ compactModel H σ = LinearMap.id := by
328   apply IndV.hom_ext
329   intro g
330   ext v
331   change (∑ᶠ q, cosetComponent H σ (functionModel H σ (IndV.mk H.subtype σ g v)) q) = _
332   rw [finsum_eq_single _ (Quotient.mk (QuotientGroup.rightRel H) g)]
333   · rw [cosetComponent_mk, functionModel_mk_self]
334     rfl
335   · intro q hq
336     induction q using Quotient.inductionOn with | h x =>
337     rw [cosetComponent_mk, functionModel_mk,
338       Rep.indToCoindAux_of_not_rel (A := Rep.of σ) g x v (fun hr => hq (Quotient.sound hr)),
339       map_zero]
340 
341 omit [TopologicalSpace G] [IsTopologicalGroup G] in
342 theorem compactModel_reconstruct :
343     compactModel H σ ∘ₗ reconstruct H σ = LinearMap.id := by
344   ext f x
345   change evaluate H σ x (∑ᶠ q, cosetComponent H σ f.val q) = f.val.val x
346   rw [map_finsum (evaluate H σ x) (cosetComponent_finite H σ f),
347     finsum_eq_single _ (Quotient.mk (QuotientGroup.rightRel H) x)]
348   · rw [cosetComponent_mk, evaluate_mk_self]
349   · intro q hq
350     induction q using Quotient.inductionOn with | h g =>
351     rw [cosetComponent_mk]
352     exact evaluate_mk_of_not_rel H σ g x (f.val.val g)
353       (fun hr => hq (Quotient.sound hr).symm)
354 
355 omit [TopologicalSpace G] [IsTopologicalGroup G] in
356 /-- An actual linear equivalence with all finite-support covariant functions,
357 not just an injection of elementary inducing vectors. -/
358 def compactModelEquiv : IndV H.subtype σ ≃ₗ[k] finiteCosetSupport H σ :=
359   LinearEquiv.ofLinearMap (compactModel H σ) (reconstruct H σ)
360     (compactModel_reconstruct H σ) (reconstruct_compactModel H σ)
361 
362 omit [TopologicalSpace G] [IsTopologicalGroup G] in
363 /-- The function model is faithful for arbitrary subgroup index. -/
364 theorem functionModel_injective : Function.Injective (functionModel H σ) := by
365   intro z w hzw
366   apply (compactModelEquiv H σ).injective
367   exact Subtype.ext hzw
368 
369 omit [TopologicalSpace G] [IsTopologicalGroup G] in
370 /-- Exactly the finite-support covariant functions occur in the function model. -/
371 theorem functionModel_range : LinearMap.range (functionModel H σ) = finiteCosetSupport H σ := by
372   ext f
373   constructor
374   · rintro ⟨z, rfl⟩
375     exact functionModel_finite_support H σ z
376   · intro hf
377     obtain ⟨z, hz⟩ := (compactModelEquiv H σ).surjective ⟨f, hf⟩
378     exact ⟨z, congrArg Subtype.val hz⟩
379 
380 /-- Every finite-support covariant function has an open right-translation
381 stabilizer. The statement is about the entire constructed function space. -/
382 theorem finite_functions_smooth (hH : IsOpen (H : Set G)) (hσ : IsSmooth σ)
383     (f : finiteCosetSupport H σ) :
384     IsOpen {t : G | ∀ x : G, f.val.val (x * t) = f.val.val x} := by
385   obtain ⟨z, hz⟩ := (compactModelEquiv H σ).surjective f
386   have hf : functionModel H σ z = f.val := congrArg Subtype.val hz
387   rw [← hf]
388   have hopen : IsOpen (vectorStabilizer (coind H.subtype σ) (functionModel H σ z) : Set G) := by
389     apply Subgroup.isOpen_mono (H₁ := vectorStabilizer (ind H.subtype σ) z)
390       _ (ind_isSmooth H σ hH hσ z)
391     intro t ht
392     have he := LinearMap.congr_fun ((functionIntertwiner H σ).isIntertwining' t) z
393     change functionModel H σ (ind H.subtype σ t z) =
394       coind H.subtype σ t (functionModel H σ z) at he
395     rw [show ind H.subtype σ t z = z from ht] at he
396     exact he.symm
397   have heq : (vectorStabilizer (coind H.subtype σ) (functionModel H σ z) : Set G) =
398       {t : G | ∀ x : G, (functionModel H σ z).val (x * t) =
399         (functionModel H σ z).val x} := by
400     ext t
401     change coind H.subtype σ t (functionModel H σ z) = functionModel H σ z ↔ _
402     constructor
403     · intro ht x
404       exact congrArg (fun u : coindV H.subtype σ => u.val x) ht
405     · intro ht
406       exact Subtype.ext (funext ht)
407   rwa [heq] at hopen
408 
409 end PaperXI.OpenSubgroupSmoothInduction

Back to source controls