CompactModCenterInduction68.lean

1 import PaperXI.EquivariantSplitting68
2 import PaperXI.InducedTypeSpace68
3 
4 /-!
5 # Full-subgroup Mackey irreducibility for compact-mod-central induction
6 
7 The ambient induction and its coefficient maps are the actual Mathlib carriers.
8 No compact-restriction intertwining criterion is substituted for the given
9 full-subgroup criterion. Smoothness, scalar cancellation and compact quotient
10 supply the needed equivariant section by a finite orbit average.
11 -/
12 set_option autoImplicit false
13 noncomputable section
14 namespace PaperXI.CompactModCenterInduction68
15 
16 open Representation PaperXI.SmoothDegreeQuotient
17 open PaperXI.InductionIrreducibility PaperXI.OpenSubgroupSmoothInduction
18 open PaperXI.RepresentationStability
19 
20 variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
21 variable (H : Subgroup G) (σ : Representation k H V)
22 
23 /-- Central scalars on the inducing space act by exactly the same scalar on
24 all actual induced vectors. -/
25 theorem induced_central_scalar (z : H) (hz : ∀ g : G, Commute (z : G) g)
26     (c : k) (hc : ∀ v, σ z v = c • v) (w : IndV H.subtype σ) :
27     ind H.subtype σ (z : G) w = c • w := by
28   apply functionModel_injective H σ
29   apply Subtype.ext
30   funext x
31   change evaluate H σ x (ind H.subtype σ (z : G) w) = evaluate H σ x (c • w)
32   rw [evaluate_translate, map_smul]
33   calc
34     evaluate H σ (x * (z : G)) w = evaluate H σ ((z : G) * x) w :=
35       congrArg (fun t => evaluate H σ t w) (hz x).eq.symm
36     _ = σ z (evaluate H σ x w) := (functionModel H σ w).property z x
37     _ = c • evaluate H σ x w := hc _
38 
39 /-- The literal inclusion of a subrepresentation as an intertwiner. -/
40 def subInclusion {A W : Type*} [Group A] [AddCommGroup W] [Module k W]
41     (τ : Representation k A W) (S : Subrepresentation τ) :
42     IntertwiningMap S.toRepresentation τ where
43   toLinearMap := S.toSubmodule.subtype
44   isIntertwining' _ := rfl
45 
46 variable [CharZero k] [TopologicalSpace G] [IsTopologicalGroup G]
47   [FiniteDimensional k V] [IsIrreducible σ]
48 
49 /-- Actual induction from an open subgroup compact modulo an ambient-central
50 subgroup is irreducible under the FULL off-H Mackey criterion. The compact
51 quotient is H / Z; no compactness of H or finite subgroup index is required. -/
52 theorem irreducible_of_compact_mod_center_mackey
53     (Z : Subgroup H) [Z.Normal] [CompactSpace (H ⧸ Z)]
54     (χ : Z →* kˣ)
55     (hcentral : ∀ z : Z, ∀ g : G, Commute (((z : H) : G)) g)
56     (hscalar : ∀ z : Z, ∀ v, σ (z : H) v = (χ z : k) • v)
57     (hHopen : IsOpen (H : Set G)) (hσ : IsSmooth σ)
58     (hM : ∀ g : G, g ∉ H →
59       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
60         (σ.comp (intersectionConjugation H g)), A = 0) :
61     IsIrreducible (ind H.subtype σ) := by
62   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space σ
63   let : Nontrivial (IndV H.subtype σ) := ind_nontrivial H σ
64   let τ := (ind H.subtype σ).comp H.subtype
65   have hτ : IsSmooth τ := by
66     intro w
67     exact (ind_isSmooth H σ hHopen hσ w).preimage continuous_subtype_val
68   have hcτ : ∀ z : Z, ∀ w, τ (z : H) w = (χ z : k) • w := by
69     intro z w
70     exact induced_central_scalar H σ (z : H) (hcentral z) (χ z : k) (hscalar z) w
71   apply irreducible_of_stable
72   intro S hS
73   by_cases hbot : S = ⊥
74   · exact Or.inl hbot
75   right
76   obtain ⟨w, hwS, hw⟩ := S.ne_bot_iff.mp hbot
77   obtain ⟨g, hg⟩ := exists_nonzero_coefficient H σ hw
78   let T : Subrepresentation τ := ⟨S, fun h v hv => hS (h : G) v hv⟩
79   let p : IntertwiningMap T.toRepresentation σ :=
80     (identityEvaluation H σ).comp (subInclusion τ T)
81   have hpne : p ≠ 0 := by
82     intro hp
83     have he := congrArg (fun f => f ⟨ind H.subtype σ g w, hS g w hwS⟩) hp
84     have he' : evaluate H σ 1 (ind H.subtype σ g w) = 0 := he
85     rw [evaluate_translate, one_mul] at he'
86     exact hg he'
87   have hpsurj := (IsIrreducible.surjective_or_eq_zero p).resolve_right hpne
88   have hT : IsSmooth T.toRepresentation :=
89     CompactSmoothSemisimple.subrepresentation_smooth τ hτ T
90   have hcT : ∀ z : Z, ∀ t, T.toRepresentation (z : H) t = (χ z : k) • t := by
91     intro z t
92     apply Subtype.ext
93     exact hcτ z t
94   obtain ⟨a, ha⟩ := EquivariantSplitting68.exists_equivariant_section
95     Z χ σ T.toRepresentation hσ hT hscalar hcT p hpsurj
96   let A : IntertwiningMap σ τ := (subInclusion τ T).comp a
97   have hA : A = identityInclusion H σ := by
98     apply sub_eq_zero.mp
99     apply intertwiner_eq_zero_of_mackey H σ hM
100     intro v
101     change identityEvaluation H σ ((a v : IndV H.subtype σ) - identityInclusion H σ v) = 0
102     rw [map_sub, identityEvaluation_inclusion]
103     exact sub_eq_zero.mpr (ha v)
104   apply eq_top_of_contains_identity H σ S hS
105   intro v
106   rw [← hA]
107   exact (a v).property
108 
109 /-- The complete general source package keeps nonzeroness, smoothness and
110 irreducibility distinct from later arithmetic admissibility claims. -/
111 theorem induction_package
112     (Z : Subgroup H) [Z.Normal] [CompactSpace (H ⧸ Z)]
113     (χ : Z →* kˣ)
114     (hcentral : ∀ z : Z, ∀ g : G, Commute (((z : H) : G)) g)
115     (hscalar : ∀ z : Z, ∀ v, σ (z : H) v = (χ z : k) • v)
116     (hHopen : IsOpen (H : Set G)) (hσ : IsSmooth σ)
117     (hM : ∀ g : G, g ∉ H →
118       ∀ A : IntertwiningMap (σ.comp (intersectionSubgroup H g).subtype)
119         (σ.comp (intersectionConjugation H g)), A = 0) :
120     Nontrivial (IndV H.subtype σ) ∧ IsSmooth (ind H.subtype σ) ∧
121       IsIrreducible (ind H.subtype σ) := by
122   let : Nontrivial V := GeneratedIrreducibility.nontrivial_space σ
123   exact ⟨ind_nontrivial H σ, ind_isSmooth H σ hHopen hσ,
124     irreducible_of_compact_mod_center_mackey H σ Z χ hcentral hscalar hHopen hσ hM⟩
125 
126 end PaperXI.CompactModCenterInduction68

Back to source controls