Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

A p-section with no local block inducing to the chosen global block

Example

Assume the Axiom of Choice. Let G=S3, p=2, and work over a splitting 2-modular system whose residue field is algebraically closed. Let B1 be the defect-zero block containing the ordinary degree-two character χstd, and let t be a transposition. The centralizer CG(t)=t has one block c, and it induces to the principal block B0, not to B1. Thus no local block over this 2-section induces to B1. If φ is the unique local irreducible Brauer character, then dχstd,φt=0,χstd(t)=0.

Facts & Assumptions

Given: AC, the algebraically closed splitting system, S3, its two blocks in characteristic 2, and the transposition in the Example.

[F1]

The preceding example gives the two blocks B0,B1, with B0 principal and B1 of defect zero, and gives CG(t)=t, its sole block c, and cG=B0 (p-sections and Brauer subsections in S3).

[F2]

Block idempotents lift uniquely from kG to OG, and ordinary irreducible characters have unique block membership (Block idempotents lift uniquely from kH to OH and Blocks partition the ordinary and Brauer irreducible characters).

[F3]

Brauer's Second Main Theorem restricts a generalized expansion to local blocks inducing to the row's global block (Brauer's Second Main Theorem), under the algebraically closed and AC hypotheses (An algebraically closed field: every nonconstant polynomial has a root in the field and The Axiom of Choice).

Verification

1.1

Put a=(123), C=a+a2, and let T be the sum of the three transpositions. The center of kG has basis 1,T,C, and in characteristic 2 one directly obtains T2=1+C, C2=C, and TC=0. Thus its only nonzero primitive central idempotents are e=1+C and f=C. The first acts as 1 on the trivial module, so it is the principal block idempotent for B0; F1 then identifies f with the remaining block B1. In OG, the idempotents e^=(1+a+a2)/3 and f^=1e^ reduce respectively to e and f. By uniqueness in F2 they are the integral block lifts. Let W={(x1,x2,x3)K3:x1+x2+x3=0} with the coordinate-permutation action. The operator e^ averages over a and projects onto Wa. An a-fixed vector has equal coordinates, and its coordinate sum is 3x1, so Wa=0. If a line in W were G-stable, the scalar λ by which a acted would satisfy λ3=1 and, from tat=a1, λ=λ1; hence λ=1, contrary to Wa=0. Thus W is irreducible and affords χstd. Now e^W=0 and f^W=W, making χstd a row of B1 by F2.

F1F2algebra
2.1

By F1, the only local block over u=t induces to B0, whereas step 1.1 puts the row χstd in B1. F3 therefore gives dχstd,φt=0 for every φIBr(CG(t),c).

F1F3step 1.1
3.1

More explicitly, kCG(t)k[X]/((X1)2) has the single simple quotient k, so there is exactly one local irreducible Brauer character φ, with φ(1)=1. The only 2-regular element of CG(t)C2 is v=1. The full generalized-decomposition identity at tv=t therefore is χstd(t)=dχstd,φtφ(1)=0. Equivalently, F3's restricted sum for the block B1 is empty.

F1F3step 2.1algebra
4.1

There is also a direct characteristic-zero check. On the basis v1=(1,1,0), v2=(0,1,1) of W, the transposition t=(12) satisfies tv1=v1 and tv2=v1+v2, so its matrix has trace 0. This agrees with step 3.1. The example is a genuine empty-local-support boundary case; it does not purport to compute a larger generalized-decomposition table. Algebraic closedness and AC are used only through F3 and the preceding AC-stated example.

F3step 1.1step 3.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

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