TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-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 in a short exact sequence is the union of the outer supports

Statement

0 ⟶ M^{'} ⟶ M ⟶ M^{''} ⟶ 0

is a short exact sequence of left $R$ -modules, then

{Supp}_{R} (M) = {Supp}_{R} (M^{'}) \cup {Supp}_{R} (M^{''}) .

Facts & Assumptions

Given: A commutative ring $R$ and a short exact sequence $0 \to M^{'} \to M \to M^{''} \to 0$ of left $R$ -modules.

[L1]

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

[L2]

Localisation sends short exact sequences to short exact sequences (Localisation of modules is exact).

[L3]

In a short exact sequence, the left map is injective and the right map is surjective (Exact sequences and short exact sequences of modules).

Proof

technique · direct

1.1

Fix a prime ideal $p$ . By [L2], localising the given short exact sequence at $p$ gives $0 \to M_{p}^{'} \to M_{p} \to M_{p}^{''} \to 0$ .

2.1

In that localised sequence, $M_{p} = 0$ holds exactly when both $M_{p}^{'} = 0$ and $M_{p}^{''} = 0$ : if the middle term is zero then injectivity and surjectivity from [L3] force both outer terms to be zero, while if both outer terms are zero then exactness makes the middle term zero as well.

step 1.1L3

3.1

By [L1], step 2.1 says exactly that $p$ lies in ${Supp}_{R} (M)$ if and only if it lies in ${Supp}_{R} (M^{'})$ or in ${Supp}_{R} (M^{''})$ .

L1step 2.1

4.1

Since this holds for every prime ideal $p$ , the support identity follows.

step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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