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 ρ σ
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 = ⊤
WantedExt/GroupTheory/UniqueIrreducibleRepresentationsSU2Kourovka16Problem58Wanted.lean:41
def IsEquivalentRep {G : Type*} [Group G] {n : ℕ}
(ρ σ : G →* Matrix.GeneralLinearGroup (Fin n) ℂ) : Prop :=
∃ P : Matrix.GeneralLinearGroup (Fin n) ℂ, ∀ g : G, σ g = P * ρ g * P⁻¹
WantedExt/GroupTheory/UniqueIrreducibleRepresentationsSU2Kourovka16Problem58Wanted.lean:47
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) ℂ)
def HasUniqueIrreducibleRepOfEachDim (G : Type*) [Group G] : Prop :=
∀ n : ℕ, 0 < n →
(∃ ρ : G →* Matrix.GeneralLinearGroup (Fin n) ℂ, IsIrreducibleRep ρ) ∧
∀ ρ σ : G →* Matrix.GeneralLinearGroup (Fin n) ℂ,
IsIrreducibleRep ρ → IsIrreducibleRep σ → IsEquivalentRep ρ σ
WantedExt/GroupTheory/UniqueIrreducibleRepresentationsSU2Kourovka16Problem58Wanted.lean:53
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
def su2OnlyGroupWithUniqueIrreducibleReps : Prop :=
∀ (G : Type) [Group G],
HasUniqueIrreducibleRepOfEachDim G ↔ Nonempty (G ≃* Matrix.specialUnitaryGroup (Fin 2) ℂ)
WantedExt/GroupTheory/UniqueIrreducibleRepresentationsSU2Kourovka16Problem58Wanted.lean:61
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.