CliffordCocycle.lean

1 import PaperXI.CliffordChoices
2 
3 /-! The Clifford cocycle is extracted from the literal multiplicity action.
4 The scalar on the multiplicity space is the inverse of the Schur scalar
5 comparing the subgroup intertwiners. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CliffordCocycle
9 open CliffordDatum CliffordMultiplicity CliffordChoices CocycleCommutator
10 open scoped IsMulCommutative
11 
12 variable {G W X : Type*} [Group G]
13 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
14 
15 /-- The unique Schur scalar for the actual subgroup-valued section defect. -/
16 def scalar (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
17     [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
18     (hρ : Invariant N ρ) (a b : G ⧸ N) : ℂˣ :=
19   intertwinerScalar N ρ (sectionMap N a * sectionMap N b)
20     (defectIntertwiner N ρ hρ a b)
21     (productIntertwiner N ρ (sectionMap N a) (sectionMap N b)
22       (sectionIntertwiner N ρ hρ a) (sectionIntertwiner N ρ hρ b))
23 
24 /-- The scalar convention on the original irreducible representation. -/
25 theorem scalar_spec (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
26     [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
27     (hρ : Invariant N ρ) (a b : G ⧸ N) (w : W) :
28     sectionIntertwiner N ρ hρ a (sectionIntertwiner N ρ hρ b w) =
29       (scalar N ρ hρ a b : ℂ) •
30         ρ (defect N a b) (sectionIntertwiner N ρ hρ (a * b) w) :=
31   intertwinerScalar_spec N ρ (sectionMap N a * sectionMap N b)
32     (defectIntertwiner N ρ hρ a b)
33     (productIntertwiner N ρ (sectionMap N a) (sectionMap N b)
34       (sectionIntertwiner N ρ hρ a) (sectionIntertwiner N ρ hρ b)) w
35 
36 /-- The actual defect-adjusted multiplicity operator cancels to the operator
37 at the product quotient element. -/
38 theorem operator_defect (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
39     (π : Representation ℂ G X) (hρ : Invariant N ρ) (a b : G ⧸ N) :
40     operator N ρ π (sectionMap N a * sectionMap N b) (defectIntertwiner N ρ hρ a b) =
41       sectionOperator N ρ π hρ (a * b) := by
42   have h := operator_subgroup_mul N ρ π (defect N a b) (sectionMap N (a * b))
43     (sectionIntertwiner N ρ hρ (a * b))
44   ext f w
45   have hh := congrArg (fun e : Space N ρ π ≃ₗ[ℂ] Space N ρ π => e f w) h
46   change π ((defect N a b : G) * sectionMap N (a * b))
47     (f ((sectionIntertwiner N ρ hρ (a * b)).symm (ρ (defect N a b)⁻¹ w))) = _ at hh
48   rw [← section_mul] at hh
49   exact hh
50 
51 /-- The inverse scalar law is proved on the literal `Hom_N` operators. -/
52 theorem sectionOperator_mul (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
53     [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
54     (π : Representation ℂ G X) (hρ : Invariant N ρ) (a b : G ⧸ N) :
55     (sectionOperator N ρ π hρ a).toLinearMap * (sectionOperator N ρ π hρ b).toLinearMap =
56       (((scalar N ρ hρ a b)⁻¹ : ℂˣ) : ℂ) •
57         (sectionOperator N ρ π hρ (a * b)).toLinearMap := by
58   rw [sectionOperator, sectionOperator, operator_product]
59   have h := operator_choice N ρ π (sectionMap N a * sectionMap N b)
60     (defectIntertwiner N ρ hρ a b)
61     (productIntertwiner N ρ (sectionMap N a) (sectionMap N b)
62       (sectionIntertwiner N ρ hρ a) (sectionIntertwiner N ρ hρ b))
63   rw [operator_defect] at h
64   exact h
65 
66 /-- An invertible multiplicity operator is nonzero on a nonzero multiplicity space. -/
67 theorem sectionOperator_ne_zero (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
68     (π : Representation ℂ G X) (hρ : Invariant N ρ) [Nontrivial (Space N ρ π)]
69     (a : G ⧸ N) : (sectionOperator N ρ π hρ a).toLinearMap ≠ 0 := by
70   intro h
71   obtain ⟨f, hf⟩ := exists_ne (0 : Space N ρ π)
72   have hz := LinearMap.congr_fun h f
73   exact hf ((sectionOperator N ρ π hρ a).injective
74     (hz.trans (sectionOperator N ρ π hρ a).map_zero.symm))
75 
76 /-- The actual scalar cocycle; associativity is derived from multiplication on `Hom_N`. -/
77 def cocycle (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
78     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
79     (π : Representation ℂ G X) (hρ : Invariant N ρ) [Nontrivial (Space N ρ π)] :
80     Cocycle (G ⧸ N) ℂˣ :=
81   ProjectiveCocycle.cocycle (fun a => (sectionOperator N ρ π hρ a).toLinearMap)
82     (sectionOperator_ne_zero N ρ π hρ) (fun a b => (scalar N ρ hρ a b)⁻¹)
83     (sectionOperator_mul N ρ π hρ)
84 
85 @[simp] theorem cocycle_coeff (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
86     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
87     (π : Representation ℂ G X) (hρ : Invariant N ρ) [Nontrivial (Space N ρ π)]
88     (a b : G ⧸ N) : (cocycle N ρ π hρ).coeff a b = (scalar N ρ hρ a b)⁻¹ := rfl
89 
90 /-- Both normalizations follow from the normalized actual quotient operators. -/
91 theorem normalized (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
92     (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
93     (π : Representation ℂ G X) (hρ : Invariant N ρ) [Nontrivial (Space N ρ π)] :
94     Normalized (cocycle N ρ π hρ) := by
95   apply ProjectiveCocycle.normalized
96   exact congrArg LinearEquiv.toLinearMap (sectionOperator_one N ρ π hρ)
97 
98 end PaperXI.CliffordCocycle

Back to source controls