ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passaudited 2026-09-05

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.

An infinitely generated module can have specialization-closed support that is not Zariski closed

Example

Let $M = ⨁_{p prime} Z / p Z$ as a $Z$ -module. Then ${Supp}_{Z} (M) = {(p) : p prime},$ which is closed under specialisation but is not Zariski-closed in $Spec (Z)$ .

Facts & Assumptions

Given: The $Z$ -module $M = ⨁_{p prime} Z / p Z$ .

[L1]

Support is closed under specialisation (The support of any module is closed under specialisation).

[L2]

Support of a direct sum is the union of the supports of the summands (Support of an arbitrary direct sum is the union of the supports).

[L3]

The support of the cyclic module $Z / p Z$ is $V ((p)) = {(p)}$ (The support of a cyclic quotient is its vanishing set).

[L4]

In $Spec (Z)$ , the points are $(0)$ and the closed points $(p)$ , and for nonzero $n$ one has $D (n) = {(0)} \cup {(q) : q ∤ n}$ (The spectrum of the integers has one generic point, closed points (p), and basic opens D(n)).

[L5]

Every open neighbourhood of a point contains a distinguished-open neighbourhood of that point (Every point of a Zariski-open set has a distinguished-open neighbourhood inside it).

Verification

technique · direct

1.1

By [L2] and [L3], ${Supp}_{Z} (M) = ⋃_{p prime} {Supp}_{Z} (Z / p Z) = ⋃_{p prime} {(p)} = {(p) : p prime}$ .

L2L3

2.1

This support is closed under specialisation by [L1]: each point $(p)$ is already closed, so the only specialisation of $(p)$ is itself.

L1step 1.1

2.2

The set from step 1.1 is not Zariski-closed. Indeed, if it were closed, its complement would be an open neighborhood of the missing point $(0)$ . By [L5], that neighbourhood contains some distinguished open $D (n)$ with $(0) \in D (n)$ . Since $(0) \in D (n)$ , the integer $n$ is nonzero by [L4]. Now [L4] says that $D (n)$ also contains every closed point $(q)$ with $q ∤ n$ . Choosing such a prime $q$ , we get $(q) \in D (n)$ and $(q)$ lies in the support from step 1.1, contradicting disjointness.

L4L5step 1.1choose

3.1

Therefore $M$ has specialization-closed support that is not Zariski-closed.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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., Exercise (13.34) (standard reference, not scraped)