CentralExtensionInductionConsequences.lean

1 import PaperXI.CentralExtensionInducing
2 import PaperXI.CentralCharacterInduction
3 
4 /-!
5 # Actual induced candidates with prescribed central scalar
6 
7 The central extension constructs nonzero smooth induced representations with
8 an arbitrary unit scalar on the adjoined central element.  Different scalars
9 give no nonzero ambient intertwiner.  These statements do not assert that the
10 induced representations are irreducible, admissible, or realizations of a
11 specified supercuspidal parameter.
12 -/
13 set_option autoImplicit false
14 noncomputable section
15 namespace PaperXI.CentralExtensionInductionConsequences
16 
17 open Representation CentralExtensionInducing
18 
19 variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
20 
21 /-- The actual induced action, with its literal Mathlib coinvariant module. -/
22 def inducedRepresentation (J : Subgroup G) (z : G)
23     (hz : ∀ g : G, Commute z g)
24     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
25     (σ : Representation k J V) (c : kˣ) :
26     Representation k G (IndV (extendedSubgroup J z hz).subtype
27       (extendedRepresentation J z hz hfree σ c)) :=
28   ind (extendedSubgroup J z hz).subtype (extendedRepresentation J z hz hfree σ c)
29 
30 /-- The prescribed scalar survives genuine induction to the ambient group. -/
31 theorem induced_central_scalar (J : Subgroup G) (z : G)
32     (hz : ∀ g : G, Commute z g)
33     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
34     (σ : Representation k J V) (c : kˣ) :
35     inducedRepresentation J z hz hfree σ c z = (c : k) • LinearMap.id :=
36   CentralCharacterInduction.ind_central_scalar (extendedSubgroup J z hz)
37     (extendedRepresentation J z hz hfree σ c) (centralElement J z hz) hz c
38     (extendedRepresentation_central J z hz hfree σ c)
39 
40 /-- The construction retains nonzero vectors; no finite-index premise is needed. -/
41 theorem induced_nontrivial (J : Subgroup G) (z : G)
42     (hz : ∀ g : G, Commute z g)
43     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
44     (σ : Representation k J V) (c : kˣ) [Nontrivial V] :
45     Nontrivial (IndV (extendedSubgroup J z hz).subtype
46       (extendedRepresentation J z hz hfree σ c)) :=
47   OpenSubgroupSmoothInduction.ind_nontrivial _ _
48 
49 /-- Unequal chosen central scalars preclude every nonzero ambient intertwiner. -/
50 theorem induced_intertwiner_eq_zero (J : Subgroup G) (z : G)
51     (hz : ∀ g : G, Commute z g)
52     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
53     (σ : Representation k J V) (c d : kˣ) (hne : c ≠ d)
54     (T : IntertwiningMap (inducedRepresentation J z hz hfree σ c)
55       (inducedRepresentation J z hz hfree σ d)) : T.toLinearMap = 0 :=
56   CentralCharacterInduction.intertwiner_eq_zero_of_scalar_ne _ _ z (c : k) (d : k)
57     (induced_central_scalar J z hz hfree σ c)
58     (induced_central_scalar J z hz hfree σ d)
59     (fun h => hne (Units.ext h)) T
60 
61 /-- Consequently the nonzero induced candidates for different scalars are inequivalent. -/
62 theorem induced_not_equiv (J : Subgroup G) (z : G)
63     (hz : ∀ g : G, Commute z g)
64     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
65     (σ : Representation k J V) (c d : kˣ) (hne : c ≠ d) [Nontrivial V] :
66     ¬ Nonempty (Representation.Equiv (inducedRepresentation J z hz hfree σ c)
67       (inducedRepresentation J z hz hfree σ d)) := by
68   rintro ⟨e⟩
69   obtain ⟨v, hv⟩ := exists_ne (0 : V)
70   let w := IndV.mk (extendedSubgroup J z hz).subtype
71     (extendedRepresentation J z hz hfree σ c) 1 v
72   have hw : w ≠ 0 := OpenSubgroupSmoothInduction.mk_ne_zero _ _ 1 hv
73   have he := induced_intertwiner_eq_zero J z hz hfree σ c d hne e.toIntertwiningMap
74   have hew : e.toLinearEquiv w = e.toLinearEquiv 0 := by
75     change e.toIntertwiningMap.toLinearMap w = e.toIntertwiningMap.toLinearMap 0
76     rw [he]
77     rfl
78   exact hw (e.toLinearEquiv.injective hew)
79 
80 section Topology
81 variable [TopologicalSpace G] [IsTopologicalGroup G]
82 
83 /-- Smooth inducing data on an open subgroup yield a smooth actual induced candidate. -/
84 theorem induced_isSmooth (J : Subgroup G) (z : G)
85     (hz : ∀ g : G, Commute z g)
86     (hfree : ∀ n : ℤ, z ^ n ∈ J → n = 0)
87     (σ : Representation k J V) (c : kˣ)
88     (hJ : IsOpen (J : Set G)) (hσ : SmoothDegreeQuotient.IsSmooth σ) :
89     SmoothDegreeQuotient.IsSmooth (inducedRepresentation J z hz hfree σ c) :=
90   OpenSubgroupSmoothInduction.ind_isSmooth _ _
91     (extendedSubgroup_isOpen J z hz hJ)
92     (extendedRepresentation_smooth J z hz hfree σ c hJ hσ)
93 
94 end Topology
95 end PaperXI.CentralExtensionInductionConsequences

Back to source controls