LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

A cyclic submodule is a residue module by its annihilator

Statement

Let $R$ be a commutative ring, let $M$ be a left $R$ -module, and let $m \in M$ . Then the cyclic submodule $R m$ is naturally isomorphic to

R / {Ann}_{R} (m) .

Facts & Assumptions

Given: A commutative ring $R$ , a left $R$ -module $M$ , and an element $m \in M$ .

[L1]

The annihilator of $m$ is ${Ann}_{R} (m) = {r \in R : r m = 0}$ (Annihilators, torsion elements and the torsion subset of a module).

Proof

technique · direct

1.1

Define $φ : R / {Ann}_{R} (m) \to R m$ by $φ (r + {Ann}_{R} (m)) = r m .$ If $r - r^{'} \in {Ann}_{R} (m)$ , then $(r - r^{'}) m = 0$ , so $r m = r^{'} m$ ; hence $φ$ is well-defined. Every element of $R m$ has the form $r m$ , so $φ$ is surjective.

L1givenconstruct

2.1

If $φ (r + {Ann}_{R} (m)) = 0$ , then $r m = 0$ , so $r \in {Ann}_{R} (m)$ by [L1]. Thus $r + {Ann}_{R} (m) = 0$ and $φ$ is injective.

L1step 1.1

3.1

Steps 1.1 and 2.1 show that $φ$ is the claimed natural isomorphism.

step 1.1step 2.1∎

Depends on

Annihilators, torsion elements and the torsion subset of a module

Used by

Associated primes are exactly primes of embedded cyclic residue modules Lemma

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)
J. S. Milne, A Primer of Commutative Algebra, v4.03, §19 (standard reference, not scraped)