NormalizerIntertwining60.lean

1 import PaperXI.InductionIrreducibility
2 import PaperXI.NormalizerExtensionInducing58
3 import PaperXI.MonomialInduction
4 
5 /-!
6 # Actual intersection intertwining at a normalizer
7 
8 The intertwining locus is defined by nonzero maps on the literal intersection
9 subgroup. At a normalizing element such a map is a whole-subgroup intertwiner.
10 An inclusion of the actual character intertwining locus in that of a prescribed
11 representation supplies the required map, without a determinant or residue-size
12 condition. The inclusion is an input; no simple-character theorem is asserted.
13 -/
14 set_option autoImplicit false
15 noncomputable section
16 namespace PaperXI.NormalizerIntertwining60
17 
18 open Representation InductionIrreducibility NormalizerExtensionInducing58
19 
20 variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
21 
22 /-- Intertwining on the actual subgroup intersection, with its actual conjugation. -/
23 def IntertwinedAt (J : Subgroup G) (κ : Representation k J V) (g : G) : Prop :=
24   ∃ T : IntertwiningMap (κ.comp (intersectionSubgroup J g).subtype)
25       (κ.comp (intersectionConjugation J g)), T ≠ 0
26 
27 variable (J : Subgroup G) (κ : Representation k J V) (t : G)
28   (ht : t ∈ Subgroup.normalizer (J : Set G))
29 
30 /-- Normalization makes every subgroup element belong to the intersection. -/
31 def intersectionInclusion : J →* intersectionSubgroup J t where
32   toFun j := ⟨j, (conjugation J t ht j).property⟩
33   map_one' := rfl
34   map_mul' _ _ := rfl
35 
36 /-- The same linear operator now intertwines on the whole original subgroup. -/
37 def normalizerIntertwiner
38     (T : IntertwiningMap (κ.comp (intersectionSubgroup J t).subtype)
39       (κ.comp (intersectionConjugation J t))) :
40     IntertwiningMap κ (κ.comp (conjugation J t ht).toMonoidHom) where
41   toLinearMap := T.toLinearMap
42   isIntertwining' j := T.isIntertwining' (intersectionInclusion J t ht j)
43 
44 @[simp] theorem normalizerIntertwiner_apply
45     (T : IntertwiningMap (κ.comp (intersectionSubgroup J t).subtype)
46       (κ.comp (intersectionConjugation J t))) (v : V) :
47     normalizerIntertwiner J κ t ht T v = T v := rfl
48 
49 theorem normalizerIntertwiner_ne_zero
50     (T : IntertwiningMap (κ.comp (intersectionSubgroup J t).subtype)
51       (κ.comp (intersectionConjugation J t))) (hT : T ≠ 0) :
52     normalizerIntertwiner J κ t ht T ≠ 0 := by
53   intro hz
54   apply hT
55   ext v
56   exact congrArg (fun A : IntertwiningMap κ
57     (κ.comp (conjugation J t ht).toMonoidHom) => A v) hz
58 
59 /-- Existential intertwining data gives a genuine normalizer map, not a scalar label. -/
60 theorem exists_normalizerIntertwiner (h : IntertwinedAt J κ t) :
61     ∃ T : IntertwiningMap κ (κ.comp (conjugation J t ht).toMonoidHom), T ≠ 0 := by
62   obtain ⟨T, hT⟩ := h
63   exact ⟨normalizerIntertwiner J κ t ht T,
64     normalizerIntertwiner_ne_zero J κ t ht T hT⟩
65 
66 /-- Irreducibility turns this actual nonzero normalizer map into an equivalence. -/
67 theorem exists_normalizerEquiv [IsIrreducible κ] (h : IntertwinedAt J κ t) :
68     Nonempty (Representation.Equiv κ (κ.comp (conjugation J t ht).toMonoidHom)) := by
69   obtain ⟨T, hT⟩ := exists_normalizerIntertwiner J κ t ht h
70   exact ⟨T.ofBijective (intertwiner_bijective J t ht κ T hT)⟩
71 
72 section Character
73 variable (H : Subgroup G) (θ : H →* ℂˣ)
74 
75 /-- Covariance of a character on the actual intersection supplies the identity map. -/
76 theorem character_intertwinedAt
77     (hθ : ∀ h : intersectionSubgroup H t,
78       θ (h : H) = θ (intersectionConjugation H t h)) :
79     IntertwinedAt H (MonomialInduction.scalarRepresentation θ) t := by
80   let T : IntertwiningMap
81       ((MonomialInduction.scalarRepresentation θ).comp (intersectionSubgroup H t).subtype)
82       ((MonomialInduction.scalarRepresentation θ).comp (intersectionConjugation H t)) :=
83     { toLinearMap := LinearMap.id
84       isIntertwining' := fun h => by
85         apply LinearMap.ext
86         intro z
87         change (θ (h : H) : ℂ) * z = (θ (intersectionConjugation H t h) : ℂ) * z
88         rw [hθ h] }
89   refine ⟨T, ?_⟩
90   intro hz
91   have he := congrArg (fun A => (A : IntertwiningMap
92     ((MonomialInduction.scalarRepresentation θ).comp (intersectionSubgroup H t).subtype)
93     ((MonomialInduction.scalarRepresentation θ).comp (intersectionConjugation H t))) 1) hz
94   exact one_ne_zero he
95 
96 variable {W : Type*} [AddCommGroup W] [Module ℂ W]
97 variable (κc : Representation ℂ J W)
98 
99 /-- The actual intertwining-locus property of a supplied extension gives its
100 normalizer operator from character covariance. There is no q>2 restriction. -/
101 theorem exists_normalizerIntertwiner_of_character
102     (hβ : ∀ g : G, IntertwinedAt H (MonomialInduction.scalarRepresentation θ) g →
103       IntertwinedAt J κc g)
104     (hθ : ∀ h : intersectionSubgroup H t,
105       θ (h : H) = θ (intersectionConjugation H t h)) :
106     ∃ T : IntertwiningMap κc (κc.comp (conjugation J t ht).toMonoidHom), T ≠ 0 :=
107   exists_normalizerIntertwiner J κc t ht
108     (hβ t (character_intertwinedAt t H θ hθ))
109 
110 end Character
111 end PaperXI.NormalizerIntertwining60

Back to source controls