Representations of finite groups

Ordinary representation theory of finite groups over algebraically closed fields of characteristic zero: characters, irreducibility, Schur's lemma, multiplicities and the Wedderburn decomposition of the group algebra.

• Characters of representations
• Representations of finite abelian groups
• Schur's lemma and multiplicities
• Wedderburn decomposition of the group algebra

TheoremDimension of an irreducible representation divides the group order#✓fully proved

If ρ is an irreducible representation of a finite group G over an algebraically closed field k of characteristic zero, then dim_k ρ ∣ |G|. In particular, over ℂ, every irreducible degree divides the order of the group.

theorem irred_dim_dvd_card
    {G : Type u} [Group G] [Fintype G] {k : Type u} [Field k] [IsAlgClosed k]
    [CharZero k]
    {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V]
    (ρ : Representation k G V) [ρ.IsIrreducible] :
    Module.finrank k V ∣ Fintype.card G

TheoremMaschke's theorem#✓fully proved

Every finite-dimensional complex representation \(\sigma\) of a finite group is equivalent to the direct sum of a finite family of irreducible subrepresentations of \(\sigma\).

theorem maschke_decomposition {G : Type v} [Group G] [Fintype G]
    {W : Type u} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
    (σ : Representation ℂ G W) :
    ∃ (ι : Type u) (_ : Fintype ι) (_ : DecidableEq ι) (T : ι → Subrepresentation σ),
      (∀ i, (T i).toRepresentation.IsIrreducible) ∧
      Nonempty (Representation.Equiv σ
        (Representation.directSum (fun i => (T i).toRepresentation)))

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.