LemmaStatement: Literature-sourcedProof: 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.

A finite module has the union of its generator-cyclic supports

Statement

If a left $R$ -module $M$ is generated by $m_{1}, \dots, m_{r}$ , then

{Supp}_{R} (M) = ⋃_{i = 1}^{r} {Supp}_{R} (R / {Ann}_{R} (m_{i})) .

Facts & Assumptions

Given: A commutative ring $R$ , a left $R$ -module $M$ , and generators $m_{1}, \dots, m_{r}$ of $M$ .

[L1]

A prime ideal $p$ lies in ${Supp}_{R} (M)$ exactly when ${Ann}_{R} (m) \subseteq p$ for some $m \in M$ (A prime lies in the support exactly when some element has annihilator inside it).

[L2]

For an ideal $I$ , the support of $R / I$ is the set of primes containing $I$ (The support of a cyclic quotient is its vanishing set).

[L3]

The generators $m_{1}, \dots, m_{r}$ generate every element of $M$ by finite $R$ -linear combinations (Generated submodule, cyclic and finitely generated modules, module basis and free module).

Proof

technique · direct

1.1

If $r = 0$ , then $M = 0$ because the empty list generates only the zero submodule. Both sides are therefore empty, so the formula holds. Hence assume $r \geq 1$ .

L3algebra

1.2

Suppose $p \in {Supp}_{R} (M)$ . By [L1], choose $m \in M$ with ${Ann}_{R} (m) \subseteq p$ , and write $m = \sum_{i} r_{i} m_{i}$ using [L3]. If no ${Ann}_{R} (m_{i})$ were contained in $p$ , choose $t_{i} \in {Ann}_{R} (m_{i}) ∖ p$ for every $i$ ; then $t = t_{1} \dots t_{r} \notin p$ because $p$ is prime, but $t m = 0$ , so $t \in {Ann}_{R} (m) \subseteq p$ , a contradiction. Thus ${Ann}_{R} (m_{i}) \subseteq p$ for some $i$ , and [L2] gives $p \in {Supp}_{R} (R / {Ann}_{R} (m_{i}))$ .

L1L2L3choose

1.3

Conversely, if $p \in {Supp}_{R} (R / {Ann}_{R} (m_{i}))$ for some $i$ , then [L2] gives ${Ann}_{R} (m_{i}) \subseteq p$ , and [L1] applied to the element $m_{i} \in M$ gives $p \in {Supp}_{R} (M)$ .

L1L2

2.1

Steps 1.1, 1.2, and 1.3 prove the union formula.

step 1.1step 1.2step 1.3∎

Depends on

Used by

For a finite module, support is the set of primes containing the annihilator Theorem

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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., (13.27) (standard reference, not scraped)