InductionIrreducibility.lean

1 import PaperXI.OpenSubgroupSmoothInduction
2 import PaperXI.RepresentationStability
3 import PaperXI.SemisimpleProjection
4 import PaperXI.CompactSmoothSemisimple
5 
6 /-!
7 # Irreducibility of actual subgroup induction from a local coefficient projector
8 
9 All spaces and actions below are Mathlib's actual `IndV` and `ind`, at arbitrary
10 subgroup index.  The projection hypothesis is a local group-algebra condition:
11 each vector's identity-coset coefficient can be isolated by a finite linear
12 combination of subgroup operators.  The conclusion is actual irreducibility,
13 not scalar endomorphisms or an assumed simple subrepresentation lattice.
14 -/
15 set_option autoImplicit false
16 noncomputable section
17 namespace PaperXI.InductionIrreducibility
18 
19 open Representation PaperXI.OpenSubgroupSmoothInduction
20 open PaperXI.RepresentationStability
21 
22 variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
23 variable (H : Subgroup G) (σ : Representation k H V)
24 
25 /-- The actual inducing space, placed on the identity right coset. -/
26 def identityInclusion : IntertwiningMap σ ((ind H.subtype σ).comp H.subtype) where
27   toLinearMap := IndV.mk H.subtype σ 1
28   isIntertwining' h := by
29     ext v
30     change IndV.mk H.subtype σ 1 (σ h v) =
31       ind H.subtype σ (h : G) (IndV.mk H.subtype σ 1 v)
32     rw [ind_mk, one_mul, ← mk_subgroup]
33     simp
34 
35 /-- Translation in the actual induced representation translates coefficients. -/
36 theorem evaluate_translate (t x : G) (z : IndV H.subtype σ) :
37     evaluate H σ x (ind H.subtype σ t z) = evaluate H σ (x * t) z := by
38   have he := LinearMap.congr_fun ((functionIntertwiner H σ).isIntertwining' t) z
39   exact congrArg (fun f : coindV H.subtype σ => f.val x) he
40 
41 /-- Evaluation on the identity coset is a subgroup intertwiner. -/
42 def identityEvaluation : IntertwiningMap ((ind H.subtype σ).comp H.subtype) σ where
43   toLinearMap := evaluate H σ 1
44   isIntertwining' h := by
45     apply LinearMap.ext
46     intro z
47     change evaluate H σ 1 (ind H.subtype σ (h : G) z) = σ h (evaluate H σ 1 z)
48     rw [evaluate_translate, one_mul]
49     change (functionModel H σ z).val (h : G) = σ h ((functionModel H σ z).val 1)
50     exact (by simpa only [Subgroup.subtype_apply, mul_one] using
51       (functionModel H σ z).property h 1)
52 
53 @[simp] theorem identityEvaluation_inclusion (v : V) :
54     identityEvaluation H σ (identityInclusion H σ v) = v := evaluate_mk_self H σ 1 v
55 
56 /-- The identity-coset projection on actual induced vectors. -/
57 def identityProjection : Module.End k (IndV H.subtype σ) :=
58   (identityInclusion H σ).toLinearMap ∘ₗ (identityEvaluation H σ).toLinearMap
59 
60 /-- A nonzero vector has a nonzero coefficient, without any finite-index assumption. -/
61 theorem exists_nonzero_coefficient {z : IndV H.subtype σ} (hz : z ≠ 0) :
62     ∃ x : G, evaluate H σ x z ≠ 0 := by
63   by_contra h
64   push Not at h
65   apply hz
66   apply functionModel_injective H σ
67   apply Subtype.ext
68   funext x
69   exact h x
70 
71 /-- Once a stable space contains the identity copy, translations generate all induction. -/
72 theorem eq_top_of_contains_identity (S : Submodule k (IndV H.subtype σ))
73     (hS : Stable (ind H.subtype σ) S)
74     (hi : ∀ v : V, identityInclusion H σ v ∈ S) : S = ⊤ := by
75   have hq : S.mkQ = 0 := by
76     apply IndV.hom_ext
77     intro g
78     ext v
79     apply (Submodule.Quotient.mk_eq_zero S).mpr
80     have hv := hS g⁻¹ (identityInclusion H σ v) (hi v)
81     simpa only [identityInclusion, IntertwiningMap.coe_mk, ind_mk, inv_inv, one_mul] using hv
82   apply top_unique
83   intro z _
84   exact (Submodule.Quotient.mk_eq_zero S).mp (LinearMap.congr_fun hq z)
85 
86 /-- The coefficient projector, together with irreducibility of the inducing
87 action, proves irreducibility of genuine induction. -/
88 theorem irreducible_of_projection [IsIrreducible σ]
89     (hP : ∀ S : Submodule k (IndV H.subtype σ), Stable (ind H.subtype σ) S →
90       ∀ z ∈ S, identityProjection H σ z ∈ S) :
91     IsIrreducible (ind H.subtype σ) := by
92   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space σ
93   let : Nontrivial (IndV H.subtype σ) := ind_nontrivial H σ
94   apply irreducible_of_stable
95   intro S hS
96   by_cases hSb : S = ⊥
97   · exact Or.inl hSb
98   right
99   obtain ⟨z, hzS, hz⟩ := S.ne_bot_iff.mp hSb
100   obtain ⟨x, hx⟩ := exists_nonzero_coefficient H σ hz
101   let T := S.comap (identityInclusion H σ).toLinearMap
102   have hT : Stable σ T := by
103     intro h v hv
104     change identityInclusion H σ (σ h v) ∈ S
105     have he := LinearMap.congr_fun ((identityInclusion H σ).isIntertwining' h) v
106     change identityInclusion H σ (σ h v) =
107       ind H.subtype σ (h : G) (identityInclusion H σ v) at he
108     rw [he]
109     exact hS (h : G) _ hv
110   have hc : evaluate H σ x z ∈ T := by
111     have hm := hP S hS (ind H.subtype σ x z) (hS x z hzS)
112     change identityInclusion H σ (evaluate H σ 1 (ind H.subtype σ x z)) ∈ S at hm
113     rw [evaluate_translate, one_mul] at hm
114     exact hm
115   have hTtop : T = ⊤ := by
116     rcases RepresentationStability.eq_bot_or_top σ T hT with hb | ht
117     · exact (hx (by simpa only [hb, Submodule.mem_bot] using hc)).elim
118     · exact ht
119   apply eq_top_of_contains_identity H σ S hS
120   intro v
121   change v ∈ T
122   rw [hTtop]
123   trivial
124 
125 /-- A stable subspace is invariant under every finite group-algebra operator. -/
126 theorem algebra_action_mem {W : Type*} [AddCommGroup W] [Module k W]
127     (τ : Representation k H W) (S : Submodule k W) (hS : Stable τ S)
128     (a : MonoidAlgebra k H) {w : W} (hw : w ∈ S) : τ.asAlgebraHom a w ∈ S := by
129   induction a using MonoidAlgebra.induction_on with
130   | of h => simpa using hS h w hw
131   | add a b ha hb => simpa using S.add_mem ha hb
132   | smul c a ha => simpa using S.smul_mem c ha
133 
134 /-- A concrete local criterion: a finite linear combination of subgroup
135 translations isolates the identity coefficient of each individual vector.
136 The combination may depend on the vector, as for compact smooth averaging. -/
137 theorem irreducible_of_local_groupAlgebra [IsIrreducible σ]
138     (hlocal : ∀ z : IndV H.subtype σ, ∃ a : MonoidAlgebra k H,
139       Representation.asAlgebraHom ((ind H.subtype σ).comp H.subtype) a z =
140         identityProjection H σ z) :
141     IsIrreducible (ind H.subtype σ) := by
142   apply irreducible_of_projection H σ
143   intro S hS z hz
144   obtain ⟨a, ha⟩ := hlocal z
145   rw [← ha]
146   exact algebra_action_mem H ((ind H.subtype σ).comp H.subtype) S
147     (fun h w hw => hS (h : G) w hw) a hz
148 
149 /-- The subgroup `H ∩ g⁻¹Hg`, viewed inside `H`. -/
150 def intersectionSubgroup (g : G) : Subgroup H :=
151   H.comap ((MulAut.conj g).toMonoidHom.comp H.subtype)
152 
153 /-- Conjugation identifies this intersection with a subgroup of the inducing group. -/
154 def intersectionConjugation (g : G) : intersectionSubgroup H g →* H where
155   toFun h := ⟨g * ((h : H) : G) * g⁻¹, h.property⟩
156   map_one' := Subtype.ext (by simp)
157   map_mul' a b := Subtype.ext (by simp)
158 
159 /-- Every coefficient of an `H`-intertwiner is an intertwiner over the exact
160 intersection subgroup appearing in Mackey's criterion. -/
161 def coefficientIntertwiner (g : G)
162     (f : IntertwiningMap σ ((ind H.subtype σ).comp H.subtype)) :
163     IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
164       (σ.comp (intersectionConjugation H g)) where
165   toLinearMap := evaluate H σ g ∘ₗ f.toLinearMap
166   isIntertwining' h := by
167     apply LinearMap.ext
168     intro v
169     change evaluate H σ g (f (σ (h : H) v)) =
170       σ (intersectionConjugation H g h) (evaluate H σ g (f v))
171     rw [f.isIntertwining]
172     change evaluate H σ g (ind H.subtype σ ((h : H) : G) (f v)) = _
173     rw [evaluate_translate]
174     change (functionModel H σ (f v)).val (g * ((h : H) : G)) =
175       σ (intersectionConjugation H g h) ((functionModel H σ (f v)).val g)
176     have hc := (functionModel H σ (f v)).property (intersectionConjugation H g h) g
177     simpa only [intersectionConjugation, MonoidHom.coe_mk, OneHom.coe_mk,
178       Subgroup.subtype_apply, Subtype.coe_mk, mul_assoc, inv_mul_cancel, mul_one] using hc
179 
180 /-- The off-identity Mackey Hom conditions force an `H`-intertwiner whose
181 identity coefficient vanishes to be zero.  No semisimplicity is used here. -/
182 theorem intertwiner_eq_zero_of_mackey
183     (hM : ∀ g : G, g ∉ H →
184       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
185         (σ.comp (intersectionConjugation H g)), A = 0)
186     (f : IntertwiningMap σ ((ind H.subtype σ).comp H.subtype))
187     (hf : ∀ v, identityEvaluation H σ (f v) = 0) : f = 0 := by
188   apply IntertwiningMap.ext
189   apply LinearMap.ext
190   intro v
191   apply functionModel_injective H σ
192   apply Subtype.ext
193   funext g
194   change evaluate H σ g (f v) = 0
195   by_cases hg : g ∈ H
196   · have hc := (functionModel H σ (f v)).property ⟨g, hg⟩ 1
197     change evaluate H σ (g * 1) (f v) = σ ⟨g, hg⟩ (identityEvaluation H σ (f v)) at hc
198     simpa only [mul_one, hf v, map_zero] using hc
199   · have he := congrArg (fun A => A v) (hM g hg (coefficientIntertwiner H σ g f))
200     exact he
201 
202 /-- A Mackey irreducibility theorem for actual induction at arbitrary subgroup
203 index.  Semisimplicity of the restricted induced representation supplies the
204 coefficient projection; all off-identity intersection Hom spaces vanish. -/
205 theorem irreducible_of_mackey [IsIrreducible σ]
206     [IsSemisimpleRepresentation ((ind H.subtype σ).comp H.subtype)]
207     (hM : ∀ g : G, g ∉ H →
208       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
209         (σ.comp (intersectionConjugation H g)), A = 0) :
210     IsIrreducible (ind H.subtype σ) := by
211   apply irreducible_of_projection H σ
212   intro S hS z hz
213   exact SemisimpleProjection.projection_mem σ ((ind H.subtype σ).comp H.subtype)
214     (identityInclusion H σ) (identityEvaluation H σ)
215     (identityEvaluation_inclusion H σ) (intertwiner_eq_zero_of_mackey H σ hM)
216     S (fun h w hw => hS (h : G) w hw) hz
217 
218 /-- The compact-open Mackey criterion has no independent semisimplicity
219 hypothesis: compactness and smoothness prove it for the actual restricted
220 induced representation.  The ambient group and coset space may be infinite. -/
221 theorem irreducible_of_compact_open_mackey [CharZero k]
222     [TopologicalSpace G] [IsTopologicalGroup G] [IsIrreducible σ]
223     (hHopen : IsOpen (H : Set G)) (hHcompact : IsCompact (H : Set G))
224     (hσ : SmoothDegreeQuotient.IsSmooth σ)
225     (hM : ∀ g : G, g ∉ H →
226       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
227         (σ.comp (intersectionConjugation H g)), A = 0) :
228     IsIrreducible (ind H.subtype σ) := by
229   let : CompactSpace H := isCompact_iff_compactSpace.mp hHcompact
230   have hres : SmoothDegreeQuotient.IsSmooth ((ind H.subtype σ).comp H.subtype) := by
231     intro z
232     exact (ind_isSmooth H σ hHopen hσ z).preimage continuous_subtype_val
233   let : IsSemisimpleRepresentation ((ind H.subtype σ).comp H.subtype) :=
234     CompactSmoothSemisimple.smooth_semisimple _ hres
235   exact irreducible_of_mackey H σ hM
236 
237 end PaperXI.InductionIrreducibility

Back to source controls