Character degrees of Sylow subgroups

DefinitionIrreducible complex representation degrees#✓fully proved

For a group \(G\), the set of natural numbers \(d\) such that \(G\) has an irreducible complex representation of finite dimension \(d\); for a finite group these are the degrees \(\chi(1)\) of its irreducible characters.

def irreducibleDegrees (G : Type*) [Group G] : Set ℕ :=
  {d | ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
    (ρ : Representation ℂ G V), ρ.IsIrreducible ∧ Module.finrank ℂ V = d}

Used by 1

Used byLargest \(p\)-adic exponent of the irreducible degrees

DefinitionLargest \(p\)-adic exponent of the irreducible degrees#✓fully proved

For a natural number \(p\) and a group \(G\), \(e_p(G)\) is the supremum in \(\mathbb{N}\) of the exponents of \(p\) in the prime factorizations of the dimensions of the finite-dimensional irreducible complex representations of \(G\), where the supremum of an empty or unbounded set is \(0\). For a prime \(p\) and a finite group \(G\), it is the largest \(e\) such that \(p^e\) divides the degree \(\chi(1)\) of some irreducible character \(\chi\) of \(G\).

noncomputable def maxPPartExponent (p : ℕ) (G : Type*) [Group G] : ℕ :=
  sSup ((fun d => d.factorization p) '' irreducibleDegrees G)

Uses 1 · Used by 1

Statement usesIrreducible complex representation degrees

Used byKourovka Problem 15.62 (\(p\)-parts of character degrees of Sylow subgroups)

DefinitionKourovka Problem 15.62 (\(p\)-parts of character degrees of Sylow subgroups)#✓fully proved

The statement, asked by A. Moretó, that there is a function \(f \colon \mathbb{N} \to \mathbb{N}\) such that \(e_p(P) \le f(e_p(G))\) for every prime \(p\), every finite group \(G\) and every Sylow \(p\)-subgroup \(P\) of \(G\), where \(e_p(H)\) is the largest exponent of \(p\) dividing an irreducible character degree of \(H\).

def sylowCharacterDegreeExponentBounded : Prop :=
  ∃ f : ℕ → ℕ, ∀ p : ℕ, p.Prime → ∀ (G : Type) [Group G] [Finite G] (P : Sylow p G),
    maxPPartExponent p (P : Subgroup G) ≤ f (maxPPartExponent p G)

Uses 1 · Used by 1

Statement usesLargest \(p\)-adic exponent of the irreducible degrees

Used byCharacter degrees of Sylow subgroups are bounded in terms of those of the group

TheoremCharacter degrees of Sylow subgroups are bounded in terms of those of the group#●ready to prove

There is a function \(f \colon \mathbb{N} \to \mathbb{N}\) such that for every prime \(p\), every finite group \(G\) and every Sylow \(p\)-subgroup \(P\) of \(G\), \(e_p(P) \le f(e_p(G))\), where \(e_p(H)\) is the largest exponent of \(p\) dividing an irreducible character degree of \(H\).

One function works for all primes, since Yang and Qian's bound \(|G : F(G)|_p \le p^{k e_p(G)}\), with \(F(G)\) the Fitting subgroup of \(G\), has an absolute constant \(k\).

public theorem_wanted sylowCharacterDegreeExponentBounded_holds :
    sylowCharacterDegreeExponentBounded

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 15.62 (A. Moretó); resolution: Yong Yang and Guohua Qian, Adv. Math. 328 (2018), 356-366, abstract (|G : F(G)|_p ≤ p^(k e_p(G)) for a constant k, F(G) the Fitting subgroup, which settles Moretó's conjecture that e_p(P) = log_p b(P), b(P) the largest character degree of P, is bounded by a function of e_p(G)); Kourovka Archive, Problem 15.62 (answer: Yes, it is true); the solvable case is due to A. Moretó and T. R. Wolf, Adv. Math. 184 (2004), 18-36.

Uses 1

Statement usesKourovka Problem 15.62 (\(p\)-parts of character degrees of Sylow subgroups)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.