CliffordSource.lean

1 import PaperXI.CliffordIrreducible
2 import PaperXI.CliffordCocycle
3 
4 /-! The normalized cocycle and literal projective action for the source
5 Clifford datum, with all auxiliary dimensions and nontriviality derived. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CliffordSource
9 open CliffordDatum CliffordMultiplicity CliffordIrreducible CocycleCommutator
10 open scoped IsMulCommutative
11 
12 variable {G W X : Type*} [Group G] [Finite G]
13 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
14 variable (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
15 variable (ρ : Representation ℂ N W) (π : Representation ℂ G X)
16 variable [Representation.IsIrreducible ρ] [Representation.IsIrreducible π]
17 variable (h : Isotypic N ρ π) (hρ : Invariant N ρ)
18 
19 /-- The actual Clifford cocycle on the quotient, extracted from its actual Hom action. -/
20 def cocycle : Cocycle (G ⧸ N) ℂˣ := by
21   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
22   let : Nontrivial (Space N ρ π) := multiplicity_nontrivial N ρ π h
23   exact CliffordCocycle.cocycle N ρ π hρ
24 
25 /-- The source cocycle is normalized at the identity. -/
26 theorem normalized : Normalized (cocycle N ρ π h hρ) := by
27   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
28   let : Nontrivial (Space N ρ π) := multiplicity_nontrivial N ρ π h
29   exact CliffordCocycle.normalized N ρ π hρ
30 
31 /-- The cocycle acts by the literal section operators, with the proved inverse-defect convention. -/
32 theorem operator_mul (a b : G ⧸ N) :
33     (sectionOperator N ρ π hρ a).toLinearMap * (sectionOperator N ρ π hρ b).toLinearMap =
34       ((cocycle N ρ π h hρ).coeff a b : ℂ) •
35         (sectionOperator N ρ π hρ (a * b)).toLinearMap := by
36   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
37   exact CliffordCocycle.sectionOperator_mul N ρ π hρ a b
38 
39 include h
40 omit [IsMulCommutative (G ⧸ N)] in
41 /-- The actual operators and cocycle have a nonzero carrier and an irreducible action. -/
42 theorem projective_irreducible :
43     Nontrivial (Space N ρ π) ∧
44       ∀ L : Submodule ℂ (Space N ρ π),
45         (∀ a f, f ∈ L → sectionOperator N ρ π hρ a f ∈ L) → L = ⊥ ∨ L = ⊤ :=
46   ⟨multiplicity_nontrivial N ρ π h, CliffordIrreducible.irreducible N ρ π h hρ⟩
47 
48 end PaperXI.CliffordSource

Back to source controls