ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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.

For a finite p-group, the augmentation map from kP to the trivial module is its projective cover

Example

Let $P$ be a finite $p$ -group and let $k$ have characteristic $p$ . Then the augmentation map

$ε : k P \to k$

is the projective cover of the trivial module.

Facts & Assumptions

Given: A finite $p$ -group $P$ , a field $k$ of characteristic $p$ , and the augmentation map $ε : k P \to k$ .

[L2]

Over every characteristic- $p$ field, the algebra $k P$ is local (For a finite group and a field of characteristic p, the group algebra is local exactly when the group is a p-group).

[L3]

Projective covers exist and are unique up to isomorphism over the target (Every finite-dimensional module has a projective cover, unique up to isomorphism over the target).

Verification

technique · direct

1.1L2givenalgebra

The regular module $k P$ is projective, and $ε$ is surjective onto the trivial module. Its kernel is the augmentation ideal, which is the unique maximal ideal because [L2] makes $k P$ local. Hence the kernel is superfluous.

2.1L3step 1.1∎

By step 1.1, $ε$ is a projective cover of the trivial module. The uniqueness theorem [L3] says every projective cover of that target is isomorphic to this one over the target.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Peter Webb, A Course in Finite Group Representation Theory (23 Feb 2016 draft) (standard reference, not scraped)