Complete reducibility for compact groups

A finite-dimensional representation of a compact group over ℝ or ℂ whose matrix coefficients are continuous is semisimple: every subrepresentation has an invariant complement. This is Maschke's theorem with Haar averaging in place of the average over a finite group.

The statement is about a plain Representation on a vector space without any chosen topology or inner product, so that it applies to representations built algebraically, such as the restriction of a rational representation of GL n ℂ to the unitary group. The continuity hypothesis is stated through linear functionals: g ↦ f (ρ g v) is continuous for every vector v and every linear functional f.

The proof transports the representation, along a basis, to a continuous representation on the Euclidean space EuclideanSpace 𝕜 (Fin d). The unitarian trick (ContRepresentation.exists_isUnitary_congr) conjugates that one into a unitary representation, in which the orthogonal complement of a subrepresentation is invariant (ContRepresentation.IsUnitary.isCompl_orthogonalSubrepresentation); pulling that complement back along the composite equivalence gives the complement in the original representation.

Main results

• Representation.isSemisimpleRepresentation_of_continuous: a finite-dimensional representation of a compact group with continuous matrix coefficients is semisimple.

References

• D. Bump, Lie Groups, second edition, Springer GTM 225 (2013), Chapter 2, Proposition 2.1.

theorem Representation.isSemisimpleRepresentation_of_continuous {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [AddCommGroup V] [Module 𝕜 V] [FiniteDimensional 𝕜 V] (ρ : Representation 𝕜 G V) (hρ : ∀ (f : Module.Dual 𝕜 V) (v : V), Continuous fun (g : G) => f ((ρ g) v)) : ρ.IsSemisimpleRepresentation

Complete reducibility for compact groups. A finite-dimensional representation of a compact group whose matrix coefficients g ↦ f (ρ g v) are continuous is semisimple: every subrepresentation has an invariant complement.