LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 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 support of a cyclic quotient is its vanishing set

Statement

For an ideal $I$ of a commutative ring $R$ , ${Supp}_{R} (R / I) = {p : I \subseteq p} .$

Facts & Assumptions

Given: A commutative ring $R$ and an ideal $I ⊴ R$ .

[L1]

A prime ideal $p$ lies in ${Supp}_{R} (R / I)$ exactly when $(R / I)_{p} \neq 0$ (Support of a module).

[L2]

Localisation commutes with quotients: $(R / I)_{p} ≅ R_{p} / I R_{p}$ (Localisation commutes with quotient rings: $S^{- 1} R / S^{- 1} I ≅ {\overset{ˉ}{S}}^{- 1} (R / I)$ ).

[L3]

The local ring $R_{p}$ has maximal ideal $p R_{p}$ , and the units are exactly the fractions with numerator outside $p$ ( $R_{p}$ is local with unique maximal ideal $p R_{p}$ ).

Proof

technique · direct

1.1L1L2

Fix a prime ideal $p$ . By [L2], $(R / I)_{p} \neq 0$ exactly when $R_{p} / I R_{p} \neq 0$ .

1.2L3

If $I \subseteq p$ , then every generator $i / 1$ of $I R_{p}$ lies in the maximal ideal $p R_{p}$ from [L3], so $I R_{p}$ is proper and the quotient is nonzero.

1.3L3choose

If $I ⊈ p$ , choose $i \in I ∖ p$ . Then $i / 1$ is a unit in $R_{p}$ by [L3], and it lies in $I R_{p}$ , so $I R_{p} = R_{p}$ and the quotient is zero.

2.1step 1.1step 1.2step 1.3∎

By steps 1.1, 1.2, and 1.3, $p$ lies in ${Supp}_{R} (R / I)$ exactly when $I \subseteq p$ .

Depends on

Dependency tree · 2 levels

Sources

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