CharacterSupport108.lean

1 import PaperXI.CharacterAttachment108
2 import PaperXI.FullTypeIntertwining105
3 import PaperXI.IntertwiningSpace107
4 
5 /-! Equality of actual intertwining supports after character attachment. The
6 centralizer beta-intertwining input follows from positive Heisenberg dimension. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.CharacterSupport108
10 open Representation IntertwiningAlong105 CharacterAttachment108
11 variable {G W : Type*} [Group G] [AddCommGroup W] [Module ℂ W]
12   (D J : Subgroup G) (hDJ : D ≤ J) (N : Subgroup J)
13   (hDN : ∀ d : D, Subgroup.inclusion hDJ d ∈ N)
14   (θ : D →* ℂˣ) (κ : Representation ℂ J W)
15 
16 def intoFirst : D →* N := (Subgroup.inclusion hDJ).codRestrict N hDN
17 
18 variable (hscalar : ∀ d : D, κ (Subgroup.inclusion hDJ d) = (θ d : ℂ) • LinearMap.id)
19   (hβ : ∀ g : G,
20     NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
21     NormalizerIntertwining60.IntertwinedAt J κ g)
22 
23 include hscalar hβ hDN in
24 /-- The reverse inclusion uses the retained beta-extension implication. This is
25 support equality, not an assertion that the two Hom spaces have equal dimension. -/
26 theorem restricted_iff_character (g : G) :
27     ExistsAt (J.subtype.comp N.subtype) (κ.comp N.subtype) g ↔
28       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g := by
29   constructor
30   · exact character_of_scalar (J.subtype.comp N.subtype) (κ.comp N.subtype)
31       D θ (intoFirst D J hDJ N hDN) (fun _ => rfl) hscalar g
32   · intro hg
33     obtain ⟨T, hn, ht⟩ := (FullTypeIntertwining105.existsAt_iff_locus J κ g).mpr (hβ g hg)
34     exact ⟨T, hn, fun x y he w => ht x y he w⟩
35 
36 omit N hDN in
37 include hscalar hβ in
38 theorem full_iff_character (g : G) :
39     ExistsAt J.subtype κ g ↔
40       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g := by
41   constructor
42   · exact character_of_scalar J.subtype κ D θ (Subgroup.inclusion hDJ)
43       (fun _ => rfl) hscalar g
44   · intro hg
45     exact (FullTypeIntertwining105.existsAt_iff_locus J κ g).mpr (hβ g hg)
46 
47 include hscalar hβ hDN in
48 theorem full_iff_restricted (g : G) :
49     ExistsAt J.subtype κ g ↔ ExistsAt (J.subtype.comp N.subtype) (κ.comp N.subtype) g :=
50   (full_iff_character D J hDJ θ κ hscalar hβ g).trans
51     (restricted_iff_character D J hDJ N hDN θ κ hscalar hβ g).symm
52 
53 /-- Positive dimension of the actual Hom space gives a nonzero operator. -/
54 theorem existsAt_of_dimension_pos {K : Type*} [Group K] (ι : K →* G)
55     (ρ : Representation ℂ K W) (g : G)
56     (hd : 0 < Module.finrank ℂ (IntertwiningSpace107.space ι ρ g)) : ExistsAt ι ρ g := by
57   let : Nontrivial (IntertwiningSpace107.space ι ρ g) := Module.nontrivial_of_finrank_pos hd
58   obtain ⟨S, hn⟩ := exists_ne (0 : IntertwiningSpace107.space ι ρ g)
59   exact ⟨S, fun h => hn (Subtype.ext h), S.property⟩
60 
61 include hscalar hβ hDN in
62 /-- No separate centralizer beta-intertwiner is required once the character is
63 attached and the Heisenberg intersection dimension is positive. -/
64 theorem beta_of_dimension_pos (g : G)
65     (hd : 0 < Module.finrank ℂ
66       (IntertwiningSpace107.space (J.subtype.comp N.subtype) (κ.comp N.subtype) g)) :
67     ExistsAt J.subtype κ g :=
68   (full_iff_restricted D J hDJ N hDN θ κ hscalar hβ g).mpr
69     (existsAt_of_dimension_pos (J.subtype.comp N.subtype) (κ.comp N.subtype) g hd)
70 
71 end PaperXI.CharacterSupport108

Back to source controls