CliffordStabilizer.lean

1 import PaperXI.CliffordDatum
2 import PaperXI.CliffordSource
3 import PaperXI.CliffordEnvelope
4 import PaperXI.CliffordTransport
5 import PaperXI.ElementaryEnvelopeTransport
6 import Mathlib.GroupTheory.QuotientGroup.Basic
7 
8 /-! The honest action induced on a normal quotient by ambient group
9 automorphisms. No coherent choices of representation intertwiners enter. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.CliffordStabilizer
13 open CocycleCommutator
14 open scoped IsMulCommutative
15 
16 variable {G C : Type*} [Group G] [Group C]
17 
18 /-- Actual ambient automorphisms preserving a normal subgroup give an honest
19 quotient action. Its group law is inherited from the ambient action. -/
20 def quotientAction (N : Subgroup G) [N.Normal] (α : C →* MulAut G)
21     (hN : ∀ g, N.map (α g).toMonoidHom = N) : C →* MulAut (G ⧸ N) where
22   toFun g := QuotientGroup.congr N N (α g) (hN g)
23   map_one' := by
24     ext x
25     induction x using QuotientGroup.induction_on with | H a =>
26       change QuotientGroup.mk (α 1 a) = QuotientGroup.mk a
27       rw [map_one]
28       rfl
29   map_mul' g h := by
30     ext x
31     induction x using QuotientGroup.induction_on with | H a =>
32       change QuotientGroup.mk (α (g * h) a) = QuotientGroup.mk (α g (α h a))
33       rw [map_mul]
34       rfl
35 
36 @[simp] theorem quotientAction_mk (N : Subgroup G) [N.Normal] (α : C →* MulAut G)
37     (hN : ∀ g, N.map (α g).toMonoidHom = N) (g : C) (a : G) :
38     quotientAction N α hN g (QuotientGroup.mk a) = QuotientGroup.mk (α g a) := rfl
39 
40 /-- The induced quotient action intertwines the original quotient homomorphism. -/
41 theorem quotientAction_comp (N : Subgroup G) [N.Normal] (α : C →* MulAut G)
42     (hN : ∀ g, N.map (α g).toMonoidHom = N) (g : C) :
43     (quotientAction N α hN g).toMonoidHom.comp (QuotientGroup.mk' N) =
44       (QuotientGroup.mk' N).comp (α g).toMonoidHom := rfl
45 
46 /-- No auxiliary representation choices can change the induced quotient action. -/
47 theorem quotientAction_unique (N : Subgroup G) [N.Normal] (α : C →* MulAut G)
48     (hN : ∀ g, N.map (α g).toMonoidHom = N) (β : C →* MulAut (G ⧸ N))
49     (hβ : ∀ g a, β g (QuotientGroup.mk a) = QuotientGroup.mk (α g a)) :
50     β = quotientAction N α hN := by
51   apply MonoidHom.ext
52   intro g
53   ext x
54   induction x using QuotientGroup.induction_on with | H a => exact hβ g a
55 
56 section Envelope
57 variable {p : ℕ} [Fact p.Prime]
58 variable (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
59 variable [Fact (∀ a : G ⧸ N, a ^ p = 1)]
60 variable (c : Cocycle (G ⧸ N) ℂˣ) (α : C →* MulAut G)
61 variable (hN : ∀ g, N.map (α g).toMonoidHom = N)
62 variable (hα : ∀ g a b, commutator c (quotientAction N α hN g a)
63   (quotientAction N α hN g b) = commutator c a b)
64 
65 /-- The ambient quotient action descends further to the actual linear envelope
66 once preservation of its intrinsic scalar pairing has been established. -/
67 def envelopeAction : C →* (ElementaryEnvelope.Space c ≃ₗ[ZMod p] ElementaryEnvelope.Space c) :=
68   ElementaryEnvelope.action c (quotientAction N α hN) hα
69 
70 @[simp] theorem envelopeAction_mk (g : C) (a : G) :
71     envelopeAction (p := p) N c α hN hα g
72       (Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N a))) =
73       Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N (α g a))) := rfl
74 
75 /-- Every induced envelope automorphism preserves its actual alternating form. -/
76 theorem envelopeAction_form (g : C) (x y : ElementaryEnvelope.Space c) :
77     ElementaryEnvelope.form (p := p) c
78       (envelopeAction (p := p) N c α hN hα g x)
79       (envelopeAction (p := p) N c α hN hα g y) =
80       ElementaryEnvelope.form (p := p) c x y :=
81   ElementaryEnvelope.action_form c (quotientAction N α hN) hα g x y
82 
83 end Envelope
84 section Equivariance
85 variable {G' : Type*} [Group G'] {p : ℕ} [Fact p.Prime]
86 
87 /-- Isomorphisms intertwining the original ambient actions intertwine the
88 constructed linear envelope actions on every quotient vector. -/
89 theorem envelopeAction_equivariant
90     (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
91     (N' : Subgroup G') [N'.Normal] [IsMulCommutative (G' ⧸ N')]
92     [Fact (∀ a : G ⧸ N, a ^ p = 1)] [Fact (∀ a : G' ⧸ N', a ^ p = 1)]
93     (c : Cocycle (G ⧸ N) ℂˣ) (d : Cocycle (G' ⧸ N') ℂˣ)
94     (α : C →* MulAut G) (β : C →* MulAut G')
95     (hN : ∀ g, N.map (α g).toMonoidHom = N)
96     (hN' : ∀ g, N'.map (β g).toMonoidHom = N')
97     (hα : ∀ g a b, commutator c (quotientAction N α hN g a)
98       (quotientAction N α hN g b) = commutator c a b)
99     (hβ : ∀ g a b, commutator d (quotientAction N' β hN' g a)
100       (quotientAction N' β hN' g b) = commutator d a b)
101     (e : G ≃* G') (heN : N.map e.toMonoidHom = N')
102     (he : ∀ a b, commutator d (CliffordTransport.quotientEquiv N N' e heN a)
103       (CliffordTransport.quotientEquiv N N' e heN b) = commutator c a b)
104     (hEquiv : ∀ g a, e (α g a) = β g (e a))
105     (g : C) (x : ElementaryEnvelope.Space c) :
106     ElementaryEnvelope.linearEquiv (p := p) c d
107       (CliffordTransport.quotientEquiv N N' e heN) he
108       (envelopeAction (p := p) N c α hN hα g x) =
109     envelopeAction (p := p) N' d β hN' hβ g
110       (ElementaryEnvelope.linearEquiv (p := p) c d
111         (CliffordTransport.quotientEquiv N N' e heN) he x) := by
112   apply ElementaryEnvelope.space_induction_on c x
113   intro a
114   induction a using QuotientGroup.induction_on with | H t =>
115     change Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N' (e (α g t)))) =
116       Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N' (β g (e t))))
117     rw [hEquiv]
118 
119 end Equivariance
120 
121 section Source
122 variable {W X : Type*} [AddCommGroup W] [Module ℂ W]
123 variable [AddCommGroup X] [Module ℂ X] [Finite G]
124 variable (N : Subgroup G) [N.Normal] [IsMulCommutative (G ⧸ N)]
125 variable (ρ : Representation ℂ N W) (π : Representation ℂ G X)
126 variable [Representation.IsIrreducible ρ] [Representation.IsIrreducible π]
127 variable (hIso : CliffordIrreducible.Isotypic N ρ π) (hρ : CliffordDatum.Invariant N ρ)
128 variable (α : C →* MulAut G) (hN : ∀ g, N.map (α g).toMonoidHom = N)
129 variable (E : ∀ g, Representation.Equiv ρ
130   (ρ.comp (CliffordTransport.subgroupEquiv N N (α g) (hN g)).toMonoidHom))
131 variable (F : ∀ g, Representation.Equiv π (π.comp (α g).toMonoidHom))
132 
133 include E F
134 
135 /-- Actual automorphisms of the original representation datum preserve the
136 intrinsic Clifford commutator. The comparison intertwiners need no group law. -/
137 theorem source_commutator_preserved (g : C) (a b : G ⧸ N) :
138     commutator (CliffordSource.cocycle N ρ π hIso hρ)
139       (quotientAction N α hN g a) (quotientAction N α hN g b) =
140       commutator (CliffordSource.cocycle N ρ π hIso hρ) a b := by
141   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
142   let : Nontrivial (CliffordMultiplicity.Space N ρ π) :=
143     CliffordIrreducible.multiplicity_nontrivial N ρ π hIso
144   exact CliffordTransport.commutator_preserved N N (α g) (hN g)
145     ρ ρ π π (E g) (F g) hρ hρ a b
146 
147 variable {p : ℕ} [Fact p.Prime] [Fact (∀ a : G ⧸ N, a ^ p = 1)]
148 
149 /-- Source 9.8: the original datum automorphisms give a genuine linear action
150 on the actual Clifford envelope. Auxiliary intertwiners are only witnesses. -/
151 def sourceAction : C →*
152     (ElementaryEnvelope.Space (CliffordSource.cocycle N ρ π hIso hρ) ≃ₗ[ZMod p]
153       ElementaryEnvelope.Space (CliffordSource.cocycle N ρ π hIso hρ)) :=
154   envelopeAction N (CliffordSource.cocycle N ρ π hIso hρ) α hN
155     (source_commutator_preserved N ρ π hIso hρ α hN E F)
156 
157 @[simp] theorem sourceAction_mk (g : C) (a : G) :
158     sourceAction (p := p) N ρ π hIso hρ α hN E F g
159       (Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N a))) =
160       Additive.ofMul (QuotientGroup.mk (QuotientGroup.mk' N (α g a))) := rfl
161 
162 /-- Every actual stabilizer element preserves the constructed symplectic form. -/
163 theorem sourceAction_form (g : C)
164     (x y : ElementaryEnvelope.Space (CliffordSource.cocycle N ρ π hIso hρ)) :
165     ElementaryEnvelope.form (p := p) (CliffordSource.cocycle N ρ π hIso hρ)
166       (sourceAction (p := p) N ρ π hIso hρ α hN E F g x)
167       (sourceAction (p := p) N ρ π hIso hρ α hN E F g y) =
168       ElementaryEnvelope.form (p := p) (CliffordSource.cocycle N ρ π hIso hρ) x y :=
169   envelopeAction_form N (CliffordSource.cocycle N ρ π hIso hρ) α hN
170     (source_commutator_preserved N ρ π hIso hρ α hN E F) g x y
171 
172 /-- Changing the individual representation comparison witnesses leaves the
173 genuine envelope action unchanged, even without coherent witness choices. -/
174 theorem sourceAction_independent
175     (E' : ∀ g, Representation.Equiv ρ
176       (ρ.comp (CliffordTransport.subgroupEquiv N N (α g) (hN g)).toMonoidHom))
177     (F' : ∀ g, Representation.Equiv π (π.comp (α g).toMonoidHom)) :
178     sourceAction (p := p) N ρ π hIso hρ α hN E F =
179       sourceAction (p := p) N ρ π hIso hρ α hN E' F' := rfl
180 
181 section Transport
182 variable {G' W' X' : Type*} [Group G'] [Finite G']
183 variable [AddCommGroup W'] [Module ℂ W'] [AddCommGroup X'] [Module ℂ X']
184 variable (N' : Subgroup G') [N'.Normal] [IsMulCommutative (G' ⧸ N')]
185 variable (ρ' : Representation ℂ N' W') (π' : Representation ℂ G' X')
186 variable [Representation.IsIrreducible ρ'] [Representation.IsIrreducible π']
187 variable (hIso' : CliffordIrreducible.Isotypic N' ρ' π') (hρ' : CliffordDatum.Invariant N' ρ')
188 variable [Fact (∀ a : G' ⧸ N', a ^ p = 1)]
189 variable (β : C →* MulAut G') (hN' : ∀ g, N'.map (β g).toMonoidHom = N')
190 variable (E' : ∀ g, Representation.Equiv ρ'
191   (ρ'.comp (CliffordTransport.subgroupEquiv N' N' (β g) (hN' g)).toMonoidHom))
192 variable (F' : ∀ g, Representation.Equiv π' (π'.comp (β g).toMonoidHom))
193 variable (e : G ≃* G') (heN : N.map e.toMonoidHom = N')
194 variable (E₀ : Representation.Equiv ρ
195   (ρ'.comp (CliffordTransport.subgroupEquiv N N' e heN).toMonoidHom))
196 variable (F₀ : Representation.Equiv π (π'.comp e.toMonoidHom))
197 
198 /-- The source datum isometry is equivariant for the actual stabilizer actions
199 whenever the original ambient datum isomorphism intertwines those actions. -/
200 theorem sourceAction_equivariant (hEquiv : ∀ g a, e (α g a) = β g (e a))
201     (g : C) (x : CliffordEnvelope.Space N ρ π hIso hρ) :
202     CliffordEnvelope.equiv (p := p) N ρ π hIso hρ N' ρ' π' hIso' hρ' e heN E₀ F₀
203       (sourceAction (p := p) N ρ π hIso hρ α hN E F g x) =
204     sourceAction (p := p) N' ρ' π' hIso' hρ' β hN' E' F' g
205       (CliffordEnvelope.equiv (p := p) N ρ π hIso hρ N' ρ' π' hIso' hρ' e heN E₀ F₀ x) := by
206   exact envelopeAction_equivariant N N'
207     (CliffordSource.cocycle N ρ π hIso hρ) (CliffordSource.cocycle N' ρ' π' hIso' hρ')
208     α β hN hN'
209     (source_commutator_preserved N ρ π hIso hρ α hN E F)
210     (source_commutator_preserved N' ρ' π' hIso' hρ' β hN' E' F')
211     e heN (CliffordEnvelope.commutator_preserved N ρ π hIso hρ
212       N' ρ' π' hIso' hρ' e heN E₀ F₀) hEquiv g x
213 
214 end Transport
215 end Source
216 end PaperXI.CliffordStabilizer

Back to source controls