CentralCharacterInduction.lean

1 import PaperXI.OpenSubgroupSmoothInduction
2 
3 /-!
4 # The central action of actual induction
5 
6 The scalar on a central element of the inducing subgroup remains the scalar on
7 the actual induced representation. Consequently, two different such scalars
8 cannot be related by a nonzero ambient intertwiner. No irreducibility hypothesis
9 or finite-index hypothesis is used.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 namespace PaperXI.CentralCharacterInduction
14 
15 open Representation PaperXI.OpenSubgroupSmoothInduction
16 
17 variable {k G V W : Type*} [Field k] [Group G]
18   [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
19 
20 /-- The action of a central inducing element on genuine induction is its
21 prescribed scalar. This checks the right-translation convention explicitly. -/
22 theorem ind_central_scalar (H : Subgroup G) (σ : Representation k H V)
23     (z : H) (hz : ∀ g : G, Commute (z : G) g) (c : k)
24     (hσ : σ z = c • LinearMap.id) :
25     ind H.subtype σ (z : G) = c • LinearMap.id := by
26   apply IndV.hom_ext
27   intro g
28   ext v
29   rw [LinearMap.comp_apply, ind_mk]
30   have hcomm : g * (z : G)⁻¹ = (z : G)⁻¹ * g :=
31     ((hz g).inv_left).eq.symm
32   rw [hcomm, mk_subgroup, hσ]
33   simp
34 
35 /-- An intertwiner between two actions with different central scalars is zero.
36 The conclusion concerns the actual linear map, without any Schur shortcut. -/
37 theorem intertwiner_eq_zero_of_scalar_ne
38     (ρ : Representation k G V) (τ : Representation k G W) (z : G)
39     (c d : k) (hc : ρ z = c • LinearMap.id)
40     (hd : τ z = d • LinearMap.id) (hne : c ≠ d)
41     (T : IntertwiningMap ρ τ) : T.toLinearMap = 0 := by
42   ext v
43   have h := LinearMap.congr_fun (T.isIntertwining' z) v
44   have he : c • T v = d • T v := by
45     simpa [hc, hd] using h
46   have hzero : (c - d) • T v = 0 := by
47     rw [sub_smul, he, sub_self]
48   exact (smul_eq_zero.mp hzero).resolve_left (sub_ne_zero.mpr hne)
49 
50 /-- The scalar distinction applies directly to actual induced representations. -/
51 theorem ind_intertwiner_eq_zero
52     (H : Subgroup G) (σ : Representation k H V) (τ : Representation k H W)
53     (z : H) (hz : ∀ g : G, Commute (z : G) g) (c d : k)
54     (hc : σ z = c • LinearMap.id) (hd : τ z = d • LinearMap.id)
55     (hne : c ≠ d)
56     (T : IntertwiningMap (ind H.subtype σ) (ind H.subtype τ)) :
57     T.toLinearMap = 0 :=
58   intertwiner_eq_zero_of_scalar_ne _ _ (z : G) c d
59     (ind_central_scalar H σ z hz c hc)
60     (ind_central_scalar H τ z hz d hd) hne T
61 
62 end PaperXI.CentralCharacterInduction

Back to source controls