IntersectionModel108.lean

1 import PaperXI.IntertwiningSpace107
2 import PaperXI.QuotientRepresentation
3 import PaperXI.CharacterPairing108
4 
5 /-! The literal conjugate-intersection operator space and its exact finite
6 quotient model. No identification of distinct Hom spaces is assumed. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.IntersectionModel108
10 open Representation IntertwiningAlong105
11 variable {k K G W U Q : Type*} [Field k] [Group K] [Group G] [Group Q]
12   [AddCommGroup W] [Module k W] [AddCommGroup U] [Module k U]
13 
14 /-- Both original elements are retained; this also works before injectivity of
15 `ι` is known. -/
16 def pairs (ι : K →* G) (g : G) : Subgroup (K × K) :=
17   (ι.comp (MonoidHom.snd K K)).eqLocus
18     ((MulAut.conj g).toMonoidHom.comp (ι.comp (MonoidHom.fst K K)))
19 
20 def left (ι : K →* G) (g : G) : pairs ι g →* K :=
21   (MonoidHom.fst K K).comp (pairs ι g).subtype
22 
23 def right (ι : K →* G) (g : G) : pairs ι g →* K :=
24   (MonoidHom.snd K K).comp (pairs ι g).subtype
25 
26 /-- Identity on underlying linear maps. -/
27 def spaceEquiv (ι : K →* G) (ρ : Representation k K W) (g : G) :
28     IntertwiningSpace107.space ι ρ g ≃ₗ[k]
29       IntertwiningMap (ρ.comp (left ι g)) (ρ.comp (right ι g)) where
30   toFun T := (T : W →ₗ[k] W).intertwiningMap_of_isIntertwiningMap _ _
31     (fun x w => T.property x.val.1 x.val.2 x.property w)
32   invFun T := ⟨T.toLinearMap, fun x y hxy w => IntertwiningMap.isIntertwining _ _ T ⟨(x, y), hxy⟩ w⟩
33   left_inv _ := rfl
34   right_inv _ := rfl
35   map_add' _ _ := rfl
36   map_smul' _ _ := rfl
37 
38 /-- Surjective pullback is a linear equivalence of actual intertwining maps. -/
39 def pullbackEquiv (q : K →* Q) (hq : Function.Surjective q)
40     (ρ : Representation k Q W) (σ : Representation k Q U) :
41     IntertwiningMap ρ σ ≃ₗ[k] IntertwiningMap (ρ.comp q) (σ.comp q) where
42   toFun T := T.toLinearMap.intertwiningMap_of_isIntertwiningMap _ _
43     (fun x w => IntertwiningMap.isIntertwining _ _ T (q x) w)
44   invFun T := T.toLinearMap.intertwiningMap_of_isIntertwiningMap _ _
45     ((QuotientRepresentation.intertwines_comp_iff q hq ρ σ T.toLinearMap).mp
46       (fun x w => IntertwiningMap.isIntertwining _ _ T x w))
47   left_inv _ := rfl
48   right_inv _ := rfl
49   map_add' _ _ := rfl
50   map_smul' _ _ := rfl
51 
52 /-- A specified finite quotient must identify both actions pointwise. -/
53 theorem finrank_model (ι : K →* G) (ρ : Representation k K W) (g : G)
54     (q : pairs ι g →* Q) (hq : Function.Surjective q)
55     (ρ₁ ρ₂ : Representation k Q W)
56     (h₁ : ρ₁.comp q = ρ.comp (left ι g)) (h₂ : ρ₂.comp q = ρ.comp (right ι g)) :
57     Module.finrank k (IntertwiningSpace107.space ι ρ g) =
58       Module.finrank k (IntertwiningMap ρ₁ ρ₂) := by
59   rw [(spaceEquiv ι ρ g).finrank_eq, ← h₁, ← h₂]
60   exact (pullbackEquiv q hq ρ₁ ρ₂).finrank_eq.symm
61 
62 end PaperXI.IntersectionModel108

Back to source controls