Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Brauer's Second Main Theorem

Statement

Assume the Axiom of Choice. Let (K,O,k) be a splitting p-modular system for a finite group G, with k algebraically closed. Let B be a block of kG, let χIrrK(G,B), let u be a p-element, and put H=CG(u). If c is a block of kH and φIBr(H,c), then dχ,φu0cG=B. Equivalently, for every p-regular vH, χ(uv)=c a block of kHcG=B φIBr(H,c)dχ,φuφ(v).

Facts & Assumptions

Given: AC and the modular system, block, character, p-element, local block, and Brauer character in the Statement.

[F1]

Generalized decomposition numbers give the unique full expansion of vχ(uv) on the p-regular elements of H (Generalized decomposition numbers exist and are unique).

[F2]

The induced local block cG is defined by the subsection convention (Brauer subsections and B-subsections).

[F3]

If cGB, the lifted c-component χc of the restricted character vanishes at every uv under the algebraically closed residue-field hypothesis (Local block projection controls p-section character support and An algebraically closed field: every nonconstant polynomial has a root in the field).

[F4]

Ordinary and Brauer irreducibles lie in unique blocks, and ordinary decomposition numbers between distinct blocks are zero (Blocks partition the ordinary and Brauer irreducible characters and After block ordering, the decomposition matrix is block diagonal).

[F5]

The irreducible Brauer characters of H are linearly independent on its p-regular elements (Irreducible Brauer characters form a basis of the p-regular class functions).

[F6]

AC is available (The Axiom of Choice) and is used through the AC-stated subsection and local-projection suppliers F2–F3. The basis partition and all sums below are finite.

Proof

1.1

Write the ordinary restriction as ResHGχ=ζIrrK(H)nχ,ζζ. For a block c of kH, its lifted idempotent selects exactly the ordinary constituents in c, so χc(uv)=ζIrrK(H,c)nχ,ζλu,ζζ(v). On p-regular v, expand each ζ(v) by ordinary decomposition numbers. F4 deletes all terms outside the block c. Conversely, in the defining formula for dχ,φu with φIBr(H,c), F4 deletes every ζ outside c. Therefore χc(uv)=φIBr(H,c)dχ,φuφ(v) for every p-regular vH.

F1F4algebra
2.1

Suppose cGB. F3 makes the left side of the last display zero for every p-regular v. Linear independence in F5 then gives dχ,φu=0 for every φIBr(H,c). The contrapositive is the asserted support implication.

F3F5F6step 1.1
3.1

F1 gives the full expansion χ(uv)=cφIBr(H,c)dχ,φuφ(v), where F4 partitions the Brauer basis by its unique blocks. Step 2.1 deletes exactly the summands with cGB and proves the displayed restricted formula in the Statement. Conversely, if that restricted formula holds, subtracting it from F1's full expansion and applying F5 block by block forces every coefficient in a noninducing block to be zero, recovering the support implication.

F1F2F4F5step 2.1
4.1

When u=1, one has H=G, cG=c, and dχ,φ1=dχ,φ; the theorem becomes ordinary block diagonality from F4. Empty local Brauer-character sets contribute empty sums, and no converse asserting that a permitted coefficient is nonzero has been used. Algebraic closedness and AC enter exactly through F2–F3.

F1F2F4F6

Depends on

Used by

Dependency tree · two levels

30 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources