CliffordPacket.lean

1 import PaperXI.CliffordSource
2 import PaperXI.TwistedActionEquivalence
3 
4 /-! Source 9.6: the actual Clifford action algebra map is an isomorphism,
5 and the actual multiplicity dimension is the square root of the quotient order. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CliffordPacket
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)] [Fintype (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 literal algebra action of the actual Clifford operators. -/
20 def action :
21     TwistedAlgebra.Algebra (CliffordSource.cocycle N ρ π h hρ)
22       (CliffordSource.normalized N ρ π h hρ) →ₐ[ℂ] Module.End ℂ (Space N ρ π) :=
23   TwistedAction.action _ _ (fun a => (sectionOperator N ρ π hρ a).toLinearMap)
24     (congrArg LinearEquiv.toLinearMap (sectionOperator_one N ρ π hρ))
25     (CliffordSource.operator_mul N ρ π h hρ)
26 
27 @[simp] theorem action_basis (a : G ⧸ N) :
28     action N ρ π h hρ
29       (TwistedAlgebra.basis (CliffordSource.cocycle N ρ π h hρ)
30         (CliffordSource.normalized N ρ π h hρ) a) =
31       (sectionOperator N ρ π hρ a).toLinearMap :=
32   TwistedAction.action_basis _ _ _ _ _ a
33 
34 variable (hnd : radical (CliffordSource.cocycle N ρ π h hρ) = ⊥)
35 include hnd
36 
37 /-- Nondegeneracy makes this actual action map bijective. -/
38 theorem action_bijective : Function.Bijective (action N ρ π h hρ) := by
39   let : Nontrivial (Space N ρ π) := multiplicity_nontrivial N ρ π h
40   exact TwistedActionEquivalence.action_bijective _ _ _ _ _ hnd
41     (CliffordIrreducible.irreducible N ρ π h hρ)
42 
43 /-- The source algebra isomorphism is the actual action, not an unrelated matrix identification. -/
44 def actionEquiv :
45     TwistedAlgebra.Algebra (CliffordSource.cocycle N ρ π h hρ)
46       (CliffordSource.normalized N ρ π h hρ) ≃ₐ[ℂ] Module.End ℂ (Space N ρ π) :=
47   AlgEquiv.ofBijective (action N ρ π h hρ) (action_bijective N ρ π h hρ hnd)
48 
49 @[simp] theorem actionEquiv_apply
50     (x : TwistedAlgebra.Algebra (CliffordSource.cocycle N ρ π h hρ)
51       (CliffordSource.normalized N ρ π h hρ)) :
52     actionEquiv N ρ π h hρ hnd x = action N ρ π h hρ x := rfl
53 
54 /-- The actual multiplicity dimension satisfies the exact square equation. -/
55 theorem finrank_sq : Module.finrank ℂ (Space N ρ π) ^ 2 = Fintype.card (G ⧸ N) := by
56   let : Nontrivial (Space N ρ π) := multiplicity_nontrivial N ρ π h
57   exact TwistedActionEquivalence.finrank_sq (CliffordSource.cocycle N ρ π h hρ)
58     (CliffordSource.normalized N ρ π h hρ)
59     (fun a => (sectionOperator N ρ π hρ a).toLinearMap)
60     (congrArg LinearEquiv.toLinearMap (sectionOperator_one N ρ π hρ))
61     (CliffordSource.operator_mul N ρ π h hρ) hnd
62     (CliffordIrreducible.irreducible N ρ π h hρ)
63 
64 /-- Source 9.6's square-root formula, with no supplied multiplicity dimension. -/
65 theorem finrank_sqrt : Module.finrank ℂ (Space N ρ π) = Nat.sqrt (Fintype.card (G ⧸ N)) := by
66   rw [← finrank_sq N ρ π h hρ hnd, Nat.sqrt_eq']
67 
68 end PaperXI.CliffordPacket

Back to source controls