LemmaStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

Vanishing sets of arbitrary sums

Statement

Let $R$ be a commutative ring, and let $(I_{λ})_{λ \in Λ}$ be a family of ideals of $R$ . Write $\sum_{λ \in Λ} I_{λ}$ for the ideal of finite sums of elements drawn from the family, with the empty sum equal to $0$ . Then

V ⁣ (\sum_{λ \in Λ} I_{λ}) = ⋂_{λ \in Λ} V (I_{λ}) .

Facts & Assumptions

Given: A commutative ring $R$ and a family $(I_{λ})_{λ \in Λ}$ of ideals of $R$ .

[L1]

$V (K)$ is the set of prime ideals containing the ideal $K$ (The prime spectrum and vanishing sets).

Proof

technique · direct

1.1

If $p \in V ⁣ (\sum_{λ} I_{λ})$ , then $\sum_{λ} I_{λ} \subseteq p$ . Since every $I_{λ}$ is contained in that sum, one has $I_{λ} \subseteq p$ for every $λ$ , so $p \in V (I_{λ})$ for all $λ$ .

L1given

1.2

Conversely, if $p \in V (I_{λ})$ for every $λ$ , then each $I_{λ}$ lies in $p$ . Because $p$ is an ideal, it contains every finite sum of elements coming from the family, hence it contains $\sum_{λ} I_{λ}$ . Therefore $p \in V ⁣ (\sum_{λ} I_{λ})$ .

L1givenalgebra

2.1

Steps 1.1 and 1.2 prove the displayed equality.

step 1.1step 1.2∎

Depends on

Used by

Vanishing-set identities Lemma

Dependency tree · two levels

5 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, §14 The spectrum of a ring (standard reference, not scraped)
A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., §13 The Spectrum of a Ring (standard reference, not scraped)