TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Support of an arbitrary direct sum is the union of the supports

Statement

For any family $(M_{i})_{i \in I}$ of left $R$ -modules,

{Supp}_{R} ⁣ (⨁_{i \in I} M_{i}) = ⋃_{i \in I} {Supp}_{R} (M_{i}) .

Facts & Assumptions

Given: A commutative ring $R$ and a family $(M_{i})_{i \in I}$ of left $R$ -modules.

[L1]

A prime ideal $p$ lies in the support of a module exactly when the localisation at $p$ is nonzero (Support of a module).

[L2]

Localisation commutes with arbitrary direct sums (Localisation commutes with quotient modules and arbitrary direct sums).

Proof

technique · direct

1.1

Fix a prime ideal $p$ . By [L2], ${(⨁_{i} M_{i})}_{p} ≅ ⨁_{i} (M_{i})_{p}$ . This direct sum is nonzero exactly when at least one summand $(M_{i})_{p}$ is nonzero.

2.1

By [L1], step 1.1 says exactly that $p$ lies in the support of $⨁_{i} M_{i}$ if and only if it lies in the support of some $M_{i}$ .

L1step 1.1

3.1

Since this holds for every prime ideal $p$ , the support of the direct sum is the union of the supports.

step 2.1∎

Depends on

Used by

The support of the direct sum over all primes of Z/pZ is the set of all nonzero prime ideals of Z Example

Dependency tree · two levels

8 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., Section 13 (standard reference, not scraped)
The Stacks Project, Section 10.40: Support (standard reference, not scraped)