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 have characteristic , , and with trivial action, so every action matrix is . Then , has vertex , and is its unique indecomposable restriction summand, also of vertex . 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.
AC (The Axiom of Choice) is needed only for the inherited general correspondence.
The exact- Green correspondence identifies the unique same-vertex restriction summand (Green correspondence for modules of vertex exactly p).
Relative projectivity is equivalent to writing the identity as a relative trace (Higman's criterion characterizes relative projectivity through the relative trace idempotent test).
A vertex is a minimal -subgroup for relative projectivity (A vertex is a minimal p-subgroup for relative projectivity, and a source is an indecomposable inducing summand there).
Verification
The six permutations are . Conjugation sends to . To normalize , a permutation must preserve and fix , hence is or . Thus . A one-dimensional nonzero module is indecomposable, since dimensions of nonzero summands would add to at least two.
Every endomorphism of a one-dimensional trivial module is multiplication by a scalar . For a subgroup , its relative trace is multiplication by , since each conjugation in the trace formula acts trivially. For , the trace of the identity is in characteristic , proving relative -projectivity. For , every trace is , never the identity. The only proper subgroup of is , so is a vertex of .
Restriction is the same trivial one-dimensional space. Its trace from is on the identity, whereas its trace from is for every scalar. Thus it is relatively -projective and not relatively -projective, so its vertex is . Its dimension gives precisely one nonzero indecomposable summand and no nonzero complement.
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 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 .
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.