Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedaudited 2026-09-12
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.

Green restriction summand with the same vertex

Example

Assume AC for the inherited Green-correspondence identification. Let k have characteristic 2, G=S3, P=H={1,(12)} and M=k with trivial action, so every action matrix is [1]. Then NG(P)=P, M has vertex P, and Res⁡HGM=k is its unique indecomposable restriction summand, also of vertex P. It is therefore the Green correspondent. The explicit calculations below do not use choice.

Facts & Assumptions

Given: These concrete groups and their one-dimensional trivial modules.

[A1]

AC (The Axiom of Choice) is needed only for the inherited general correspondence.

[F1]

The exact-P Green correspondence identifies the unique same-vertex restriction summand (Green correspondence for modules of vertex exactly p).

[F2]

Relative projectivity is equivalent to writing the identity as a relative trace (Higman's criterion characterizes relative projectivity through the relative trace idempotent test).

Verification

1.1givenalgebra

The six permutations are 1,(12),(13),(23),(123),(132). Conjugation sends (12) to (g(1) g(2)). To normalize P, a permutation must preserve {1,2} and fix 3, hence is 1 or (12). Thus NG(P)=P=H. A one-dimensional nonzero module is indecomposable, since dimensions of nonzero summands would add to at least two.

1.2F2F3givenalgebra

Every endomorphism of a one-dimensional trivial module is multiplication by a scalar a. For a subgroup D≤G, its relative trace is multiplication by [G:D]a, since each conjugation in the trace formula acts trivially. For D=P, the trace of the identity is 3⋅1=1 in characteristic 2, proving relative P-projectivity. For D=1, every trace is 6a=0, never the identity. The only proper subgroup of P is 1, so P is a vertex of M.

2.1F2F3step 1.1algebra

Restriction is the same trivial one-dimensional space. Its trace from H is 1 on the identity, whereas its trace from 1 is 2a=0 for every scalar. Thus it is relatively H-projective and not relatively 1-projective, so its vertex is P=H. Its dimension gives precisely one nonzero indecomposable summand and no nonzero complement.

3.1A1F1step 1.1step 1.2step 2.1∎

The normalizer condition in 1.1 and the two vertex calculations in 1.2–2.1 verify every hypothesis of F1. Under A1 that corollary identifies the sole restriction summand k as the Green correspondent. No group or vector-space choice was needed for the matrices or traces; AC is only propagated from F1. The nonzero condition is witnessed by dim⁡kk=1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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.