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.

p-sections and Brauer subsections in S3

Example

Assume the Axiom of Choice. Let G=S3, let p=2, and work over the residue field of a splitting 2-modular system. Fix a transposition t=(12). Then SG(1)={1,(123),(132)},SG(t)={(12),(13),(23)}. Moreover, CG(t)=tC2 has a unique block c, and cG=B0, the principal block of kS3. Thus (t,c) is a B0-subsection and is not a subsection for the defect-zero block B1. At the identity, (1,B0) and (1,B1) are respectively B0- and B1-subsections.

Facts & Assumptions

Given: AC, S3, p=2, the transposition, and the splitting system in the Example.

[F1]

A p-section is determined by the conjugacy class of the unique p-part (The p-section of a p-element).

[F2]

A B-subsection uses local-to-global block induction (Brauer subsections and B-subsections).

[F3]

The Brauer map is coefficient projection to a centralizer, and its maximal nonzero supports are the defect groups (Brauer homomorphism for a p subgroup and Defect groups are maximal Brauer support). The principal block has Sylow defect (Principal block has sylow defect).

[F4]

For a fixed p-subgroup D, Brauer's First Main Theorem gives a bijection, by block induction, between the blocks of kNG(D) having defect group D and the blocks of kG having defect group D (Brauer's First Main Theorem).

[F5]

A central p-subgroup lies in each local defect group (Central p-subgroups lie in every block defect group). AC is available (The Axiom of Choice) and is used through the AC-stated subsection and published block contracts; the calculations below are finite.

Verification

1.1

The conjugacy classes of S3 are the identity, the three transpositions, and the two 3-cycles. The identity and 3-cycles have 2-part 1, while the 2-part of a transposition is the transposition itself. All transpositions are conjugate. F1 therefore gives the two displayed sections, and these exhaust the sections indexed by conjugacy classes of 2-elements.

F1algebra
1.2

Direct commutation shows CG(t)=t. In characteristic 2, kCG(t)k[X]/(X21)=k[X]/((X1)2), which is local: its elements a+b(X1) are units exactly when a0. It therefore has one primitive central idempotent and one block c, the principal block. The group D=t is central in itself; F5 puts it in every defect group of c, and since it is already the Sylow 2-subgroup, D is the defect group of c.

F5algebra
1.3

Put a=(123), T=(12)+(13)+(23), and C=a+a2 in kG. The center of kG has basis 1,T,C, since central coefficients are constant on conjugacy classes. In characteristic 2 one computes T2=1+C, C2=C, and TC=0. Hence for z=α1+βT+γC the equation z2=z forces β=0 and α,γ{0,1}. The only central idempotents are therefore 0,1,e:=1+C, and f:=C; thus e,f are precisely the two block idempotents. The augmentation of e is 1, so e defines the principal block B0, while f defines B1. F3 gives Sylow defect D for B0. For any nontrivial 2-subgroup P of S3, one has CG(P)=P and coefficient projection gives BrP(f)=0, whereas Br1(f)=f0; F3 therefore gives defect 1 for B1.

F3algebra
2.1

If an element normalizes D, it fixes its unique nonidentity element t, and hence centralizes t. Thus NG(D)=CG(t)=D. Step 1.2 says that c has defect D, so F4 defines cG and makes it a global block of defect D. Step 1.3 says that B0 is the only such global block, because B1 has defect 1. Hence cG=B0. F2 now gives the asserted subsection statements at t.

F2F4step 1.2step 1.3
3.1

For u=1, one has CG(1)=G, and induction from G to itself fixes each block. Hence (1,Bi) is a Bi-subsection for i=0,1. No generalized-decomposition table is being asserted here. AC is used only through F2–F5.

F2F5algebra

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