Character degrees of symmetric groups
DefinitionIrreducible complex matrix representations (Kourovka 16.67)#✓fully proved
Let \(G\) be a group and \(n\) a natural number. A homomorphism \(\rho \colon G \to \mathrm{GL}_n(\mathbb{C})\) is irreducible when \(n \ge 1\) and every subspace \(W\) of \(\mathbb{C}^n\) such that \(\rho(g) v \in W\) for all \(g \in G\) and all \(v \in W\) is either \(0\) or \(\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 complex matrix representations (Kourovka 16.67)#✓fully proved
Let \(G\) be a group and \(n\) a natural number. Two homomorphisms \(\rho, \sigma \colon G \to \mathrm{GL}_n(\mathbb{C})\) are equivalent when there is a single invertible matrix \(P \in \mathrm{GL}_n(\mathbb{C})\) with \(\sigma(g) = P \rho(g) P^{-1}\) for every \(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
DefinitionMoretó's conjecture on equal character degrees of symmetric groups#✓fully proved
For every natural number \(k\) there is a natural number \(n_0\) such that for every \(n \ge n_0\) there are a natural number \(d\) and irreducible representations \(\rho_1, \dots, \rho_k\) of the symmetric group \(S_n\) into \(\mathrm{GL}_d(\mathbb{C})\) that are pairwise inequivalent: \(\rho_i\) and \(\rho_j\) are not equivalent whenever \(i \ne j\).
Since irreducible complex characters correspond to equivalence classes of irreducible complex representations and the degree of a character is the dimension, this says that \(S_n\) has at least \(k\) distinct irreducible complex characters of the same degree.
def symmetricGroupManyCharactersOfEqualDegree : Prop :=
∀ k : ℕ, ∃ n₀ : ℕ, ∀ n ≥ n₀, ∃ (d : ℕ)
(ρ : Fin k → (Equiv.Perm (Fin n) →* Matrix.GeneralLinearGroup (Fin d) ℂ)),
(∀ i, IsIrreducibleRep (ρ i)) ∧ ∀ i j, i ≠ j → ¬ IsEquivalentRep (ρ i) (ρ j)
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/SymmetricGroupEqualCharacterDegreesKourovka16Problem67Wanted.lean:40
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/SymmetricGroupEqualCharacterDegreesKourovka16Problem67Wanted.lean:46
TheoremSymmetric groups have many irreducible characters of equal degree#●ready to prove
Moretó's conjecture holds: for every natural number \(k\) there is a natural number \(n_0\) such that for every \(n \ge n_0\) there are a natural number \(d\) and irreducible representations \(\rho_1, \dots, \rho_k\) of the symmetric group \(S_n\) into \(\mathrm{GL}_d(\mathbb{C})\) that are pairwise inequivalent.
public theorem_wanted symmetricGroupManyCharactersOfEqualDegree_holds :
symmetricGroupManyCharactersOfEqualDegree
def symmetricGroupManyCharactersOfEqualDegree : Prop :=
∀ k : ℕ, ∃ n₀ : ℕ, ∀ n ≥ n₀, ∃ (d : ℕ)
(ρ : Fin k → (Equiv.Perm (Fin n) →* Matrix.GeneralLinearGroup (Fin d) ℂ)),
(∀ i, IsIrreducibleRep (ρ i)) ∧ ∀ i j, i ≠ j → ¬ IsEquivalentRep (ρ i) (ρ j)
WantedExt/GroupTheory/SymmetricGroupEqualCharacterDegreesKourovka16Problem67Wanted.lean:53
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.67 (A. Moretó); resolution: D. A. Craven, Symmetric group character degrees and hook numbers, Proc. London Math. Soc. (3) 96 (2008), 26-50, arXiv:0709.0897, Theorem 1.2 (the size of a largest set of irreducible characters of S_n of one degree tends to infinity), the case k = 1 of Theorem 1.1 (for any k and ℓ and all sufficiently large n, S_n has k disjoint sets of ℓ irreducible characters, equal degrees within each set); Kourovka Archive, Problem 16.67 (This is proved), https://arxiv.org/abs/0709.0897.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.