CompactSmoothSemisimple.lean

1 import PaperXI.SmoothDegreeQuotient
2 import Mathlib.Topology.Algebra.OpenSubgroup
3 import Mathlib.RepresentationTheory.Subrepresentation
4 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
5 import PaperXI.LocallyFiniteSemisimple
6 
7 /-! Smooth representations of compact groups are locally finite dimensional.
8 This uses compactness of the actual group, not finiteness of the ambient group.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.CompactSmoothSemisimple
13 
14 open Representation PaperXI.SmoothDegreeQuotient
15 variable {k G V : Type*} [Field k] [Group G] [AddCommGroup V] [Module k V]
16 variable (ρ : Representation k G V)
17 
18 /-- The orbit map factors through the actual vector stabilizer. -/
19 def orbitQuotient (v : V) : G ⧸ vectorStabilizer ρ v → V :=
20   Quotient.lift (fun g => ρ g v) fun g h hgh => by
21     have hh : ρ (g⁻¹ * h) v = v := QuotientGroup.leftRel_apply.mp hgh
22     calc
23       ρ g v = ρ g (ρ (g⁻¹ * h) v) := congrArg (ρ g) hh.symm
24       _ = ρ h v := by rw [← Module.End.mul_apply, ← map_mul, mul_inv_cancel_left]
25 
26 /-- The subrepresentation generated by one vector. -/
27 def orbitSpan (v : V) : Subrepresentation ρ where
28   toSubmodule := Submodule.span k (Set.range fun g => ρ g v)
29   apply_mem_toSubmodule g := by
30     intro w hw
31     induction hw using Submodule.span_induction with
32     | mem w hw =>
33       obtain ⟨h, rfl⟩ := hw
34       apply Submodule.subset_span
35       exact ⟨g * h, by simp only [map_mul, Module.End.mul_apply]⟩
36     | zero => simp
37     | add a b _ _ ha hb => simpa only [map_add] using Submodule.add_mem _ ha hb
38     | smul a w _ hw => simpa only [map_smul] using Submodule.smul_mem _ a hw
39 
40 theorem mem_orbitSpan (v : V) : v ∈ orbitSpan ρ v := by
41   apply Submodule.subset_span
42   exact ⟨1, by simp⟩
43 
44 variable [TopologicalSpace G] [IsTopologicalGroup G]
45 
46 omit [IsTopologicalGroup G] in
47 /-- Smoothness passes to every subrepresentation. -/
48 theorem subrepresentation_smooth (hρ : IsSmooth ρ) (S : Subrepresentation ρ) :
49     IsSmooth S.toRepresentation := by
50   intro v
51   have he : (vectorStabilizer S.toRepresentation v : Set G) =
52       (vectorStabilizer ρ (v : V) : Set G) := by
53     ext g
54     exact Subtype.ext_iff
55   rw [he]
56   exact hρ v
57 
58 variable [CompactSpace G]
59 
60 /-- Every smooth orbit under a compact group is finite. -/
61 theorem orbit_finite (hρ : IsSmooth ρ) (v : V) :
62     Set.Finite (Set.range fun g => ρ g v) := by
63   let : Finite (G ⧸ vectorStabilizer ρ v) :=
64     Subgroup.quotient_finite_of_isOpen _ (hρ v)
65   apply (Set.finite_range (orbitQuotient ρ v)).subset
66   rintro w ⟨g, rfl⟩
67   exact ⟨QuotientGroup.mk g, rfl⟩
68 
69 /-- Thus each actual orbit-generated subrepresentation is finite dimensional. -/
70 theorem orbitSpan_finiteDimensional (hρ : IsSmooth ρ) (v : V) :
71     FiniteDimensional k (orbitSpan ρ v).toSubmodule :=
72   FiniteDimensional.span_of_finite k (orbit_finite ρ hρ v)
73 
74 /-- A finite-dimensional smooth piece factors through a finite quotient group. -/
75 theorem subrepresentation_kernel_quotient_finite (hρ : IsSmooth ρ)
76     (S : Subrepresentation ρ) [FiniteDimensional k S.toSubmodule] :
77     Finite (G ⧸ S.toRepresentation.ker) :=
78   Subgroup.quotient_finite_of_isOpen _
79     (isOpen_kernel_of_smooth S.toRepresentation (subrepresentation_smooth ρ hρ S))
80 
81 /-- Every smooth representation of an actual compact group in characteristic
82 zero is semisimple, including infinite-dimensional smooth representations. -/
83 theorem smooth_semisimple [CharZero k] (hρ : IsSmooth ρ) :
84     IsSemisimpleRepresentation ρ := by
85   apply LocallyFiniteSemisimple.semisimple_of_locally_finite_quotient ρ
86   intro v
87   let S := orbitSpan ρ v
88   let : FiniteDimensional k S.toSubmodule := orbitSpan_finiteDimensional ρ hρ v
89   exact ⟨S, mem_orbitSpan ρ v, S.toRepresentation.ker, inferInstance,
90     subrepresentation_kernel_quotient_finite ρ hρ S, le_rfl⟩
91 
92 end PaperXI.CompactSmoothSemisimple

Back to source controls