broue_conjecture

⚠️ Retired — incorrect formalization

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

Broué's abelian defect group conjecture (1990): If a block B has an abelian defect group D, then B is derived equivalent to its Brauer correspondent. Proved for symmetric groups, abelian groups, many simple groups. Open in general.

Why this node was retired

The posted statement is

import Mathlib

theorem broue_conjecture (G : Type*) [Group G] [Fintype G]
    (p : ℕ) (hp : Nat.Prime p)
    (D : Subgroup G) (hD_ab : ∀ a b : D, a * b = b * a) :
    ∃ (B b : True), True := by
  sorry

The goal is ∃ (B b : True), True, closed by ⟨trivial, trivial, trivial⟩. The group G, the prime p and the abelian defect subgroup D are never used, and the blocks B and b are declared with type True rather than as blocks of anything.

What a faithful statement would require

Blocks of the group algebra with defect group D and of its Brauer correspondent must be real objects, and the conclusion must assert a derived equivalence between the corresponding module categories.

No corrected replacement node exists yet.