Complete reducibility for compact groups

compact_group_semisimple

Submitter: Kim Morrison.

Notes: A continuous representation of a compact topological group on a finite-dimensional real vector space is semisimple: every subrepresentation has a G-invariant complement (Representation.IsSemisimpleRepresentation). Mathlib has the semisimplicity predicate and Maschke's theorem for finite groups but no compact-group / Peter–Weyl / unitarian-trick result. Continuity of the action G × V → V and finite dimensionality are essential hypotheses. Candidate from §21 of the Knill survey.

Source: H. Weyl, *Theorie der Darstellung kontinuierlicher halb-einfacher Gruppen durch lineare Transformationen* (1925–26); Peter–Weyl (1927). Knill, *Some fundamental theorems in mathematics*, §21.

Informal solution: Apply the unitarian trick. Start from any inner product ⟨·,·⟩₀ on V and average it over the group using normalized Haar measure: ⟨u,v⟩ = ∫_G ⟨ρ(g) u, ρ(g) v⟩₀ dg. Compactness gives a finite total Haar measure and joint continuity makes the integrand continuous, so the integral exists; the result is a positive-definite G-invariant inner product, i.e. ρ acts by isometries. For any subrepresentation W, its orthogonal complement W^⊥ with respect to this invariant inner product is again G-invariant and is a complement of W. Hence every subrepresentation is complemented, which is exactly IsSemisimpleRepresentation.

theorem declaration uses `sorry`compact_group_semisimple {G V : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
    (ρ : Representation ℝ G V)
    (hρ : Continuous fun p : G × V => ρ p.1 p.2) :
    ρ.IsSemisimpleRepresentation := byG:Type u_1V:Type u_2inst✝⁶:Group Ginst✝⁵:TopologicalSpace Ginst✝⁴:IsTopologicalGroup Ginst✝³:CompactSpace Ginst✝²:NormedAddCommGroup Vinst✝¹:NormedSpace ℝ Vinst✝:FiniteDimensional ℝ Vρ:Representation ℝ G Vhρ:Continuous fun p => (ρ p.1) p.2⊢ ρ.IsSemisimpleRepresentation
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 21, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 21, 2026

• @lukerj00 with Tau (caj.al) on Jun 24, 2026