CliffordCocycleClass.lean

1 import PaperXI.CocycleClass
2 import PaperXI.CliffordCocycleChoices
3 import PaperXI.CliffordTransport
4 import PaperXI.CliffordSource
5 
6 /-! The class of the actual Clifford multiplicity cocycle in the explicit
7 quotient of normalized cocycles by normalized scalar coboundaries. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CliffordCocycleClass
11 
12 open CliffordDatum CliffordMultiplicity CocycleCommutator
13 open scoped IsMulCommutative
14 variable {G W X : Type*} [Group G]
15   [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
16   (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
17   (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
18   (π : Representation ℂ G X) (hρ : Invariant N ρ) [Nontrivial (Space N ρ π)]
19 
20 /-- The cohomological class of the actual Clifford multiplicity action. -/
21 def value : CocycleClass.Class (G ⧸ N) ℂˣ :=
22   CocycleClass.of (CliffordCocycle.cocycle N ρ π hρ) (CliffordCocycle.normalized N ρ π hρ)
23 
24 @[simp] theorem commutator_value (a b : G ⧸ N) :
25     CocycleClass.commutator (value N ρ π hρ) a b =
26       commutator (CliffordCocycle.cocycle N ρ π hρ) a b := rfl
27 
28 @[simp] theorem radical_value :
29     CocycleClass.radical (value N ρ π hρ) = radical (CliffordCocycle.cocycle N ρ π hρ) := rfl
30 
31 /-- Any normalized actual section/intertwiner choice has precisely the same class. -/
32 theorem choice_class (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
33     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a)))
34     (hI : (operator N ρ π (s 1) (I 1)).toLinearMap = 1) :
35     CocycleClass.of (CliffordCocycleChoices.choiceCocycle N ρ π hρ s hs I)
36       (CliffordCocycleChoices.choiceCocycle_normalized N ρ π hρ s hs I hI) = value N ρ π hρ :=
37   CocycleClass.of_rescale (CliffordCocycle.cocycle N ρ π hρ)
38     (CliffordCocycle.normalized N ρ π hρ) (CliffordChoices.choiceCochain N ρ hρ s hs I)
39     (CliffordCocycleChoices.choiceCochain_one N ρ π hρ s hs I hI)
40 
41 /-- Class independence also holds for any independently supplied actual multiplication coefficients. -/
42 theorem class_of_multiplication (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
43     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a)))
44     (hI : (operator N ρ π (s 1) (I 1)).toLinearMap = 1)
45     (d : Cocycle (G ⧸ N) ℂˣ) (hd : Normalized d)
46     (hmul : ∀ a b, (operator N ρ π (s a) (I a)).toLinearMap *
47       (operator N ρ π (s b) (I b)).toLinearMap =
48         (d.coeff a b : ℂ) • (operator N ρ π (s (a * b)) (I (a * b))).toLinearMap) :
49     CocycleClass.of d hd = value N ρ π hρ := by
50   have he := CliffordCocycleChoices.choiceCocycle_unique N ρ π hρ s hs I d hmul
51   subst d
52   exact choice_class N ρ π hρ s hs I hI
53 
54 section Transport
55 variable {G' W' X' : Type*} [Group G']
56   [AddCommGroup W'] [Module ℂ W'] [AddCommGroup X'] [Module ℂ X']
57   (N' : Subgroup G') [N'.Normal] [IsMulCommutative (G' ⧸ N')]
58   (e : G ≃* G') (hN : N.map e.toMonoidHom = N')
59   (ρ' : Representation ℂ N' W') [Representation.IsIrreducible ρ'] [FiniteDimensional ℂ W']
60   (π' : Representation ℂ G' X') [Nontrivial (Space N' ρ' π')]
61   (E : Representation.Equiv ρ (ρ'.comp (CliffordTransport.subgroupEquiv N N' e hN).toMonoidHom))
62   (F : Representation.Equiv π (π'.comp e.toMonoidHom)) (hρ' : Invariant N' ρ')
63 
64 include E F
65 
66 /-- Actual isomorphisms of the original data preserve the cocycle class under quotient pullback. -/
67 theorem value_transport :
68     CocycleClass.pullback (CliffordTransport.quotientEquiv N N' e hN).toMonoidHom
69       (value N' ρ' π' hρ') = value N ρ π hρ := by
70   unfold value
71   rw [CocycleClass.pullback_of]
72   symm
73   apply CocycleClass.of_eq_of_rescale _ _ _ _ (CliffordTransport.cochain N N' e hN ρ ρ' E hρ hρ')
74     (CliffordTransport.cochain_one N N' e hN ρ ρ' π π' E F hρ hρ')
75   apply CocycleClass.cocycle_ext
76   intro a b
77   exact CliffordTransport.cocycle_transport N N' e hN ρ ρ' π π' E F hρ hρ' a b
78 
79 end Transport
80 
81 /-- The class for a finite source datum, with dimension and nonzero multiplicity derived. -/
82 def sourceValue [Finite G] [Representation.IsIrreducible π]
83     (h : CliffordIrreducible.Isotypic N ρ π) : CocycleClass.Class (G ⧸ N) ℂˣ :=
84   CocycleClass.of (CliffordSource.cocycle N ρ π h hρ) (CliffordSource.normalized N ρ π h hρ)
85 
86 section SourceTransport
87 variable {G' W' X' : Type*} [Group G'] [Finite G] [Finite G']
88   [AddCommGroup W'] [Module ℂ W'] [AddCommGroup X'] [Module ℂ X']
89   (N' : Subgroup G') [N'.Normal] [IsMulCommutative (G' ⧸ N')]
90   (e : G ≃* G') (hN : N.map e.toMonoidHom = N')
91   (ρ' : Representation ℂ N' W') [Representation.IsIrreducible ρ']
92   (π' : Representation ℂ G' X') [Representation.IsIrreducible π] [Representation.IsIrreducible π']
93   (E : Representation.Equiv ρ (ρ'.comp (CliffordTransport.subgroupEquiv N N' e hN).toMonoidHom))
94   (F : Representation.Equiv π (π'.comp e.toMonoidHom)) (hρ' : Invariant N' ρ')
95   (h : CliffordIrreducible.Isotypic N ρ π) (h' : CliffordIrreducible.Isotypic N' ρ' π')
96 
97 include E F
98 
99 omit [FiniteDimensional ℂ W] [Nontrivial (Space N ρ π)] in
100 /-- Source 9.7 cocycle-class invariance from actual finite group and representation isomorphisms. -/
101 theorem source_transport :
102     CocycleClass.pullback (CliffordTransport.quotientEquiv N N' e hN).toMonoidHom
103       (sourceValue N' ρ' π' hρ' h') = sourceValue N ρ π hρ h := by
104   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
105   let : FiniteDimensional ℂ W' := FiniteRepresentation.finiteDimensional ρ'
106   let : Nontrivial (Space N ρ π) := CliffordIrreducible.multiplicity_nontrivial N ρ π h
107   let : Nontrivial (Space N' ρ' π') := CliffordIrreducible.multiplicity_nontrivial N' ρ' π' h'
108   exact value_transport N ρ π hρ N' e hN ρ' π' E F hρ'
109 
110 end SourceTransport
111 end PaperXI.CliffordCocycleClass

Back to source controls