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.

Nagao decomposition for restriction to a centralizer

Statement

Assume the Axiom of Choice. Let (K,O,k) be a splitting p-modular system for a finite group G. Let B be a block of kG, let B^ denote its block-idempotent lift in OG, and let D be a p-subgroup such that DCG(D)HNG(D). If M is a finite-free OG-lattice with B^M=M, then there is an OH-decomposition ResHGM=McorrMerr with the following properties.

  1. Every indecomposable summand of Mcorr belongs to the lift c^ of a block c of kH satisfying cG=B.
  2. Every indecomposable summand of Merr has a vertex that does not contain D (indeed, no vertex of such a summand contains D).

Either displayed summand may be zero.

Facts & Assumptions

Given: AC and the system, groups, blocks, lift, and lattice in the Statement.

[F1]

Block idempotents have unique central lifts to integral group algebras (Block idempotents lift uniquely from kH to OH).

[F2]

Every finite-rank OH-lattice has a finite Krull--Schmidt decomposition, and an indecomposable has local endomorphism ring (Krull-Schmidt holds for finite-rank OH-lattices).

[F3]

Integral relative traces satisfy Higman's criterion, and a vertex of an indecomposable relatively R-projective lattice is contained in an H-conjugate of R (Integral Mackey decomposition and Higman's criterion for group lattices and Relative projectivity and vertices for integral group lattices).

[F4]

The center of a modular block is local (Block centre locality and trace ideal sums).

[F5]

Block induction is the unique restriction-summand block and exists under centralizer containment (A block induced from a subgroup and Centralizer containment makes block induction well-defined).

[F6]

A normal p-subgroup lies in every block defect group (Normal p core lies in every block defect group).

[F7]

AC is available (The Axiom of Choice) and discharges the inherited published contracts in F4–F6. All new sums and decompositions below are finite.

Proof

1.1

Since HNG(D), the group D is normal in H. Hence DOp(H), and F6 shows that every defect group Q of every block c of kH contains D. It follows that CG(Q)CG(D)H. Thus F5 defines cG for every block c of kH.

F5F6F7
1.2

We record the block corner that controls an error component. Write b for the idempotent of the global block B, and let πH:kGkH delete coefficients outside H. For a block c of kH, the maps kHckG,acπH(a):kGkHc split the identity H-double-coset copy of the block bimodule kHc. The corner of left multiplication by b on this copy is left multiplication by cπH(b). If that corner were a unit in EndH×H(kHc)=Z(kHc), normalizing the second map by its inverse would split kHc from the restriction of the global block kGb. By F5 this would imply cG=B. Therefore, when cGB, the element cπH(b) is a nonunit of the local algebra Z(kHc) and hence is nilpotent.

F4F5
1.3

The coefficients of the central element B^ are constant on G-conjugacy classes, hence on H-conjugacy classes. The complement of H in G is H-conjugation invariant, so for suitable coefficients axO and representatives x of its finitely many H-classes, B^πH(B^)=x(GH)/H-conjaxTrCH(x)H(x). Here the trace is for the conjugation action: its summands are exactly the elements of the H-class of x. Moreover, D≰CH(x), because the opposite containment would put x in CG(D)H.

givenalgebra
2.1

Let c^ denote the lift of c. The lifts are pairwise orthogonal and sum to 1: their products and the difference between their sum and 1 are central idempotents reducing respectively to 0 and 0, so F1's uniqueness forces those idempotents to vanish. Consequently M=cc^M. Define Mcorr=c:cG=Bc^M,Merr=c:cGBc^M. F2 decomposes each component into indecomposables, and the first asserted property follows directly from the definition.

F1F2step 1.1
2.2

Let U be an indecomposable summand of c^M for a block c with cGB, and choose H-linear split maps i:UM and r:MU. Put E=EndOH(U), which is local by F2. Integral coefficient truncation πH:OGOH commutes with reduction. Thus step 1.2 shows that the reduction of c^πH(B^) is nilpotent. Some power of this element therefore belongs to mOH, where m is the maximal ideal of O. Since c^ acts as the identity on U and the central element πH(B^) commutes with the H-projection ir, it follows that s=rπH(B^)iE has a power in mE. Such a power cannot be a unit, so s is a nonunit and belongs to J(E).

F1F2step 1.2
3.1

The equality B^M=M and the H-linearity of i,r now give inside E 1U=s+x(GH)/H-conjTrCH(x)H(axrxi). Indeed, axrxi is CH(x)-linear, and taking the H-linear corner commutes with each finite relative trace. The first term lies in J(E) by step 2.2. If every displayed trace term were a nonunit, their finite sum would also lie in the maximal ideal J(E), contradicting the equality. Hence one trace term is a unit. For βE and any CH(x)-endomorphism α of U, one has βTrCH(x)H(α)=TrCH(x)H(βα) and TrCH(x)H(α)β=TrCH(x)H(αβ). Thus the image of this relative trace is a two-sided ideal of E; since it contains a unit, it contains 1U. Higman's criterion makes U relatively CH(x)-projective for the corresponding x.

F2F3F7step 2.2step 1.3
4.1

Let P be any vertex of U. F3 gives PhCH(x)h1 for some hH. Were DP, normality of D in H would imply D=h1DhCH(x), contrary to step 1.3. Thus D≰P, proving the second property. If D=1, the hypotheses force H=G, so the outside-class sum is empty and all error components are zero; if M=0, both conclusions are vacuous. These also cover all boundary cases without an empty-sum inference.

F3step 2.1step 1.3step 3.1

Depends on

Used by

Dependency tree · two levels

24 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