Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-13
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.

Corresponding block bimodules are Green correspondents

Statement

Assume AC. Let B be a block of kG with defect group D, and let b be its Brauer correspondent in N=NG(D). Then B and b, viewed as indecomposable double-group modules, are Green correspondents for G×G, N×N and vertex ΔD.

Facts & Assumptions

Given: The stated finite groups, splitting residue field and corresponding blocks.

[A1]

The Axiom of Choice is assumed only through the published Green theorem's finite-length chain and selection argument.

[F1]

The Brauer correspondent of a block supplies bG=B and defect group D for both blocks.

[F2]

Block bimodule for the double group supplies their nonzero indecomposable double-group actions.

[F3]

Green correspondence for modules of vertex exactly p gives the unique same-vertex restriction summand and its inverse induction correspondent under AC.

[F4]

Defect group and numerical defect of a block translates defect D to vertex ΔD.

Proof

1.1F1F2F4algebra

If (x,y) normalizes ΔD, conjugation and coordinate projection give xDx−1=yDy−1=D. Thus x,y∈N and NG×G(ΔD)≤N×N. By F1, F2 and F4 both blocks are nonzero indecomposable modules with vertex exactly ΔD, and the defining induction property gives b∣Res⁡N×NB. The global vertex is already proved by the Brauer bijection; it is not inferred from this summand relation.

2.1A1F3step 1.1algebra∎

Apply F3 under A1 using the normalizer containment in step 1.1. Its unique vertex-ΔD restriction summand must be b, and the inverse correspondence sends b to B. These are exactly the two Green-correspondence assertions. When D=1 or N=G, the double-group normalizer interval is the identity case and the correspondence fixes the block. The only added AC use is application of F3, whose inherited finite-length argument declares it; the finite group calculation in step 1.1 and the block bijection do not use AC.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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