ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

The p-primary quotient Q/Z_(p) over Z_(p) shows finite generation is essential in Nakayama

Example

Fix a prime number $p$ and let $R = Z_{(p)}$ . The $R$ -module

M = Q / Z_{(p)}

satisfies $p M = M$ but $M \neq 0$ , so Nakayama's lemma fails without finite generation.

Facts & Assumptions

Given: A prime number $p$ , the local ring $R = Z_{(p)}$ , and the $R$ -module $M = Q / Z_{(p)}$ .

[L1]

The localisation $Z_{(p)}$ is a local ring at the prime $(p)$ , and $Q$ is the field of fractions of $Z$ into which $Z_{(p)}$ embeds (Localisation at a prime ideal: $R_{p} = (R ∖ p)^{- 1} R$ , $R_{p}$ is local with unique maximal ideal $p R_{p}$ , $R_{p} / p R_{p} ≅ Frac (R / p)$ is the residue field at $p$ , $Frac (D)$ is a field and $d \mapsto d / 1$ embeds the integral domain $D$ ).

Verification

technique · direct

1.1

The class of $1 / p$ is nonzero in $Q / Z_{(p)}$ , because $1 / p \notin Z_{(p)}$ . Hence $M \neq 0$ .

1.2

Every element of $M$ has the form $q + Z_{(p)}$ with $q \in Q$ . Then $p (q / p + Z_{(p)}) = q + Z_{(p)}$ , so multiplication by $p$ is surjective and therefore $p M = M$ .

L1algebra

1.3

The module $M$ is not finitely generated. If classes $q_{1} + Z_{(p)}, \dots, q_{r} + Z_{(p)}$ generated $M$ , choose $N$ so that every $q_{i}$ has denominator dividing $p^{N}$ modulo $Z_{(p)}$ . Then every generated class would also have denominator dividing $p^{N}$ , but $1 / p^{N + 1} + Z_{(p)}$ would not lie in that span.

L1algebra

2.1

So $p M = M$ and $M \neq 0$ hold for a module that is not finitely generated, exactly showing why the finite-generation hypothesis is essential.

step 1.1step 1.2step 1.3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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

J. S. Milne, A Primer of Commutative Algebra, v4.03, Lemma 3.9 (standard reference, not scraped)
The Stacks Project, Section 10.19: Nakayama's Lemma (standard reference, not scraped)