Alphabeta Math
LemmaStatement: 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.

Centralizer containment makes block induction well-defined

Statement

Let b=kHe be a block of kH with defect group D, where k comes from a splitting p-modular system for finite G. If CG(D)≤H≤G, then bG is defined. If also H≤NG(D), then on every z∈Z(kG), and in particular on class sums, λbG(z)=λb(Br⁡D(z)). In this formula the Brauer projection lands in kCG(D)⊆kH and is central in kH.

Facts & Assumptions

Given: The stated groups, field and nonzero block b.

[F1]

A block induced from a subgroup defines induction and proves that distinct block bimodules are nonisomorphic.

[F2]

The group algebra's double action and its permutation-module realization are Group algebra bimodule is induced from the diagonal.

[F3]

Mackey, vertex containment and finite summand extraction are Relative projectivity mackey intersections for finite modules.

[F4]

Diagonal block vertices are Block bimodule has a diagonal vertex.

[F5]

The Brauer projection deletes coefficients outside CG(D) and is multiplicative on the fixed algebra, as used in Central idempotents under the Brauer homomorphism.

[F6]

Modular block central characters correspond to blocks gives λb and each global λB. The block-center identification End⁡H×H(b)=Z(b) and its unique nilpotent maximal ideal are supplied separately by Block bimodule for the double group. Since λb is a unital map to k, its kernel is a maximal ideal and therefore is that unique nilpotent ideal.

[F7]

Normal p-subgroups act trivially on simple modules by A normal p-subgroup acts trivially on every simple module in characteristic p.

[F9]

By Defect group and numerical defect of a block, saying that D is a defect group of b means exactly that ΔD is a vertex of the block bimodule b.

Proof

1.1F2F3algebra

By F2, as an H×H-module M=kG splits over its double-coset orbits into kH⊕⨁t∉Hk[HtH]. Each orbit module is induced from its point stabilizer: the map from stabilizer cosets to orbit points is a bijection, exactly as in F2. If an indecomposable summand of k[HtH] had a vertex containing an (H×H)-conjugate of ΔD, F3 would place that diagonal conjugate in a conjugate of the point stabilizer. Equivalently ΔD would fix some point t′∈HtH, so dt′=t′d for every d∈D. This puts t′∈CG(D)≤H, impossible when t∉H. The same argument proves the exclusion for any p-subgroup Q≤H with CG(Q)≤H, replacing D by Q.

2.1F1F4F8F9step 1.1algebra

The identity orbit kH contains b exactly once in its block decomposition, by F1. By F4, F9 and step 1.1 no other orbit contains an isomorphic summand. Thus b has multiplicity one in M. Decomposing M=kG into global blocks and applying F8 shows exactly one global block B has b as a restriction summand. By F1 this is bG. This proves existence without the extra normalizer assumption.

3.1F6F8step 2.1algebra

We identify its central character carefully. Use the decomposition M=b⊕X, where the projection onto b is r(a)=eπH(a) and πH deletes coefficients outside H. Decompose X into indecomposables Xj by F8; none is isomorphic to b by step 2.1. Any composite b→Xj→b is a nonunit in End⁡H×H(b): if invertible it would split b from Xj, forcing an isomorphism by indecomposability. This endomorphism ring is Z(b), as in F6's block-center construction; its nonunits form the nilpotent ideal Jb. Therefore for T∈End⁡H×H(M) the function χ(T)=λb(rT∣b) is a unital algebra homomorphism: in the corner of a composite, all cross-composites through the Xj vanish modulo Jb, leaving the product of the two corners.

4.1F6step 2.1step 3.1algebra

Let EC be projection of M onto a global block C. If C≠B, decompose its restriction into indecomposables, none isomorphic to b, and step 3.1 gives χ(EC)=0. Since the projections sum to the identity, χ(EB)=1. For z∈Z(kG) let Lz be multiplication by z. On B, multiplication by z−λB(z) is nilpotent by F6. Hence (Lz−λB(z))EB is nilpotent on M, and applying the field-valued homomorphism χ gives χ(Lz)=λB(z). But its corner on the explicit b⊂kH is multiplication by eπH(z), because πH is an H-bimodule projection. Thus λB(z)=λb(πH(z)). Centrality of z makes πH(z)∈Z(kH).

5.1F5F6F7step 4.1algebra

Now assume H≤NG(D), so D⊴H. Let S be a simple b-module, whose existence and scalar character are proved in F6. F7 says every d∈D acts trivially on S. Expand πH(z) in group elements and partition H∖CG(D) into conjugation orbits of D. Each orbit has size a power of p greater than one; its coefficients in z are constant. All conjugate elements have the same operator on S, so its orbit sum acts as zero in characteristic p. The remaining terms are precisely Br⁡D(z) by F5. Since H normalizes D, it preserves CG(D) and this projection is central in kH. Consequently the two central elements have the same scalar on S, giving λb(πH(z))=λb(Br⁡D(z)). Combine with step 4.1 to prove the formula.

6.1F1step 1.1step 2.1step 5.1algebra∎

For D=1, the containment assumption forces H=G and all projections in the formula are identity. For H=G induction is already the identity by F1. Empty off-identity double-coset families and empty noncentralizing orbit families simply contribute zero in the above sums. Every decomposition and orbit calculation is finite; no AC is added. The extra normalizer assumption was used only in step 5.1, so the formula has not been asserted outside its stated domain.

Depends on

Used by

Dependency tree · two levels

23 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