CliffordMultiplicity.lean

1 import PaperXI.CliffordDatum
2 
3 /-! Invertible operators on the actual space of subgroup intertwiners. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.CliffordMultiplicity
7 open CliffordDatum
8 
9 variable {G W X : Type*} [Group G]
10 variable [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
11 
12 /-- The actual multiplicity space, with no tensor identification supplied. -/
13 abbrev Space (N : Subgroup G) (ρ : Representation ℂ N W) (π : Representation ℂ G X) :=
14   Representation.IntertwiningMap ρ (restriction N π)
15 
16 theorem space_intertwines (N : Subgroup G) (ρ : Representation ℂ N W)
17     (π : Representation ℂ G X) (f : Space N ρ π) (n : N) (w : W) :
18     f (ρ n w) = π (n : G) (f w) := congrArg (fun F : W →ₗ[ℂ] X => F w) (f.isIntertwining' n)
19 
20 theorem inverse_intertwines (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
21     (g : G) (I : Representation.Equiv ρ (conjugate N ρ g)) (n : N) (w : W) :
22     I.symm (ρ n w) = ρ (conjugation N g⁻¹ n) (I.symm w) := by
23   have hi := congrArg (fun F : W →ₗ[ℂ] W => F w) (I.symm.isIntertwining' (conjugation N g⁻¹ n))
24   change I.symm (ρ (conjugation N g (conjugation N g⁻¹ n)) w) = _ at hi
25   simpa using hi
26 
27 theorem action_conjugation (N : Subgroup G) [N.Normal] (π : Representation ℂ G X)
28     (g : G) (n : N) (x : X) :
29     π g (π (conjugation N g⁻¹ n : G) x) = π (n : G) (π g x) := by
30   change (π g * π (conjugation N g⁻¹ n : G)) x = (π (n : G) * π g) x
31   rw [← map_mul, ← map_mul]
32   simp [mul_assoc]
33 
34 /-- Literal forward operator; subgroup equivariance is proved in the definition. -/
35 def operatorMap (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
36     (π : Representation ℂ G X) (g : G)
37     (I : Representation.Equiv ρ (conjugate N ρ g)) : Space N ρ π →ₗ[ℂ] Space N ρ π where
38   toFun f :=
39     { toLinearMap := (π g).comp (f.toLinearMap.comp I.symm.toLinearMap)
40       isIntertwining' n := by
41         apply LinearMap.ext
42         intro w
43         change π g (f (I.symm (ρ n w))) = π (n : G) (π g (f (I.symm w)))
44         rw [inverse_intertwines, space_intertwines, action_conjugation] }
45   map_add' f h := by ext w; simp
46   map_smul' c f := by ext w; simp
47 
48 @[simp] theorem operatorMap_apply (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
49     (π : Representation ℂ G X) (g : G)
50     (I : Representation.Equiv ρ (conjugate N ρ g)) (f : Space N ρ π) (w : W) :
51     operatorMap N ρ π g I f w = π g (f (I.symm w)) := rfl
52 
53 /-- Literal inverse operator, proved to preserve the same actual Hom space. -/
54 def inverseMap (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
55     (π : Representation ℂ G X) (g : G)
56     (I : Representation.Equiv ρ (conjugate N ρ g)) : Space N ρ π →ₗ[ℂ] Space N ρ π where
57   toFun f :=
58     { toLinearMap := (π g⁻¹).comp (f.toLinearMap.comp I.toLinearMap)
59       isIntertwining' n := by
60         apply LinearMap.ext
61         intro w
62         change π g⁻¹ (f (I (ρ n w))) = π (n : G) (π g⁻¹ (f (I w)))
63         have hi := congrArg (fun F : W →ₗ[ℂ] W => F w) (I.isIntertwining' n)
64         change I (ρ n w) = ρ (conjugation N g n) (I w) at hi
65         rw [hi]
66         change π g⁻¹ (f (ρ (conjugation N g n) (I w))) = _
67         rw [space_intertwines]
68         have ha := action_conjugation N π g⁻¹ n (f (I w))
69         simp only [inv_inv] at ha
70         exact ha }
71   map_add' f h := by ext w; simp
72   map_smul' c f := by ext w; simp
73 
74 @[simp] theorem inverseMap_apply (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
75     (π : Representation ℂ G X) (g : G)
76     (I : Representation.Equiv ρ (conjugate N ρ g)) (f : Space N ρ π) (w : W) :
77     inverseMap N ρ π g I f w = π g⁻¹ (f (I w)) := rfl
78 
79 /-- The invertible Clifford multiplicity operator. -/
80 def operator (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
81     (π : Representation ℂ G X) (g : G)
82     (I : Representation.Equiv ρ (conjugate N ρ g)) : Space N ρ π ≃ₗ[ℂ] Space N ρ π where
83   __ := operatorMap N ρ π g I
84   invFun := inverseMap N ρ π g I
85   left_inv f := by
86     ext w
87     change π g⁻¹ (π g (f (I.symm (I w)))) = f w
88     rw [Representation.Equiv.symm_apply_apply]
89     change (π g⁻¹ * π g) (f w) = f w
90     rw [← map_mul, inv_mul_cancel, map_one]
91     rfl
92   right_inv f := by
93     ext w
94     change π g (π g⁻¹ (f (I (I.symm w)))) = f w
95     rw [Representation.Equiv.apply_symm_apply]
96     change (π g * π g⁻¹) (f w) = f w
97     rw [← map_mul, mul_inv_cancel, map_one]
98     rfl
99 
100 @[simp] theorem operator_apply (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
101     (π : Representation ℂ G X) (g : G)
102     (I : Representation.Equiv ρ (conjugate N ρ g)) (f : Space N ρ π) (w : W) :
103     operator N ρ π g I f w = π g (f (I.symm w)) := rfl
104 
105 @[simp] theorem operator_symm_apply (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
106     (π : Representation ℂ G X) (g : G)
107     (I : Representation.Equiv ρ (conjugate N ρ g)) (f : Space N ρ π) (w : W) :
108     (operator N ρ π g I).symm f w = π g⁻¹ (f (I w)) := rfl
109 
110 /-- The normalized family obtained from the actual quotient section and invariance. -/
111 def sectionOperator (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
112     (π : Representation ℂ G X) (hρ : Invariant N ρ) (a : G ⧸ N) :
113     Space N ρ π ≃ₗ[ℂ] Space N ρ π :=
114   operator N ρ π (sectionMap N a) (sectionIntertwiner N ρ hρ a)
115 
116 theorem sectionOperator_one (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
117     (π : Representation ℂ G X) (hρ : Invariant N ρ) :
118     sectionOperator N ρ π hρ 1 = LinearEquiv.refl ℂ (Space N ρ π) := by
119   ext f w
120   change π (sectionMap N 1) (f ((sectionIntertwiner N ρ hρ 1).symm w)) = f w
121   have hi : (sectionIntertwiner N ρ hρ 1).symm w = w := by
122     calc
123       _ = (sectionIntertwiner N ρ hρ 1).symm (sectionIntertwiner N ρ hρ 1 w) := by rw [sectionIntertwiner_one]
124       _ = w := (sectionIntertwiner N ρ hρ 1).symm_apply_apply w
125   simp [hi]
126 
127 /-- Pointwise form of an actual conjugation intertwiner. -/
128 theorem intertwiner_apply (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
129     (g : G) (I : Representation.Equiv ρ (conjugate N ρ g)) (n : N) (w : W) :
130     I (ρ n w) = ρ (conjugation N g n) (I w) :=
131   congrArg (fun F : W →ₗ[ℂ] W => F w) (I.isIntertwining' n)
132 
133 /-- Compose the actual conjugation intertwiners in the source convention. -/
134 def productIntertwiner (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
135     (g h : G) (I : Representation.Equiv ρ (conjugate N ρ g))
136     (J : Representation.Equiv ρ (conjugate N ρ h)) :
137     Representation.Equiv ρ (conjugate N ρ (g * h)) :=
138   Representation.Equiv.mk (J.toLinearEquiv.trans I.toLinearEquiv) (by
139     intro n
140     apply LinearMap.ext
141     intro w
142     change I (J (ρ n w)) = ρ (conjugation N (g * h) n) (I (J w))
143     rw [intertwiner_apply, intertwiner_apply, conjugation_mul])
144 
145 @[simp] theorem productIntertwiner_apply (N : Subgroup G) [N.Normal]
146     (ρ : Representation ℂ N W) (g h : G)
147     (I : Representation.Equiv ρ (conjugate N ρ g))
148     (J : Representation.Equiv ρ (conjugate N ρ h)) (w : W) :
149     productIntertwiner N ρ g h I J w = I (J w) := rfl
150 
151 /-- Any group action operator, with its actual inverse action. -/
152 def actionEquiv {K Y : Type*} [Group K] [AddCommGroup Y] [Module ℂ Y]
153     (τ : Representation ℂ K Y) (k : K) : Y ≃ₗ[ℂ] Y where
154   __ := τ k
155   invFun := τ k⁻¹
156   left_inv y := by
157     change (τ k⁻¹ * τ k) y = y
158     rw [← map_mul, inv_mul_cancel, map_one]
159     rfl
160   right_inv y := by
161     change (τ k * τ k⁻¹) y = y
162     rw [← map_mul, mul_inv_cancel, map_one]
163     rfl
164 
165 @[simp] theorem actionEquiv_apply {K Y : Type*} [Group K] [AddCommGroup Y] [Module ℂ Y]
166     (τ : Representation ℂ K Y) (k : K) (y : Y) : actionEquiv τ k y = τ k y := rfl
167 
168 /-- The adjusted intertwiner for multiplication of a representative by `n ∈ N`. -/
169 def subgroupIntertwiner (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
170     (n : N) (g : G) (I : Representation.Equiv ρ (conjugate N ρ g)) :
171     Representation.Equiv ρ (conjugate N ρ ((n : G) * g)) :=
172   Representation.Equiv.mk (I.toLinearEquiv.trans (actionEquiv ρ n)) (by
173     intro m
174     apply LinearMap.ext
175     intro w
176     change ρ n (I (ρ m w)) = ρ (conjugation N ((n : G) * g) m) (ρ n (I w))
177     rw [intertwiner_apply]
178     change (ρ n * ρ (conjugation N g m)) (I w) =
179       (ρ (conjugation N ((n : G) * g) m) * ρ n) (I w)
180     rw [← map_mul, ← map_mul]
181     congr 2
182     apply Subtype.ext
183     simp [mul_assoc])
184 
185 @[simp] theorem subgroupIntertwiner_apply (N : Subgroup G) [N.Normal]
186     (ρ : Representation ℂ N W) (n : N) (g : G)
187     (I : Representation.Equiv ρ (conjugate N ρ g)) (w : W) :
188     subgroupIntertwiner N ρ n g I w = ρ n (I w) := rfl
189 
190 /-- The section-defect-adjusted intertwiner with exactly the product representative target. -/
191 def defectIntertwiner (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
192     (hρ : Invariant N ρ) (a b : G ⧸ N) :
193     Representation.Equiv ρ (conjugate N ρ (sectionMap N a * sectionMap N b)) :=
194   Representation.Equiv.mk
195     (subgroupIntertwiner N ρ (defect N a b) (sectionMap N (a * b))
196       (sectionIntertwiner N ρ hρ (a * b))).toLinearEquiv (by
197     intro n
198     apply LinearMap.ext
199     intro w
200     have hi := intertwiner_apply N ρ
201       ((defect N a b : G) * sectionMap N (a * b))
202       (subgroupIntertwiner N ρ (defect N a b) (sectionMap N (a * b))
203         (sectionIntertwiner N ρ hρ (a * b))) n w
204     change ρ (defect N a b) (sectionIntertwiner N ρ hρ (a * b) (ρ n w)) =
205       ρ (conjugation N ((defect N a b : G) * sectionMap N (a * b)) n)
206         (ρ (defect N a b) (sectionIntertwiner N ρ hρ (a * b) w)) at hi
207     rw [← section_mul] at hi
208     exact hi)
209 
210 @[simp] theorem defectIntertwiner_apply (N : Subgroup G) [N.Normal]
211     (ρ : Representation ℂ N W) (hρ : Invariant N ρ) (a b : G ⧸ N) (w : W) :
212     defectIntertwiner N ρ hρ a b w = ρ (defect N a b) (sectionIntertwiner N ρ hρ (a * b) w) := rfl
213 
214 /-- Multiplicity composition follows the reversed inverse composition on `W`. -/
215 theorem operator_product (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
216     (π : Representation ℂ G X) (g h : G)
217     (I : Representation.Equiv ρ (conjugate N ρ g))
218     (J : Representation.Equiv ρ (conjugate N ρ h)) :
219     (operator N ρ π g I).toLinearMap * (operator N ρ π h J).toLinearMap =
220       (operator N ρ π (g * h) (productIntertwiner N ρ g h I J)).toLinearMap := by
221   ext f w
222   change π g (π h (f (J.symm (I.symm w)))) = π (g * h) (f (J.symm (I.symm w)))
223   rw [map_mul]
224   rfl
225 
226 /-- Changing the representative by an actual subgroup factor cancels on `Hom_N`. -/
227 theorem operator_subgroup_mul (N : Subgroup G) [N.Normal] (ρ : Representation ℂ N W)
228     (π : Representation ℂ G X) (n : N) (g : G)
229     (I : Representation.Equiv ρ (conjugate N ρ g)) :
230     operator N ρ π ((n : G) * g) (subgroupIntertwiner N ρ n g I) = operator N ρ π g I := by
231   ext f w
232   let T := operator N ρ π g I f
233   change π ((n : G) * g) (f (I.symm (ρ n⁻¹ w))) = π g (f (I.symm w))
234   rw [map_mul]
235   change π (n : G) (T (ρ n⁻¹ w)) = T w
236   rw [space_intertwines]
237   change (π (n : G) * π (n⁻¹ : N)) (T w) = T w
238   rw [← map_mul]
239   simp
240 
241 end PaperXI.CliffordMultiplicity

Back to source controls