CliffordTransport.lean

1 import PaperXI.CliffordCocycle
2 
3 /-! Actual transport of subgroup intertwiners and multiplicity operators
4 along isomorphisms of the original representation data. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.CliffordTransport
8 open CliffordDatum CliffordMultiplicity
9 
10 variable {G G' W W' X X' : Type*} [Group G] [Group G']
11 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup W'] [Module ℂ W']
12 variable [AddCommGroup X] [Module ℂ X] [AddCommGroup X'] [Module ℂ X']
13 
14 /-- The actual subgroup isomorphism induced by the group isomorphism. -/
15 def subgroupEquiv (N : Subgroup G) (N' : Subgroup G') (e : G ≃* G')
16     (hN : N.map e.toMonoidHom = N') : N ≃* N' where
17   toFun n := ⟨e n, by rw [← hN]; exact ⟨n, n.property, rfl⟩⟩
18   invFun n := ⟨e.symm n, by
19     have hn : (n : G') ∈ N.map e.toMonoidHom := hN.symm ▸ n.property
20     obtain ⟨g, hg, he⟩ := hn
21     simpa [← he] using hg⟩
22   left_inv n := by apply Subtype.ext; simp
23   right_inv n := by apply Subtype.ext; simp
24   map_mul' n m := by apply Subtype.ext; exact map_mul e (n : G) (m : G)
25 
26 @[simp] theorem subgroupEquiv_coe (N : Subgroup G) (N' : Subgroup G')
27     (e : G ≃* G') (hN : N.map e.toMonoidHom = N') (n : N) :
28     (subgroupEquiv N N' e hN n : G') = e n := rfl
29 
30 theorem subgroupEquiv_conjugation (N : Subgroup G) [N.Normal]
31     (N' : Subgroup G') [N'.Normal] (e : G ≃* G')
32     (hN : N.map e.toMonoidHom = N') (g : G) (n : N) :
33     subgroupEquiv N N' e hN (conjugation N g n) =
34       conjugation N' (e g) (subgroupEquiv N N' e hN n) := by
35   apply Subtype.ext
36   simp [map_mul]
37 
38 /-- The actual induced quotient group isomorphism. -/
39 def quotientEquiv (N : Subgroup G) [N.Normal] (N' : Subgroup G') [N'.Normal]
40     (e : G ≃* G') (hN : N.map e.toMonoidHom = N') : G ⧸ N ≃* G' ⧸ N' :=
41   QuotientGroup.congr N N' e hN
42 
43 @[simp] theorem quotientEquiv_mk (N : Subgroup G) [N.Normal]
44     (N' : Subgroup G') [N'.Normal] (e : G ≃* G')
45     (hN : N.map e.toMonoidHom = N') (g : G) :
46     quotientEquiv N N' e hN (QuotientGroup.mk' N g) = QuotientGroup.mk' N' (e g) :=
47   QuotientGroup.congr_mk' N N' e hN g
48 
49 /-- The induced quotient map preserves identity isomorphisms. -/
50 theorem quotientEquiv_refl (N : Subgroup G) [N.Normal]
51     (hN : N.map (MulEquiv.refl G).toMonoidHom = N) :
52     quotientEquiv N N (MulEquiv.refl G) hN = MulEquiv.refl (G ⧸ N) := by
53   apply MulEquiv.ext
54   intro a
55   obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective a
56   rfl
57 
58 /-- The actual quotient transport respects composition of group isomorphisms. -/
59 theorem quotientEquiv_comp {G'' : Type*} [Group G'']
60     (N : Subgroup G) [N.Normal] (N' : Subgroup G') [N'.Normal]
61     (N'' : Subgroup G'') [N''.Normal] (e : G ≃* G') (e' : G' ≃* G'')
62     (hN : N.map e.toMonoidHom = N') (hN' : N'.map e'.toMonoidHom = N'')
63     (hNN : N.map (e.trans e').toMonoidHom = N'') (a : G ⧸ N) :
64     quotientEquiv N' N'' e' hN' (quotientEquiv N N' e hN a) =
65       quotientEquiv N N'' (e.trans e') hNN a := by
66   obtain ⟨g, rfl⟩ := QuotientGroup.mk_surjective a
67   rfl
68 
69 variable (N : Subgroup G) (N' : Subgroup G') (e : G ≃* G')
70 variable (hN : N.map e.toMonoidHom = N')
71 variable (ρ : Representation ℂ N W) (ρ' : Representation ℂ N' W')
72 variable (π : Representation ℂ G X) (π' : Representation ℂ G' X')
73 variable (E : Representation.Equiv ρ (ρ'.comp (subgroupEquiv N N' e hN).toMonoidHom))
74 variable (F : Representation.Equiv π (π'.comp e.toMonoidHom))
75 
76 theorem source_apply (n : N) (w : W) :
77     E (ρ n w) = ρ' (subgroupEquiv N N' e hN n) (E w) :=
78   congrArg (fun L : W →ₗ[ℂ] W' => L w) (E.isIntertwining' n)
79 
80 theorem source_inverse_apply (n : N') (w : W') :
81     E.symm (ρ' n w) = ρ ((subgroupEquiv N N' e hN).symm n) (E.symm w) := by
82   have hi := congrArg (fun L : W' →ₗ[ℂ] W => L w)
83     (E.symm.isIntertwining' ((subgroupEquiv N N' e hN).symm n))
84   change E.symm (ρ' (subgroupEquiv N N' e hN ((subgroupEquiv N N' e hN).symm n)) w) = _ at hi
85   rw [MulEquiv.apply_symm_apply] at hi
86   exact hi
87 
88 theorem target_apply (g : G) (x : X) : F (π g x) = π' (e g) (F x) :=
89   congrArg (fun L : X →ₗ[ℂ] X' => L x) (F.isIntertwining' g)
90 
91 theorem target_inverse_apply (g : G') (x : X') :
92     F.symm (π' g x) = π (e.symm g) (F.symm x) := by
93   have hi := congrArg (fun L : X' →ₗ[ℂ] X => L x) (F.symm.isIntertwining' (e.symm g))
94   change F.symm (π' (e (e.symm g)) x) = _ at hi
95   rw [MulEquiv.apply_symm_apply] at hi
96   exact hi
97 
98 /-- Transport on the literal Hom spaces. -/
99 def homMap : Space N ρ π →ₗ[ℂ] Space N' ρ' π' where
100   toFun f :=
101     { toLinearMap := F.toLinearMap.comp (f.toLinearMap.comp E.symm.toLinearMap)
102       isIntertwining' n := by
103         apply LinearMap.ext
104         intro w
105         change F (f (E.symm (ρ' n w))) = π' (n : G') (F (f (E.symm w)))
106         rw [source_inverse_apply, space_intertwines, target_apply]
107         congr 2
108         have hh := congrArg (fun m : N' => (m : G')) ((subgroupEquiv N N' e hN).apply_symm_apply n)
109         exact hh }
110   map_add' f g := by ext w; simp
111   map_smul' c f := by ext w; simp
112 
113 @[simp] theorem homMap_apply (f : Space N ρ π) (w : W') :
114     homMap N N' e hN ρ ρ' π π' E F f w = F (f (E.symm w)) := rfl
115 
116 /-- The inverse transport on the literal Hom spaces. -/
117 def inverseHomMap : Space N' ρ' π' →ₗ[ℂ] Space N ρ π where
118   toFun f :=
119     { toLinearMap := F.symm.toLinearMap.comp (f.toLinearMap.comp E.toLinearMap)
120       isIntertwining' n := by
121         apply LinearMap.ext
122         intro w
123         change F.symm (f (E (ρ n w))) = π (n : G) (F.symm (f (E w)))
124         rw [source_apply, space_intertwines, target_inverse_apply]
125         simp }
126   map_add' f g := by ext w; simp
127   map_smul' c f := by ext w; simp
128 
129 /-- The actual multiplicity-space isomorphism induced by an isomorphism of data. -/
130 def homEquiv : Space N ρ π ≃ₗ[ℂ] Space N' ρ' π' where
131   __ := homMap N N' e hN ρ ρ' π π' E F
132   invFun := inverseHomMap N N' e hN ρ ρ' π π' E F
133   left_inv f := by
134     ext w
135     change F.symm (F (f (E.symm (E w)))) = f w
136     rw [Representation.Equiv.symm_apply_apply, Representation.Equiv.symm_apply_apply]
137   right_inv f := by
138     ext w
139     change F (F.symm (f (E (E.symm w)))) = f w
140     rw [Representation.Equiv.apply_symm_apply, Representation.Equiv.apply_symm_apply]
141 
142 @[simp] theorem homEquiv_apply (f : Space N ρ π) (w : W') :
143     homEquiv N N' e hN ρ ρ' π π' E F f w = F (f (E.symm w)) := rfl
144 
145 @[simp] theorem homEquiv_symm_apply (f : Space N' ρ' π') (w : W) :
146     (homEquiv N N' e hN ρ ρ' π π' E F).symm f w = F.symm (f (E w)) := rfl
147 
148 variable [N.Normal] [N'.Normal]
149 
150 /-- The transported conjugation intertwiner, constructed from the original datum map. -/
151 def transportedIntertwiner (g : G) (I : Representation.Equiv ρ (conjugate N ρ g)) :
152     Representation.Equiv ρ' (conjugate N' ρ' (e g)) :=
153   Representation.Equiv.mk
154     ((E.toLinearEquiv.symm.trans I.toLinearEquiv).trans E.toLinearEquiv) (by
155     intro n
156     apply LinearMap.ext
157     intro w
158     change E (I (E.symm (ρ' n w))) = ρ' (conjugation N' (e g) n) (E (I (E.symm w)))
159     rw [source_inverse_apply, intertwiner_apply, source_apply, subgroupEquiv_conjugation]
160     simp)
161 
162 @[simp] theorem transportedIntertwiner_apply (g : G)
163     (I : Representation.Equiv ρ (conjugate N ρ g)) (w : W') :
164     transportedIntertwiner N N' e hN ρ ρ' E g I w = E (I (E.symm w)) := rfl
165 
166 /-- Actual operators commute with the induced Hom-space map. -/
167 theorem operator_transport (g : G) (I : Representation.Equiv ρ (conjugate N ρ g))
168     (f : Space N ρ π) :
169     homEquiv N N' e hN ρ ρ' π π' E F (operator N ρ π g I f) =
170       operator N' ρ' π' (e g) (transportedIntertwiner N N' e hN ρ ρ' E g I)
171         (homEquiv N N' e hN ρ ρ' π π' E F f) := by
172   ext w
173   change F (π g (f (I.symm (E.symm w)))) =
174     π' (e g) (F (f (E.symm (E (I.symm (E.symm w))))))
175   rw [Representation.Equiv.symm_apply_apply, target_apply]
176 
177 /-- Conjugacy of the actual multiplicity operators as endomorphisms. -/
178 theorem operator_transport_conj (g : G) (I : Representation.Equiv ρ (conjugate N ρ g)) :
179     (operator N' ρ' π' (e g) (transportedIntertwiner N N' e hN ρ ρ' E g I)).toLinearMap =
180       (homEquiv N N' e hN ρ ρ' π π' E F).conj (operator N ρ π g I).toLinearMap := by
181   apply LinearMap.ext
182   intro f
183   have ht := operator_transport N N' e hN ρ ρ' π π' E F g I
184     ((homEquiv N N' e hN ρ ρ' π π' E F).symm f)
185   rw [LinearEquiv.apply_symm_apply] at ht
186   exact ht.symm
187 
188 /-- The transported representative has precisely the induced quotient class. -/
189 theorem transported_representative (a : G ⧸ N) :
190     QuotientGroup.mk' N' (e (sectionMap N a)) = quotientEquiv N N' e hN a := by
191   have hh := quotientEquiv_mk N N' e hN (sectionMap N a)
192   rw [quotient_section] at hh
193   exact hh.symm
194 
195 variable [Representation.IsIrreducible ρ'] [FiniteDimensional ℂ W']
196 
197 /-- The comparing cochain is obtained by Schur on the actual transported intertwiner. -/
198 def cochain (hρ : Invariant N ρ) (hρ' : Invariant N' ρ') (a : G ⧸ N) : ℂˣ :=
199   CliffordChoices.intertwinerScalar N' ρ' (e (sectionMap N a))
200     (CliffordChoices.representativeIntertwiner N' ρ' hρ'
201       (quotientEquiv N N' e hN a) (e (sectionMap N a))
202       (transported_representative N N' e hN a))
203     (transportedIntertwiner N N' e hN ρ ρ' E (sectionMap N a) (sectionIntertwiner N ρ hρ a))
204 
205 /-- Normalized section operators compare by the derived cochain and actual Hom conjugacy. -/
206 theorem sectionOperator_transport (hρ : Invariant N ρ) (hρ' : Invariant N' ρ')
207     (a : G ⧸ N) :
208     (sectionOperator N' ρ' π' hρ' (quotientEquiv N N' e hN a)).toLinearMap =
209       (cochain N N' e hN ρ ρ' E hρ hρ' a : ℂ) •
210         (homEquiv N N' e hN ρ ρ' π π' E F).conj (sectionOperator N ρ π hρ a).toLinearMap := by
211   let J := transportedIntertwiner N N' e hN ρ ρ' E (sectionMap N a) (sectionIntertwiner N ρ hρ a)
212   let K := CliffordChoices.representativeIntertwiner N' ρ' hρ'
213     (quotientEquiv N N' e hN a) (e (sectionMap N a))
214     (transported_representative N N' e hN a)
215   have hc := CliffordChoices.operator_choice N' ρ' π' (e (sectionMap N a)) K J
216   rw [CliffordChoices.operator_representative] at hc
217   change (operator N' ρ' π' (e (sectionMap N a)) J).toLinearMap =
218     (((cochain N N' e hN ρ ρ' E hρ hρ' a)⁻¹ : ℂˣ) : ℂ) •
219       (sectionOperator N' ρ' π' hρ' (quotientEquiv N N' e hN a)).toLinearMap at hc
220   have ht := operator_transport_conj N N' e hN ρ ρ' π π' E F (sectionMap N a)
221     (sectionIntertwiner N ρ hρ a)
222   calc
223     _ = (cochain N N' e hN ρ ρ' E hρ hρ' a : ℂ) •
224         (operator N' ρ' π' (e (sectionMap N a)) J).toLinearMap := by rw [hc]; simp [smul_smul]
225     _ = _ := by rw [ht]; rfl
226 
227 include E F
228 
229 /-- The actual comparison cochain is normalized because both chosen operator families are. -/
230 theorem cochain_one (hρ : Invariant N ρ) (hρ' : Invariant N' ρ')
231     [Nontrivial (Space N' ρ' π')] : cochain N N' e hN ρ ρ' E hρ hρ' 1 = 1 := by
232   apply ProjectiveCocycle.scalar_injective (1 : Module.End ℂ (Space N' ρ' π')) one_ne_zero
233   have hh := sectionOperator_transport N N' e hN ρ ρ' π π' E F hρ hρ' 1
234   simpa [sectionOperator_one, Module.End.one_eq_id] using hh.symm
235 
236 open scoped IsMulCommutative
237 open CocycleCommutator
238 variable [IsMulCommutative (G ⧸ N)] [IsMulCommutative (G' ⧸ N')]
239 variable [Representation.IsIrreducible ρ] [FiniteDimensional ℂ W]
240 variable [Nontrivial (Space N ρ π)] [Nontrivial (Space N' ρ' π')]
241 
242 /-- The actual cocycles differ by the explicitly constructed normalized coboundary. -/
243 theorem cocycle_transport (hρ : Invariant N ρ) (hρ' : Invariant N' ρ') (a b : G ⧸ N) :
244     (CliffordCocycle.cocycle N' ρ' π' hρ').coeff
245         (quotientEquiv N N' e hN a) (quotientEquiv N N' e hN b) =
246       cochain N N' e hN ρ ρ' E hρ hρ' a * cochain N N' e hN ρ ρ' E hρ hρ' b /
247         cochain N N' e hN ρ ρ' E hρ hρ' (a * b) * (CliffordCocycle.cocycle N ρ π hρ).coeff a b := by
248   apply ProjectiveCocycle.conjugate_rescale_coefficients
249     (fun a => (sectionOperator N ρ π hρ a).toLinearMap)
250     (fun a => (sectionOperator N' ρ' π' hρ' (quotientEquiv N N' e hN a)).toLinearMap)
251     (CliffordCocycle.sectionOperator_ne_zero N ρ π hρ)
252     (CliffordCocycle.cocycle N ρ π hρ).coeff
253     (fun a b => (CliffordCocycle.cocycle N' ρ' π' hρ').coeff
254       (quotientEquiv N N' e hN a) (quotientEquiv N N' e hN b))
255     (CliffordCocycle.sectionOperator_mul N ρ π hρ)
256     _ (homEquiv N N' e hN ρ ρ' π π' E F)
257     (cochain N N' e hN ρ ρ' E hρ hρ')
258     (sectionOperator_transport N N' e hN ρ ρ' π π' E F hρ hρ') a b
259   intro x y
260   rw [map_mul]
261   exact CliffordCocycle.sectionOperator_mul N' ρ' π' hρ'
262     (quotientEquiv N N' e hN x) (quotientEquiv N N' e hN y)
263 
264 /-- Isomorphisms of the original data preserve the intrinsic commutator pairing. -/
265 theorem commutator_preserved (hρ : Invariant N ρ) (hρ' : Invariant N' ρ') (a b : G ⧸ N) :
266     commutator (CliffordCocycle.cocycle N' ρ' π' hρ')
267       (quotientEquiv N N' e hN a) (quotientEquiv N N' e hN b) =
268       commutator (CliffordCocycle.cocycle N ρ π hρ) a b := by
269   exact ProjectiveCocycle.conjugate_rescale_commutator
270     (fun a => (sectionOperator N ρ π hρ a).toLinearMap)
271     (fun a => (sectionOperator N' ρ' π' hρ' a).toLinearMap)
272     (CliffordCocycle.sectionOperator_ne_zero N ρ π hρ)
273     (CliffordCocycle.cocycle N ρ π hρ) (CliffordCocycle.cocycle N' ρ' π' hρ')
274     (CliffordCocycle.sectionOperator_mul N ρ π hρ)
275     (CliffordCocycle.sectionOperator_mul N' ρ' π' hρ')
276     (homEquiv N N' e hN ρ ρ' π π' E F) (quotientEquiv N N' e hN)
277     (cochain N N' e hN ρ ρ' E hρ hρ')
278     (sectionOperator_transport N N' e hN ρ ρ' π π' E F hρ hρ') a b
279 
280 end PaperXI.CliffordTransport

Back to source controls