LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

Associated primes are exactly primes of embedded cyclic residue modules

Statement

Let $R$ be a commutative ring, let $M$ be a left $R$ -module, and let $p$ be a prime ideal of $R$ . Then $p \in {Ass}_{R} (M)$ if and only if there exists an injective $R$ -module homomorphism $R / p ↪ M .$

Facts & Assumptions

Given: A commutative ring $R$ , a left $R$ -module $M$ , and a prime ideal $p \subseteq R$ .

[L1]

A prime ideal is associated to $M$ exactly when it is the annihilator of some element of $M$ (Associated primes of a module).

[L2]

For any $m \in M$ , the cyclic submodule $R m$ is naturally isomorphic to $R / {Ann}_{R} (m)$ (A cyclic submodule is a residue module by its annihilator).

Proof

technique · direct

1.1L1L2choose

Assume $p \in {Ass}_{R} (M)$ . By [L1], choose $m \in M$ with ${Ann}_{R} (m) = p$ . Then [L2] gives $R m ≅ R / p$ , and the inclusion $R m ↪ M$ composes with this isomorphism to give an embedding $R / p ↪ M$ .

1.2L1givenalgebra

Conversely, let $j : R / p ↪ M$ be injective, and put $m = j (1 + p)$ . Every $r \in p$ kills $1 + p$ , so $r m = 0$ . If $r m = 0$ , then $j (r + p) = 0$ , and injectivity gives $r + p = 0$ , hence $r \in p$ . Therefore ${Ann}_{R} (m) = p$ , so $p \in {Ass}_{R} (M)$ by [L1].

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove the equivalence.

Depends on

Used by

Dependency tree · two levels

4 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Lemma (17.2) (standard reference, not scraped)
The Stacks Project, Section 10.63: Associated primes (standard reference, not scraped)