CliffordEvaluation.lean

1 import PaperXI.IsotypicEvaluation
2 import PaperXI.FiniteRepresentation
3 import PaperXI.CliffordMultiplicity
4 import Mathlib.RepresentationTheory.Maschke
5 import Mathlib.LinearAlgebra.TensorProduct.Map
6 
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.CliffordEvaluation
10 
11 open scoped TensorProduct MonoidAlgebra
12 open Representation
13 
14 variable {N W X : Type*} [Group N]
15   [AddCommGroup W] [Module ℂ W] [AddCommGroup X] [Module ℂ X]
16   (ρ : Representation ℂ N W) (σ : Representation ℂ N X)
17 
18 /-- Evaluation on the actual multiplicity space of intertwining maps. -/
19 def map : W ⊗[ℂ] IntertwiningMap ρ σ →ₗ[ℂ] X :=
20   TensorProduct.lift
21     { toFun := fun w =>
22         { toFun := fun f => f w
23           map_add' := fun _ _ => rfl
24           map_smul' := fun _ _ => rfl }
25       map_add' := by intro w v; ext f; exact f.toLinearMap.map_add w v
26       map_smul' := by intro c w; ext f; exact f.toLinearMap.map_smul c w }
27 
28 @[simp] theorem map_tmul (w : W) (f : IntertwiningMap ρ σ) :
29     map ρ σ (w ⊗ₜ[ℂ] f) = f w := rfl
30 
31 /-- Evaluation intertwines the literal restricted group action. -/
32 theorem map_action (n : N) (t : W ⊗[ℂ] IntertwiningMap ρ σ) :
33     map ρ σ (TensorProduct.map (ρ n) LinearMap.id t) = σ n (map ρ σ t) := by
34   induction t using TensorProduct.induction_on with
35   | zero => simp
36   | add u v hu hv => simp [hu, hv]
37   | tmul w f => simpa using IntertwiningMap.isIntertwining ρ σ f n w
38 
39 /-- Genuine module isotypy gives canonical evaluation bijectivity. -/
40 theorem bijective [Finite N] [IsIrreducible ρ] [FiniteDimensional ℂ X]
41     (h : IsIsotypicOfType ℂ[N] σ.asModule ρ.asModule) :
42     Function.Bijective (map ρ σ) := by
43   let : FiniteDimensional ℂ W := FiniteRepresentation.finiteDimensional ρ
44   let : Module.Finite ℂ[N] σ.asModule :=
45     Module.Finite.of_restrictScalars_finite ℂ ℂ[N] σ.asModule
46   let E : W ⊗[ℂ] IntertwiningMap ρ σ ≃ₗ[ℂ] X :=
47     ((TensorProduct.congr ρ.asModuleEquiv.symm (IntertwiningMap.equivLinearMapAsModule ρ σ)).trans
48       (IsotypicEvaluation.equiv h)).trans σ.asModuleEquiv
49   have hE : E.toLinearMap = map ρ σ := by
50     ext w f
51     rfl
52   exact hE ▸ E.bijective
53 
54 /-- The actual isotypic evaluation equivalence. -/
55 def equiv [Finite N] [IsIrreducible ρ] [FiniteDimensional ℂ X]
56     (h : IsIsotypicOfType ℂ[N] σ.asModule ρ.asModule) :
57     W ⊗[ℂ] IntertwiningMap ρ σ ≃ₗ[ℂ] X :=
58   LinearEquiv.ofBijective (map ρ σ) (bijective ρ σ h)
59 
60 @[simp] theorem equiv_tmul [Finite N] [IsIrreducible ρ] [FiniteDimensional ℂ X]
61     (h : IsIsotypicOfType ℂ[N] σ.asModule ρ.asModule)
62     (w : W) (f : IntertwiningMap ρ σ) : equiv ρ σ h (w ⊗ₜ[ℂ] f) = f w := rfl
63 
64 theorem equiv_action [Finite N] [IsIrreducible ρ] [FiniteDimensional ℂ X]
65     (h : IsIsotypicOfType ℂ[N] σ.asModule ρ.asModule)
66     (n : N) (t : W ⊗[ℂ] IntertwiningMap ρ σ) :
67     equiv ρ σ h (TensorProduct.map (ρ n) LinearMap.id t) = σ n (equiv ρ σ h t) :=
68   map_action ρ σ n t
69 
70 /-- Nonzero isotypic representations have nonzero actual multiplicity spaces. -/
71 theorem multiplicity_nontrivial [Finite N] [IsIrreducible ρ] [FiniteDimensional ℂ X]
72     [Nontrivial X] (h : IsIsotypicOfType ℂ[N] σ.asModule ρ.asModule) :
73     Nontrivial (IntertwiningMap ρ σ) := by
74   by_contra hn
75   let : Subsingleton (IntertwiningMap ρ σ) := not_nontrivial_iff_subsingleton.mp hn
76   have : Subsingleton X := (equiv ρ σ h).symm.injective.subsingleton
77   exact not_subsingleton X this
78 
79 /-- Currying an equivariant tensor map produces an actual multiplicity endomorphism. -/
80 def choiceMap (E : W ⊗[ℂ] IntertwiningMap ρ σ →ₗ[ℂ] X)
81     (hE : ∀ (n : N) (w : W) (f : IntertwiningMap ρ σ),
82       E ((ρ n w) ⊗ₜ[ℂ] f) = σ n (E (w ⊗ₜ[ℂ] f))) :
83     IntertwiningMap ρ σ →ₗ[ℂ] IntertwiningMap ρ σ where
84   toFun f :=
85     { toLinearMap := E.comp ((TensorProduct.mk ℂ W (IntertwiningMap ρ σ)).flip f)
86       isIntertwining' n := by ext w; exact hE n w f }
87   map_add' f g := by ext w; simp
88   map_smul' c f := by ext w; simp
89 
90 @[simp] theorem choiceMap_apply (E : W ⊗[ℂ] IntertwiningMap ρ σ →ₗ[ℂ] X)
91     (hE : ∀ (n : N) (w : W) (f : IntertwiningMap ρ σ),
92       E ((ρ n w) ⊗ₜ[ℂ] f) = σ n (E (w ⊗ₜ[ℂ] f)))
93     (f : IntertwiningMap ρ σ) (w : W) : choiceMap ρ σ E hE f w = E (w ⊗ₜ[ℂ] f) := rfl
94 
95 /-- An equivariant evaluation isomorphism induces an injective change on multiplicity. -/
96 theorem choiceMap_injective (E : W ⊗[ℂ] IntertwiningMap ρ σ ≃ₗ[ℂ] X)
97     (hE : ∀ (n : N) (w : W) (f : IntertwiningMap ρ σ),
98       E ((ρ n w) ⊗ₜ[ℂ] f) = σ n (E (w ⊗ₜ[ℂ] f))) :
99     Function.Injective (choiceMap ρ σ E.toLinearMap hE) := by
100   intro f g hfg
101   ext w
102   have ht : E (w ⊗ₜ[ℂ] f) = E (w ⊗ₜ[ℂ] g) :=
103     congrArg (fun q : IntertwiningMap ρ σ => q w) hfg
104   exact congrArg (map ρ σ) (E.injective ht)
105 
106 /-- The actual linear change of multiplicity induced by an arbitrary evaluation choice. -/
107 def choiceEquiv [FiniteDimensional ℂ W] [FiniteDimensional ℂ X]
108     (E : W ⊗[ℂ] IntertwiningMap ρ σ ≃ₗ[ℂ] X)
109     (hE : ∀ (n : N) (w : W) (f : IntertwiningMap ρ σ),
110       E ((ρ n w) ⊗ₜ[ℂ] f) = σ n (E (w ⊗ₜ[ℂ] f))) :
111     IntertwiningMap ρ σ ≃ₗ[ℂ] IntertwiningMap ρ σ :=
112   LinearEquiv.ofBijective (choiceMap ρ σ E.toLinearMap hE)
113     ⟨choiceMap_injective ρ σ E hE, LinearMap.injective_iff_surjective.mp
114       (choiceMap_injective ρ σ E hE)⟩
115 
116 @[simp] theorem choiceEquiv_apply [FiniteDimensional ℂ W] [FiniteDimensional ℂ X]
117     (E : W ⊗[ℂ] IntertwiningMap ρ σ ≃ₗ[ℂ] X)
118     (hE : ∀ (n : N) (w : W) (f : IntertwiningMap ρ σ),
119       E ((ρ n w) ⊗ₜ[ℂ] f) = σ n (E (w ⊗ₜ[ℂ] f)))
120     (f : IntertwiningMap ρ σ) (w : W) : choiceEquiv ρ σ E hE f w = E (w ⊗ₜ[ℂ] f) := rfl
121 
122 /-- Every equivariant evaluation choice factors uniquely through a multiplicity automorphism. -/
123 theorem exists_unique_choice [FiniteDimensional ℂ W] [FiniteDimensional ℂ X]
124     (E : W ⊗[ℂ] IntertwiningMap ρ σ ≃ₗ[ℂ] X)
125     (hE : ∀ (n : N) (w : W) (f : IntertwiningMap ρ σ),
126       E ((ρ n w) ⊗ₜ[ℂ] f) = σ n (E (w ⊗ₜ[ℂ] f))) :
127     ∃! L : IntertwiningMap ρ σ ≃ₗ[ℂ] IntertwiningMap ρ σ,
128       ∀ t : W ⊗[ℂ] IntertwiningMap ρ σ,
129         E t = map ρ σ (TensorProduct.map LinearMap.id L.toLinearMap t) := by
130   refine ⟨choiceEquiv ρ σ E hE, ?_, ?_⟩
131   · intro t
132     induction t using TensorProduct.induction_on with
133     | zero => simp
134     | add u v hu hv => simp [hu, hv]
135     | tmul w f => rfl
136   · intro L hL
137     ext f w
138     exact (hL (w ⊗ₜ[ℂ] f)).symm
139 
140 section Operators
141 variable {G : Type*} [Group G] (N : Subgroup G) [N.Normal]
142   (π : Representation ℂ G X) (ρ : Representation ℂ N W)
143   (g : G) (I : Representation.Equiv ρ (CliffordDatum.conjugate N ρ g))
144 
145 /-- The constructed multiplicity operator has the required literal tensor action. -/
146 theorem map_operator (t : W ⊗[ℂ] CliffordMultiplicity.Space N ρ π) :
147     map ρ (CliffordDatum.restriction N π)
148       (TensorProduct.map I.toLinearMap (CliffordMultiplicity.operator N ρ π g I).toLinearMap t) =
149         π g (map ρ (CliffordDatum.restriction N π) t) := by
150   induction t using TensorProduct.induction_on with
151   | zero => simp
152   | add u v hu hv => simp [hu, hv]
153   | tmul w f => simp [map_tmul, CliffordMultiplicity.operator_apply]
154 
155 /-- Tensor evaluation determines the actual multiplicity operator uniquely. -/
156 theorem operator_unique (T : CliffordMultiplicity.Space N ρ π →ₗ[ℂ]
157     CliffordMultiplicity.Space N ρ π)
158     (hT : ∀ (w : W) (f : CliffordMultiplicity.Space N ρ π),
159       map ρ (CliffordDatum.restriction N π) ((I w) ⊗ₜ[ℂ] T f) =
160         π g (map ρ (CliffordDatum.restriction N π) (w ⊗ₜ[ℂ] f))) :
161     T = (CliffordMultiplicity.operator N ρ π g I).toLinearMap := by
162   ext f w
163   simpa using hT (I.symm w) f
164 
165 /-- Changing any equivariant isotypic evaluation conjugates the actual action on multiplicity. -/
166 theorem choice_operator_conjugation [FiniteDimensional ℂ W] [FiniteDimensional ℂ X]
167     (E : W ⊗[ℂ] CliffordMultiplicity.Space N ρ π ≃ₗ[ℂ] X)
168     (hE : ∀ (n : N) (w : W) (f : CliffordMultiplicity.Space N ρ π),
169       E ((ρ n w) ⊗ₜ[ℂ] f) = π (n : G) (E (w ⊗ₜ[ℂ] f)))
170     (T : CliffordMultiplicity.Space N ρ π →ₗ[ℂ] CliffordMultiplicity.Space N ρ π)
171     (hT : ∀ (w : W) (f : CliffordMultiplicity.Space N ρ π),
172       E ((I w) ⊗ₜ[ℂ] T f) = π g (E (w ⊗ₜ[ℂ] f)))
173     (f : CliffordMultiplicity.Space N ρ π) :
174     T f = (choiceEquiv ρ (CliffordDatum.restriction N π) E hE).symm
175       (CliffordMultiplicity.operator N ρ π g I
176         (choiceEquiv ρ (CliffordDatum.restriction N π) E hE f)) := by
177   apply (choiceEquiv ρ (CliffordDatum.restriction N π) E hE).injective
178   simp only [LinearEquiv.apply_symm_apply]
179   ext w
180   change E (w ⊗ₜ[ℂ] T f) = π g (E (I.symm w ⊗ₜ[ℂ] f))
181   simpa using hT (I.symm w) f
182 
183 /-- Construct the multiplicity operator for an arbitrary equivariant evaluation choice. -/
184 def choiceOperator [FiniteDimensional ℂ W] [FiniteDimensional ℂ X]
185     (E : W ⊗[ℂ] CliffordMultiplicity.Space N ρ π ≃ₗ[ℂ] X)
186     (hE : ∀ (n : N) (w : W) (f : CliffordMultiplicity.Space N ρ π),
187       E ((ρ n w) ⊗ₜ[ℂ] f) = π (n : G) (E (w ⊗ₜ[ℂ] f))) :
188     CliffordMultiplicity.Space N ρ π ≃ₗ[ℂ] CliffordMultiplicity.Space N ρ π :=
189   ((choiceEquiv ρ (CliffordDatum.restriction N π) E hE).trans
190     (CliffordMultiplicity.operator N ρ π g I)).trans
191       (choiceEquiv ρ (CliffordDatum.restriction N π) E hE).symm
192 
193 /-- The constructed operator satisfies the defining tensor identity for that evaluation. -/
194 theorem choiceOperator_tensor [FiniteDimensional ℂ W] [FiniteDimensional ℂ X]
195     (E : W ⊗[ℂ] CliffordMultiplicity.Space N ρ π ≃ₗ[ℂ] X)
196     (hE : ∀ (n : N) (w : W) (f : CliffordMultiplicity.Space N ρ π),
197       E ((ρ n w) ⊗ₜ[ℂ] f) = π (n : G) (E (w ⊗ₜ[ℂ] f)))
198     (w : W) (f : CliffordMultiplicity.Space N ρ π) :
199     E ((I w) ⊗ₜ[ℂ] choiceOperator N π ρ g I E hE f) = π g (E (w ⊗ₜ[ℂ] f)) := by
200   let L := choiceEquiv ρ (CliffordDatum.restriction N π) E hE
201   change (L (L.symm (CliffordMultiplicity.operator N ρ π g I (L f)))) (I w) =
202     π g ((L f) w)
203   simp
204 
205 /-- Every equivariant evaluation has a unique invertible multiplicity factor. -/
206 theorem exists_unique_choice_operator [FiniteDimensional ℂ W] [FiniteDimensional ℂ X]
207     (E : W ⊗[ℂ] CliffordMultiplicity.Space N ρ π ≃ₗ[ℂ] X)
208     (hE : ∀ (n : N) (w : W) (f : CliffordMultiplicity.Space N ρ π),
209       E ((ρ n w) ⊗ₜ[ℂ] f) = π (n : G) (E (w ⊗ₜ[ℂ] f))) :
210     ∃! T : CliffordMultiplicity.Space N ρ π ≃ₗ[ℂ] CliffordMultiplicity.Space N ρ π,
211       ∀ (w : W) (f : CliffordMultiplicity.Space N ρ π),
212         E ((I w) ⊗ₜ[ℂ] T f) = π g (E (w ⊗ₜ[ℂ] f)) := by
213   refine ⟨choiceOperator N π ρ g I E hE, choiceOperator_tensor N π ρ g I E hE, ?_⟩
214   intro T hT
215   apply LinearEquiv.ext
216   intro f
217   exact choice_operator_conjugation N π ρ g I E hE T.toLinearMap hT f
218 
219 end Operators
220 
221 section Restriction
222 variable {G : Type*} [Group G] [Finite G] (N : Subgroup G)
223   (π : Representation ℂ G X) (ρ : Representation ℂ N W)
224   [IsIrreducible π] [IsIrreducible ρ]
225 
226 /-- The finite Clifford datum supplies every hypothesis of canonical evaluation. -/
227 theorem restriction_bijective
228     (h : IsIsotypicOfType ℂ[N] (Representation.asModule (π.comp N.subtype)) ρ.asModule) :
229     Function.Bijective (map ρ (π.comp N.subtype)) := by
230   let : FiniteDimensional ℂ X := FiniteRepresentation.finiteDimensional π
231   exact bijective ρ (π.comp N.subtype) h
232 
233 /-- The actual finite Clifford multiplicity space is nonzero. -/
234 theorem restriction_multiplicity_nontrivial
235     (h : IsIsotypicOfType ℂ[N] (Representation.asModule (π.comp N.subtype)) ρ.asModule) :
236     Nontrivial (IntertwiningMap ρ (π.comp N.subtype)) := by
237   let : FiniteDimensional ℂ X := FiniteRepresentation.finiteDimensional π
238   let : Nontrivial X := ((RepresentationStability.irreducible_iff π).mp inferInstance).1
239   exact multiplicity_nontrivial ρ (π.comp N.subtype) h
240 
241 end Restriction
242 end PaperXI.CliffordEvaluation

Back to source controls