Groups with one irreducible representation in each dimension

DefinitionIrreducible representations into \(\mathrm{GL}_n(\mathbb{C})\)#✓fully proved

Let \(G\) be a group and \(\rho \colon G \to \mathrm{GL}_n(\mathbb{C})\) a homomorphism. Then \(\rho\) is irreducible when \(n \ge 1\) and the only subspaces \(W\) of \(\mathbb{C}^n\) with \(\rho(g)v \in W\) for all \(g \in G\) and \(v \in W\) are \(0\) and \(\mathbb{C}^n\).

def IsIrreducibleRep {G : Type*} [Group G] {n : ℕ}
    (ρ : G →* Matrix.GeneralLinearGroup (Fin n) ℂ) : Prop :=
  0 < n ∧ ∀ W : Submodule ℂ (Fin n → ℂ),
    (∀ g : G, ∀ v ∈ W, (ρ g : Matrix (Fin n) (Fin n) ℂ).mulVec v ∈ W) → W = ⊥ ∨ W = ⊤
Used by 1

DefinitionEquivalent representations into \(\mathrm{GL}_n(\mathbb{C})\)#✓fully proved

Let \(G\) be a group. Two homomorphisms \(\rho, \sigma \colon G \to \mathrm{GL}_n(\mathbb{C})\) are equivalent when there is a matrix \(P \in \mathrm{GL}_n(\mathbb{C})\) with \(\sigma(g) = P \rho(g) P^{-1}\) for all \(g \in G\).

def IsEquivalentRep {G : Type*} [Group G] {n : ℕ}
    (ρ σ : G →* Matrix.GeneralLinearGroup (Fin n) ℂ) : Prop :=
  ∃ P : Matrix.GeneralLinearGroup (Fin n) ℂ, ∀ g : G, σ g = P * ρ g * P⁻¹
Used by 1

DefinitionGroups with exactly one irreducible representation of each dimension#✓fully proved

A group \(G\) has exactly one irreducible complex representation of each dimension when for every \(n \ge 1\) there is an irreducible homomorphism \(G \to \mathrm{GL}_n(\mathbb{C})\) and any two irreducible homomorphisms \(G \to \mathrm{GL}_n(\mathbb{C})\) are equivalent. Representations are arbitrary homomorphisms of the abstract group \(G\); no continuity is required.

def HasUniqueIrreducibleRepOfEachDim (G : Type*) [Group G] : Prop :=
  ∀ n : ℕ, 0 < n →
    (∃ ρ : G →* Matrix.GeneralLinearGroup (Fin n) ℂ, IsIrreducibleRep ρ) ∧
    ∀ ρ σ : G →* Matrix.GeneralLinearGroup (Fin n) ℂ,
      IsIrreducibleRep ρ → IsIrreducibleRep σ → IsEquivalentRep ρ σ
Uses 2 · Used by 1

DefinitionMcKay's question on \(\mathrm{SU}_2(\mathbb{C})\) (Kourovka 16.58)#✓fully proved

A group \(G\) has exactly one irreducible complex representation of each dimension \(n = 1, 2, \dots\), up to equivalence, if and only if \(G\) is isomorphic to \(\mathrm{SU}_2(\mathbb{C})\). Here a representation of dimension \(n\) is any homomorphism \(G \to \mathrm{GL}_n(\mathbb{C})\) of abstract groups, with no continuity required.

def su2OnlyGroupWithUniqueIrreducibleReps : Prop :=
  ∀ (G : Type) [Group G],
    HasUniqueIrreducibleRepOfEachDim G ↔ Nonempty (G ≃* Matrix.specialUnitaryGroup (Fin 2) ℂ)
Uses 1 · Used by 1

TheoremMcKay's question 16.58 has a negative answer#●ready to prove

It is not the case that a group has exactly one irreducible complex representation of each dimension \(n \ge 1\), up to equivalence, if and only if it is isomorphic to \(\mathrm{SU}_2(\mathbb{C})\). Here a representation of dimension \(n\) is any homomorphism to \(\mathrm{GL}_n(\mathbb{C})\) of abstract groups, with no continuity required.

Applying a field automorphism \(\varphi\) of \(\mathbb{C}\) to matrix entries gives irreducible \(2\)-dimensional representations \(x \mapsto x^\varphi\) of the abstract group \(\mathrm{SU}_2(\mathbb{C})\), infinitely many of them pairwise non-equivalent (von Neumann), so \(\mathrm{SU}_2(\mathbb{C})\) itself lacks the property. It does have it if only unitary representations are counted, as these are continuous (Cartan).

public theorem_wanted su2OnlyGroupWithUniqueIrreducibleReps_refuted :
    ¬ su2OnlyGroupWithUniqueIrreducibleReps
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 16.58 (J. McKay); resolution: V. P. Burichenko, letter of 16 July 2013, as recorded in the Kourovka Archive (observation of J. von Neumann), Kourovka Archive, Problem 16.58 (No: for field automorphisms φ of ℂ the representations x ↦ x^φ of SU₂(ℂ) are irreducible and infinitely many are pairwise non-equivalent, so SU₂(ℂ) itself lacks the property; it has it for unitary representations, which are continuous by É. Cartan).
Uses 1
4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.