alperin_weight_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result alperin_weight_conjecture is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Alperin's weight conjecture (1987): For a finite group G and prime p, the number of irreducible Brauer characters of G equals the number of weights (pairs (Q,phi) where Q is a p-subgroup and phi is a projective character of N_G(Q)/Q). Proved for many families; open in general.

Why this node was retired

The posted statement is

import Mathlib

theorem alperin_weight_conjecture (G : Type*) [Group G] [Fintype G]
    (p : ℕ) (hp : Nat.Prime p) :
    ∃ (weight_count : ℕ),
      weight_count = (∑ B : Finset G, if True then 1 else 0) ∧
      weight_count > 0 := by
  sorry

The goal is ∃ weight_count, weight_count = (∑ B : Finset G, if True then 1 else 0) ∧ weight_count > 0. The condition if True then 1 else 0 is constantly 1, so the sum is just the number of subsets of G, and the goal reduces to the arithmetic fact that 2 ^ |G| > 0. Neither irreducible Brauer characters nor weights occur anywhere.

What a faithful statement would require

A faithful statement needs the number of irreducible p-Brauer characters of G and the number of G-conjugacy classes of p-weights, and must assert that the two are equal.

No corrected replacement node exists yet.