CliffordCocycleChoices.lean

1 import PaperXI.CliffordCocycle
2 
3 /-! Explicit cocycle and commutator comparisons for all actual section and
4 intertwiner choices in the Clifford construction. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CliffordCocycleChoices
8 open CliffordDatum CliffordMultiplicity CliffordChoices CocycleCommutator
9 open scoped IsMulCommutative
10 
11 variable {G W X : Type*} [Group G]
12 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
13 variable (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
14 variable (ρ : Representation ℂ N W) [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
15 variable (π : Representation ℂ G X) (hρ : Invariant N ρ) [Nontrivial (Space N ρ π)]
16 
17 /-- The cocycle for arbitrary actual choices, with its explicit constructed coboundary. -/
18 def choiceCocycle (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
19     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a))) : Cocycle (G ⧸ N) ℂˣ :=
20   rescale (CliffordCocycle.cocycle N ρ π hρ) (choiceCochain N ρ hρ s hs I)
21 
22 /-- The displayed coboundary is the multiplication cocycle of the actual chosen operators. -/
23 theorem choiceOperator_mul (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
24     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a))) (a b : G ⧸ N) :
25     (operator N ρ π (s a) (I a)).toLinearMap * (operator N ρ π (s b) (I b)).toLinearMap =
26       ((choiceCocycle N ρ π hρ s hs I).coeff a b : ℂ) •
27         (operator N ρ π (s (a * b)) (I (a * b))).toLinearMap :=
28   ProjectiveCocycle.rescaledFamily_mul
29     (fun a => (sectionOperator N ρ π hρ a).toLinearMap)
30     (fun a => (operator N ρ π (s a) (I a)).toLinearMap)
31     (CliffordCocycle.cocycle N ρ π hρ) (CliffordCocycle.sectionOperator_mul N ρ π hρ)
32     (choiceCochain N ρ hρ s hs I) (arbitrary_choices N ρ π hρ s hs I) a b
33 
34 /-- Every other coefficient family with the actual multiplication law is this cocycle. -/
35 theorem choiceCocycle_unique (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
36     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a))) (d : Cocycle (G ⧸ N) ℂˣ)
37     (hd : ∀ a b, (operator N ρ π (s a) (I a)).toLinearMap *
38       (operator N ρ π (s b) (I b)).toLinearMap =
39         (d.coeff a b : ℂ) • (operator N ρ π (s (a * b)) (I (a * b))).toLinearMap) :
40     d = choiceCocycle N ρ π hρ s hs I := by
41   have he (a b : G ⧸ N) : d.coeff a b = (choiceCocycle N ρ π hρ s hs I).coeff a b := by
42     apply ProjectiveCocycle.scalar_injective (operator N ρ π (s (a * b)) (I (a * b))).toLinearMap
43     · intro h
44       obtain ⟨f, hf⟩ := exists_ne (0 : Space N ρ π)
45       have hz := LinearMap.congr_fun h f
46       exact hf ((operator N ρ π (s (a * b)) (I (a * b))).injective
47         (hz.trans (operator N ρ π (s (a * b)) (I (a * b))).map_zero.symm))
48     · exact (hd a b).symm.trans (choiceOperator_mul N ρ π hρ s hs I a b)
49   have hcoeff := funext (fun a => funext (he a))
50   cases d
51   unfold choiceCocycle rescale
52   congr 1
53 
54 /-- The intrinsic commutator is unchanged by any section and intertwiner choices. -/
55 theorem commutator_choice (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
56     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a))) (a b : G ⧸ N) :
57     commutator (choiceCocycle N ρ π hρ s hs I) a b =
58       commutator (CliffordCocycle.cocycle N ρ π hρ) a b :=
59   commutator_rescale _ _ a b
60 
61 /-- Consequently the actual radical subgroup is choice independent. -/
62 theorem radical_choice (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
63     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a))) :
64     radical (choiceCocycle N ρ π hρ s hs I) = radical (CliffordCocycle.cocycle N ρ π hρ) :=
65   radical_rescale _ _
66 
67 /-- If the alternative actual identity operator is normalized, its comparing cochain is too. -/
68 theorem choiceCochain_one (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
69     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a)))
70     (hI : (operator N ρ π (s 1) (I 1)).toLinearMap = 1) :
71     choiceCochain N ρ hρ s hs I 1 = 1 := by
72   apply ProjectiveCocycle.cochain_one
73     (fun a => (sectionOperator N ρ π hρ a).toLinearMap)
74     (fun a => (operator N ρ π (s a) (I a)).toLinearMap)
75     (CliffordCocycle.sectionOperator_ne_zero N ρ π hρ 1)
76     _ hI (choiceCochain N ρ hρ s hs I) (arbitrary_choices N ρ π hρ s hs I)
77   exact congrArg LinearEquiv.toLinearMap (sectionOperator_one N ρ π hρ)
78 
79 /-- The actual cocycle of normalized choices is normalized. -/
80 theorem choiceCocycle_normalized (s : G ⧸ N → G) (hs : ∀ a, QuotientGroup.mk' N (s a) = a)
81     (I : ∀ a, Representation.Equiv ρ (conjugate N ρ (s a)))
82     (hI : (operator N ρ π (s 1) (I 1)).toLinearMap = 1) :
83     Normalized (choiceCocycle N ρ π hρ s hs I) :=
84   normalized_rescale _ (CliffordCocycle.normalized N ρ π hρ) _
85     (choiceCochain_one N ρ π hρ s hs I hI)
86 
87 end PaperXI.CliffordCocycleChoices

Back to source controls