The McKay conjecture

Source: arxiv:2410.20392, doi:10.4007/annals.2026.203.3.5 Proposed by: Vasily Ilin Open declarations: Challenge.McKay.card_pPrimeCharacters_eq Tags: group-theory, representation-theory, character-theory, mckay-conjecture MSC: 20C15, 20D20 Estimated size: ~1000000 lines of Lean

Informal statement:

• Challenge.McKay.card_pPrimeCharacters_eq — For every finite group G, every prime p, and every Sylow p-subgroup P of G, the set of character functions of simple finite-dimensional complex representations of G whose dimension p does not divide has the same cardinality as the corresponding set for the normalizer of P in G. Two simple representations have equal characters exactly when they are isomorphic, so both sets are in bijection with the sets Irr_p'(G) and Irr_p'(N_G(P)) that the McKay conjecture counts.

def Challenge.McKay.pPrimeCharacters (G : Type u_1) [Group G] (p : ℕ) : Set (G → ℂ)

The irreducible complex characters of G of p'-degree, as a set of functions: the characters of simple finite-dimensional complex representations whose dimension is not divisible by p. Two simple representations have equal characters exactly when they are isomorphic, so this set is in canonical bijection with the set Irr_{p'}(G) counted by the McKay conjecture.

Equations

• Challenge.McKay.pPrimeCharacters G p = {χ : G → ℂ | ∃ (V : FDRep ℂ G), CategoryTheory.Simple V ∧ V.character = χ ∧ ¬p ∣ Module.finrank ℂ ↑V.V}

theorem Challenge.McKay.card_pPrimeCharacters_eq (G : Type u_1) [Group G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] (P : Sylow p G) : Cardinal.mk ↑(pPrimeCharacters G p) = Cardinal.mk ↑(pPrimeCharacters (↥(Subgroup.normalizer ↑P)) p)

The McKay conjecture, now the theorem of Cabanes and Späth: for every finite group G, every prime p, and every Sylow p-subgroup P of G, the irreducible complex characters of G of degree not divisible by p are equinumerous with those of the normalizer of P in G.