GallagherTensorIrreducibility58.lean

1 import PaperXI.SchurScalar
2 import PaperXI.RepresentationStability
3 import Mathlib.LinearAlgebra.TensorProduct.Map
4 import Mathlib.LinearAlgebra.TensorProduct.Basis
5 
6 /-!
7 # Reverse Clifford tensor irreducibility
8 
9 The prescribed extension factor is tensored with an irreducible quotient
10 representation. The resulting action is irreducible; no irreducibility of the
11 tensor product is assumed. The argument uses Jacobson density on the actual
12 normal-subgroup action.
13 -/
14 set_option autoImplicit false
15 noncomputable section
16 namespace PaperXI.GallagherTensorIrreducibility58
17 
18 open Representation
19 open scoped TensorProduct MonoidAlgebra
20 
21 variable {G W : Type*} [Group G] [AddCommGroup W] [Module ℂ W]
22 variable [FiniteDimensional ℂ W]
23 
24 /-- An actual finite-dimensional complex irreducible action spans all operators. -/
25 theorem algebraAction_surjective (ρ : Representation ℂ G W) [IsIrreducible ρ] :
26     Function.Surjective ρ.asAlgebraHom := by
27   classical
28   intro F
29   let M := ρ.asModule
30   let E := ρ.asModuleEquiv
31   let T : M →ₗ[ℂ] M := E.symm.toLinearMap.comp (F.comp E.toLinearMap)
32   let T' : Module.End (Module.End ℂ[G] M) M :=
33     { toFun := T
34       map_add' := T.map_add
35       map_smul' := by
36         intro a x
37         obtain ⟨c, rfl⟩ :=
38           (IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed
39             (A := ℂ[G]) (V := M) ℂ).surjective a
40         exact T.map_smul c x }
41   let b := Module.finBasis ℂ M
42   obtain ⟨r, hr⟩ := jacobson_density T' (Finset.univ.image b)
43   refine ⟨r, ?_⟩
44   have he : T = (E.symm.toLinearMap.comp ((ρ.asAlgebraHom r).comp E.toLinearMap)) := by
45     apply b.ext
46     intro i
47     have h := hr (b i) (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩)
48     exact h
49   ext w
50   have h := LinearMap.congr_fun he (E.symm w)
51   have hh := congrArg E h
52   simpa [T] using hh.symm
53 
54 variable {U Q : Type*} [AddCommGroup U] [Module ℂ U] [Group Q]
55 
56 omit [FiniteDimensional ℂ W] in
57 /-- Stability under the first-factor group action implies stability under its
58 actual group-algebra action. -/
59 theorem stable_tensor_algebra (ρ : Representation ℂ G W)
60     (S : Submodule ℂ (W ⊗[ℂ] U))
61     (hS : ∀ g x, x ∈ S → TensorProduct.map (ρ g) LinearMap.id x ∈ S)
62     (r : ℂ[G]) (x : W ⊗[ℂ] U) (hx : x ∈ S) :
63     TensorProduct.map (ρ.asAlgebraHom r) LinearMap.id x ∈ S := by
64   induction r using MonoidAlgebra.induction_on with
65   | of g => simpa using hS g x hx
66   | add a b ha hb =>
67     simpa only [map_add, TensorProduct.map_add_left, LinearMap.add_apply] using S.add_mem ha hb
68   | smul c a ha =>
69     simpa only [map_smul, TensorProduct.map_smul_left, LinearMap.smul_apply] using S.smul_mem c ha
70 
71 /-- On an irreducible finite-dimensional first factor, every operator on that
72 factor preserves any subspace stable under the group action. -/
73 theorem stable_tensor_end (ρ : Representation ℂ G W) [IsIrreducible ρ]
74     (S : Submodule ℂ (W ⊗[ℂ] U))
75     (hS : ∀ g x, x ∈ S → TensorProduct.map (ρ g) LinearMap.id x ∈ S)
76     (F : Module.End ℂ W) (x : W ⊗[ℂ] U) (hx : x ∈ S) :
77     TensorProduct.map F LinearMap.id x ∈ S := by
78   obtain ⟨r, rfl⟩ := algebraAction_surjective ρ F
79   exact stable_tensor_algebra ρ S hS r x hx
80 
81 omit [FiniteDimensional ℂ W] in
82 /-- A basis coefficient is extracted by an actual first-factor rank-one operator. -/
83 theorem map_rankOne {ι : Type*} [DecidableEq ι] (b : Module.Basis ι ℂ W)
84     (i : ι) (w : W) (x : W ⊗[ℂ] U) :
85     TensorProduct.map ((b.coord i).smulRight w) LinearMap.id x =
86       w ⊗ₜ[ℂ] (TensorProduct.equivFinsuppOfBasisLeft b x i) := by
87   induction x using TensorProduct.induction_on with
88   | zero => simp
89   | add x y hx hy => simp [hx, hy, TensorProduct.tmul_add]
90   | tmul v u =>
91     simp [TensorProduct.smul_tmul]
92 
93 omit [FiniteDimensional ℂ W] in
94 /-- The literal multiplicity subspace belonging to a tensor subspace. -/
95 def multiplicitySubspace (S : Submodule ℂ (W ⊗[ℂ] U)) : Submodule ℂ U where
96   carrier := {u | ∀ w : W, w ⊗ₜ[ℂ] u ∈ S}
97   zero_mem' := by intro w; simp
98   add_mem' := by intro u v hu hv w; simpa [TensorProduct.tmul_add] using S.add_mem (hu w) (hv w)
99   smul_mem' := by intro c u hu w; simpa [TensorProduct.tmul_smul] using S.smul_mem c (hu w)
100 
101 /-- Reverse Clifford/Gallagher irreducibility on the actual tensor space.
102 The second factor is trivial on N and irreducible on its surjective quotient;
103 only the restriction of the prescribed first factor to N must be irreducible. -/
104 theorem tensor_irreducible (N : Subgroup G) (q : G →* Q)
105     (hq : Function.Surjective q) (hN : N ≤ q.ker)
106     (κ : Representation ℂ G W) (σ : Representation ℂ Q U)
107     [IsIrreducible (κ.comp N.subtype)] [IsIrreducible σ] :
108     IsIrreducible (κ.tprod (σ.comp q)) := by
109   classical
110   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space (κ.comp N.subtype)
111   let : Nontrivial U := GeneratedIrreducibility.nontrivial_space σ
112   let b := Module.finBasis ℂ W
113   let : Nonempty (Fin (Module.finrank ℂ W)) := b.index_nonempty
114   let : Nontrivial (W ⊗[ℂ] U) :=
115     (TensorProduct.equivFinsuppOfBasisLeft b).symm.injective.nontrivial
116   apply RepresentationStability.irreducible_of_stable
117   intro S hS
118   have hSN : ∀ n : N, ∀ x, x ∈ S →
119       TensorProduct.map ((κ.comp N.subtype) n) LinearMap.id x ∈ S := by
120     intro n x hx
121     have hn : q n = 1 := hN n.property
122     have h := hS n x hx
123     change TensorProduct.map (κ n) (σ (q n)) x ∈ S at h
124     rw [hn, map_one] at h
125     exact h
126   have hL : RepresentationStability.Stable σ (multiplicitySubspace S) := by
127     intro a u hu w
128     obtain ⟨g, rfl⟩ := hq a
129     have h := hS g (κ g⁻¹ w ⊗ₜ[ℂ] u) (hu (κ g⁻¹ w))
130     simpa [Representation.tprod_apply] using h
131   rcases RepresentationStability.eq_bot_or_top σ (multiplicitySubspace S) hL with hb | ht
132   · left
133     apply le_antisymm _ bot_le
134     intro x hx
135     have hc (i : Fin (Module.finrank ℂ W)) :
136         TensorProduct.equivFinsuppOfBasisLeft b x i ∈ multiplicitySubspace S := by
137       intro w
138       rw [← map_rankOne b i w x]
139       exact stable_tensor_end (κ.comp N.subtype) S hSN _ x hx
140     have hz : TensorProduct.equivFinsuppOfBasisLeft b x = 0 := by
141       ext i
142       have h := hc i
143       rw [hb] at h
144       exact h
145     exact (TensorProduct.equivFinsuppOfBasisLeft b).injective (hz.trans (map_zero _).symm)
146   · right
147     apply top_unique
148     intro x htop
149     clear htop
150     induction x using TensorProduct.induction_on with
151     | zero => exact S.zero_mem
152     | add x y hx hy => exact S.add_mem hx hy
153     | tmul w u =>
154       have hu : u ∈ multiplicitySubspace S := ht ▸ Submodule.mem_top
155       exact hu w
156 
157 /-- The exact normal-subgroup quotient specialization used in compact types. -/
158 theorem quotient_tensor_irreducible (N : Subgroup G) [N.Normal]
159     (κ : Representation ℂ G W) (σ : Representation ℂ (G ⧸ N) U)
160     [IsIrreducible (κ.comp N.subtype)] [IsIrreducible σ] :
161     IsIrreducible (κ.tprod (σ.comp (QuotientGroup.mk' N))) :=
162   tensor_irreducible N (QuotientGroup.mk' N) QuotientGroup.mk_surjective
163     (by intro n hn; exact (QuotientGroup.eq_one_iff n).mpr hn) κ σ
164 
165 end PaperXI.GallagherTensorIrreducibility58

Back to source controls