CharacterAttachment108.lean

1 import PaperXI.TypeSideDescent
2 import PaperXI.CharacterNormalizer61
3 import PaperXI.RepresentationStability
4 import PaperXI.IntertwiningAlong105
5 
6 /-! Attach the actual character to the prescribed carrier. A single character
7 vector and character normalization imply scalar action, by irreducibility. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CharacterAttachment108
11 open Representation IntertwiningAlong105
12 variable {G K W : Type*} [Group G] [Group K] [AddCommGroup W] [Module ℂ W]
13 
14 theorem irreducible_of_restriction (N : Subgroup K) (κ : Representation ℂ K W)
15     [IsIrreducible (κ.comp N.subtype)] : IsIrreducible κ := by
16   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space (κ.comp N.subtype)
17   apply RepresentationStability.irreducible_of_stable
18   intro S hS
19   exact RepresentationStability.eq_bot_or_top (κ.comp N.subtype) S
20     (fun n w hw => hS n w hw)
21 
22 /-- Original subgroup and character, carried into the prescribed compact group. -/
23 def insideCharacter (D J : Subgroup G) (hDJ : D ≤ J) (θ : D →* ℂˣ) :
24     D.subgroupOf J →* ℂˣ :=
25   θ.comp (Subgroup.subgroupOfEquivOfLe hDJ).toMonoidHom
26 
27 theorem scalar_of_contains (D J : Subgroup G) (hDJ : D ≤ J) (θ : D →* ℂˣ)
28     (hJ : J ≤ CharacterNormalizer61.normalizer D θ)
29     (κ : Representation ℂ J W) [IsIrreducible κ]
30     (hv : ∃ v : W, v ≠ 0 ∧ ∀ d : D, κ (Subgroup.inclusion hDJ d) v = (θ d : ℂ) • v)
31     (d : D) : κ (Subgroup.inclusion hDJ d) = (θ d : ℂ) • LinearMap.id := by
32   let : (D.subgroupOf J).Normal :=
33     Subgroup.normal_subgroupOf_of_le_normalizer
34       (hJ.trans (CharacterNormalizer61.normalizes_domain D θ))
35   have hi : TypeSideDescent.Invariant (D.subgroupOf J) (insideCharacter D J hDJ θ) := by
36     intro j x
37     exact CharacterNormalizer61.character_covariance D θ (hJ j.property)
38       ((Subgroup.subgroupOfEquivOfLe hDJ) x)
39       ((Subgroup.subgroupOfEquivOfLe hDJ) (TypeSideDescent.conjugate (D.subgroupOf J) j x)) rfl
40   have hc : TypeSideDescent.Contains (D.subgroupOf J) (insideCharacter D J hDJ θ) κ := by
41     obtain ⟨v, hn, hv⟩ := hv
42     refine ⟨v, hn, ?_⟩
43     intro x
44     exact hv ((Subgroup.subgroupOfEquivOfLe hDJ) x)
45   exact TypeSideDescent.scalar_restriction (D.subgroupOf J) (insideCharacter D J hDJ θ)
46     hi κ hc ⟨Subgroup.inclusion hDJ d, d.property⟩
47 
48 /-- Nonzero intertwining of a representation with scalar character restriction
49 forces equality of the original character on its literal intersection. -/
50 theorem character_of_scalar (ι : K →* G) (ρ : Representation ℂ K W)
51     (D : Subgroup G) (θ : D →* ℂˣ) (j : D →* K)
52     (hj : ∀ d : D, ι (j d) = (d : G))
53     (hscalar : ∀ d : D, ρ (j d) = (θ d : ℂ) • LinearMap.id)
54     (g : G) (hg : ExistsAt ι ρ g) :
55     NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g := by
56   obtain ⟨T, hn, ht⟩ := hg
57   obtain ⟨w, hw⟩ : ∃ w : W, T w ≠ 0 := by
58     by_contra h
59     push Not at h
60     exact hn (LinearMap.ext h)
61   apply NormalizerIntertwining60.character_intertwinedAt
62   intro x
63   let y := InductionIrreducibility.intersectionConjugation D g x
64   have he : ι (j y) = g * ι (j (x : D)) * g⁻¹ := by
65     rw [hj, hj]
66     rfl
67   have h := ht (j (x : D)) (j y) he w
68   rw [hscalar, hscalar] at h
69   simp only [LinearMap.smul_apply, LinearMap.id_apply, map_smul] at h
70   apply Units.ext
71   exact (smul_left_injective ℂ hw) h
72 
73 end PaperXI.CharacterAttachment108

Back to source controls