LocallyFiniteSemisimple.lean

1 import Mathlib.RepresentationTheory.Maschke
2 import PaperXI.QuotientRepresentation
3 
4 /-! Semisimplicity from finite quotient actions on local invariant subspaces.
5 The representation may have arbitrary dimension; the local pieces supply the
6 semisimple submodules whose supremum is the whole group-algebra module. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 namespace PaperXI.LocallyFiniteSemisimple
12 
13 open Representation
14 open scoped MonoidAlgebra
15 
16 section LocalModules
17 
18 variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
19 
20 /-- A module covered by semisimple submodules is semisimple. -/
21 theorem module_of_locally_semisimple
22     (h : ∀ x : M, ∃ S : Submodule R M, x ∈ S ∧ IsSemisimpleModule R S) :
23     IsSemisimpleModule R M := by
24   classical
25   choose S hx hS using h
26   apply isSemisimpleModule_of_isSemisimpleModule_submodule' hS
27   apply top_unique
28   intro x _
29   exact (le_iSup S x) (hx x)
30 
31 end LocalModules
32 
33 section Representations
34 
35 variable {k G Q V W : Type*} [Field k] [Group G] [Group Q]
36   [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
37 
38 /-- Surjective pullback preserves semisimplicity. -/
39 theorem semisimple_comp_iff (q : G →* Q) (hq : Function.Surjective q)
40     (σ : Representation k Q V) :
41     IsSemisimpleRepresentation (σ.comp q) ↔ IsSemisimpleRepresentation σ :=
42   (QuotientRepresentation.subrepresentationEquiv q hq σ).complementedLattice_iff
43 
44 /-- An action factoring through a finite group is semisimple in characteristic zero. -/
45 theorem semisimple_finite_pullback [CharZero k] [Finite Q]
46     (q : G →* Q) (hq : Function.Surjective q) (σ : Representation k Q V) :
47     IsSemisimpleRepresentation (σ.comp q) := by
48   have : NeZero (Nat.card Q : k) := ⟨by exact_mod_cast (Nat.card_pos (α := Q)).ne'⟩
49   exact (semisimple_comp_iff q hq σ).mpr inferInstance
50 
51 /-- A finite quotient by an actual subgroup of the kernel gives semisimplicity. -/
52 theorem semisimple_of_finite_quotient [CharZero k]
53     (τ : Representation k G V) (N : Subgroup G) [N.Normal] [Finite (G ⧸ N)]
54     (hN : N ≤ τ.ker) : IsSemisimpleRepresentation τ :=
55   semisimple_finite_pullback (QuotientGroup.mk' N) QuotientGroup.mk_surjective
56     (QuotientRepresentation.descend N τ hN)
57 
58 /-- A semisimple invariant subspace gives a semisimple group-algebra submodule. -/
59 theorem semisimple_asSubmodule (τ : Representation k G W) (S : Subrepresentation τ)
60     [IsSemisimpleRepresentation S.toRepresentation] :
61     IsSemisimpleModule k[G] S.asSubmodule := by
62   let : IsSemisimpleModule k[G] S.toRepresentation.asModule :=
63     (isSemisimpleRepresentation_iff_isSemisimpleModule_asModule S.toRepresentation).mp
64       inferInstance
65   let incl : IntertwiningMap S.toRepresentation τ :=
66     { toLinearMap := S.toSubmodule.subtype
67       isIntertwining' := by intro g; ext v; rfl }
68   let j := IntertwiningMap.equivLinearMapAsModule S.toRepresentation τ incl
69   have hj : LinearMap.range j = S.asSubmodule := by
70     ext x
71     constructor
72     · rintro ⟨y, rfl⟩
73       exact y.property
74     · intro hx
75       exact ⟨⟨x, hx⟩, rfl⟩
76   rw [← hj]
77   exact IsSemisimpleModule.range j
78 
79 /-- An arbitrary-dimensional representation is semisimple if each vector belongs
80 to a semisimple invariant subspace. -/
81 theorem semisimple_of_locally_semisimple (τ : Representation k G W)
82     (h : ∀ w : W, ∃ S : Subrepresentation τ,
83       w ∈ S ∧ IsSemisimpleRepresentation S.toRepresentation) :
84     IsSemisimpleRepresentation τ := by
85   apply (isSemisimpleRepresentation_iff_isSemisimpleModule_asModule τ).mpr
86   apply module_of_locally_semisimple
87   intro w
88   obtain ⟨S, hw, hS⟩ := h w
89   let : IsSemisimpleRepresentation S.toRepresentation := hS
90   exact ⟨S.asSubmodule, hw, semisimple_asSubmodule τ S⟩
91 
92 /-- Local finite quotient actions imply semisimplicity, without a global finite
93 quotient or a finite-dimensionality hypothesis. -/
94 theorem semisimple_of_locally_finite_quotient [CharZero k]
95     (τ : Representation k G W)
96     (h : ∀ w : W, ∃ S : Subrepresentation τ, w ∈ S ∧
97       ∃ N : Subgroup G, N.Normal ∧ Finite (G ⧸ N) ∧ N ≤ S.toRepresentation.ker) :
98     IsSemisimpleRepresentation τ := by
99   apply semisimple_of_locally_semisimple τ
100   intro w
101   obtain ⟨S, hw, N, hN, hfin, hker⟩ := h w
102   let : N.Normal := hN
103   let : Finite (G ⧸ N) := hfin
104   exact ⟨S, hw, semisimple_of_finite_quotient S.toRepresentation N hker⟩
105 
106 end Representations
107 
108 end PaperXI.LocallyFiniteSemisimple

Back to source controls