LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Constructible subsets stable under generalisation are open in an affine spectrum

Statement

Assume the Axiom of Choice (AC). Let $A$ be a commutative ring and let $E \subseteq Spec A$ be a constructible subset (Constructible subsets of a scheme). Call $E$ stable under specialisation if every specialisation of a point of $E$ lies in $E$ , and stable under generalisation if every generalisation of a point of $E$ lies in $E$ (Specialisations, generalisations, and generic points).

If $E$ is stable under specialisation, then $E$ is closed in $Spec A$ .
If $E$ is stable under generalisation, then $E$ is open in $Spec A$ .

Both assertions are formulated for subsets of an affine spectrum; no other hypothesis is imposed on $A$ , and $A$ may be the zero ring, whose spectrum is empty.

Facts & Assumptions

Given: The data and hypotheses displayed in the Statement, with the conventions fixed there.

[F1]

For a topological space $X$ an open $U \subseteq X$ is retrocompact when $U \cap V$ is quasi-compact for every quasi-compact open $V$ , and a subset is constructible when it is a finite union of sets $U \cap (X ∖ V)$ with $U, V$ retrocompact open; the empty union is allowed. On $Spec A$ the retrocompact opens are exactly the quasi-compact opens, so a subset there is constructible exactly when it is a finite union of sets $D (f) \cap V (finitely many elements)$ (Constructible subsets of a scheme).

[F2]

For a ring $A$ the points of $Spec A$ are the prime ideals; the basic opens $D (f) = {p : f \notin p}$ form a basis of the topology; for $A = 0$ the spectrum is empty (The underlying space of an affine spectrum).

[F3]

For $T \subseteq A$ the vanishing set is $V (T) = {p : T \subseteq p}$ , and $V (T) = V ((T))$ for the ideal $(T)$ generated by $T$ (The prime spectrum and vanishing sets).

[F4]

For $f \in A$ the distinguished open $D (f) = {p : f \notin p}$ is the complement of $V ((f))$ (Principal distinguished subsets of the prime spectrum).

[F5]

A ring homomorphism $φ : A \to B$ induces the continuous contraction map $Spec B \to Spec A$ , $q \mapsto φ^{- 1} q$ (The map of affine spectra induced by a ring homomorphism).

[F6]

For an ideal $I ⊴ R$ the quotient map $R \to R / I$ induces a bijection $Spec (R / I) \to V (I)$ by contraction, with inverse sending a prime $p \supseteq I$ to $p / I$ (Prime ideals of a quotient ring are exactly the prime ideals containing the ideal).

[F7]

For $f \in R$ the localisation map $R \to R_{f}$ induces a homeomorphism from $Spec (R_{f})$ onto the distinguished open $D (f)$ (The spectrum of a principal localisation is the distinguished open D(f)).

[F8]

For $r \geq 1$ and rings $R_{1}, \dots, R_{r}$ with $R = \prod_{i} R_{i}$ the distinguished opens $D (e_{i})$ are pairwise disjoint and clopen, $Spec R = D (e_{1}) ⊔ \dots ⊔ D (e_{r})$ , and the morphism induced by the projection $π_{i} : R \to R_{i}$ is an isomorphism of locally ringed spaces from $Spec R_{i}$ onto the open subscheme $D (e_{i})$ (The spectrum of a finite product ring is the disjoint union of the factor spectra).

[F9]

A scheme is quasi-compact when its underlying topological space is quasi-compact, that is, every open cover has a finite subcover; every affine scheme is quasi-compact; a morphism $g : Z \to Y$ of schemes is quasi-compact when $g^{- 1} (V)$ is quasi-compact for every quasi-compact open $V \subseteq Y$ (Quasi-compact and quasi-separated schemes, Every affine scheme is quasi-compact, Quasi-compact and quasi-separated morphisms).

[F10]

Assume AC. For every commutative ring $A$ and every $f \in A$ the distinguished open $D (f) \subseteq Spec A$ is quasi-compact (Every distinguished open of an affine spectrum is quasi-compact).

[F11]

A point $y$ is a specialisation of $x$ when $y \in \overline{{x}}$ , and then $x$ is a generalisation of $y$ (Specialisations, generalisations, and generic points).

[F12]

Assume AC. For a quasi-compact morphism $g : Z \to Y$ of schemes the image $g (Z)$ is closed if and only if it is stable under specialisation in $Y$ (A quasi-compact image stable under specialization is closed).

[F13]

The Axiom of Choice states that every family of nonempty sets has a choice function (The Axiom of Choice).

Proof

technique · direct

1.1F1F3

By [F1] write $E = ⋃_{i = 1}^{n} (D (f_{i}) \cap V (J_{i}))$ , where $J_{i} \subseteq A$ is the ideal generated by the finitely many elements listed in the $i$ -th vanishing set of that description; note $V (J_{i})$ is the set of primes containing $J_{i}$ by [F3], and if the union is empty ( $n = 0$ ) then $E = \emptyset$ is closed and open and both assertions hold, so assume $n \geq 1$ .

1.2F4F5F6F7

For each $i$ put $B_{i} = (A / J_{i})_{f_{i}}$ and let $φ_{i} : A \to B_{i}$ be the composite homomorphism. The image of the induced map $Spec B_{i} \to Spec A$ of [F5] is exactly $D (f_{i}) \cap V (J_{i})$ : by [F6] the contraction $Spec (A / J_{i}) \to Spec A$ is a bijection onto $V (J_{i})$ , and by [F7] applied over the ring $A / J_{i}$ the localisation map $Spec B_{i} \to Spec (A / J_{i})$ is a homeomorphism onto the primes of $A / J_{i}$ not containing the image of $f_{i}$ , which under the bijection of [F6] correspond to the primes of $A$ containing $J_{i}$ and avoiding $f_{i}$ .

1.3F2F9F10

The morphism $Spec B \to Spec A$ is quasi-compact: if $U \subseteq Spec A$ is a quasi-compact open, then by [F2] the sets $D (a)$ contained in $U$ cover $U$ , and quasi-compactness [F9] gives $U = D (a_{1}) \cup \dots \cup D (a_{r})$ for finitely many $a_{j}$ ; writing $φ : A \to B$ for the structure homomorphism, the preimage of $U$ is $D (φ (a_{1})) \cup \dots \cup D (φ (a_{r}))$ , each $D (φ (a_{j}))$ is quasi-compact by [F10], and a finite union of quasi-compact spaces is quasi-compact because an open cover of the union restricts to an open cover of each piece, for which a finite subcover exists.

1.4F11given

For assertion 2 assume that $E$ is stable under generalisation. Then $X ∖ E$ is stable under specialisation: if $x \in X ∖ E$ and $x^{'} \in \overline{{x}}$ , then $x^{'}$ is a specialisation of $x$ by [F11], and $x^{'} \in E$ would make the generalisation $x$ of $x^{'}$ a point of $E$ by stability under generalisation, a contradiction; hence $x^{'} \in X ∖ E$ .

1.5F1

The complement $X ∖ E$ is constructible. Indeed, by [F1] retrocompact opens are closed under finite intersections, since $U \cap V \cap W = U \cap (V \cap W)$ with $V \cap W$ quasi-compact for retrocompact $U, V$ and quasi-compact open $W$ , and under finite unions, since $(U \cup V) \cap W = (U \cap W) \cup (V \cap W)$ is a union of two quasi-compact spaces; also $X$ itself is retrocompact, as $X \cap W = W$ . Hence for a piece $P = U \cap (X ∖ V)$ the complement is $X ∖ P = (X ∖ U) \cup V = (V \cap (X ∖ U)) \cup (X \cap (X ∖ (U \cup V))) \cup ((U \cap V) \cap (X ∖ \emptyset))$ , a union of three pieces of the same form: the first covers $V ∖ U$ , the second $X ∖ (U \cup V)$ , and the third $U \cap V$ . The intersection of two pieces is $(U \cap (X ∖ V)) \cap (U^{'} \cap (X ∖ V^{'})) = (U \cap U^{'}) \cap (X ∖ (V \cup V^{'}))$ , again a piece. Therefore finite unions of pieces are closed under finite unions, finite intersections and complements, by distributivity and De Morgan, so the complement of the constructible set $E$ is a finite union of pieces, hence constructible.

2.1F5F8step 1.2

Put $B = \prod_{i = 1}^{n} B_{i}$ . By [F8] the spectrum $Spec B$ is the disjoint union of the clopen pieces $D (e_{i}) ≅ Spec B_{i}$ , and under these identifications the map $Spec B \to Spec A$ induced by the homomorphism $A \to B$ , $a \mapsto (φ_{i} (a))_{i}$ , restricts on the $i$ -th piece to the map $Spec B_{i} \to Spec A$ of step 1.2; since the image of a disjoint union is the union of the images of its pieces, step 1.2 gives $im (Spec B \to Spec A) = E$ .

3.1F12step 2.1step 1.3

Assume now that $E$ is stable under specialisation in the sense of the Statement. By steps 2.1 and 1.3 the set $E$ is the image of the quasi-compact morphism $Spec B \to Spec A$ , so assertion (1) of [F12] gives that $E$ is closed; this proves assertion 1.

4.1

Apply assertion (1), proved in step 3.1, to the constructible subset $X ∖ E$ of $Spec A$ : it is stable under specialisation by step 1.4, hence closed, so $E$ is open, proving assertion 2. The case $n = 0$ of step 1.1 covers $E = \emptyset$ , and $E = X$ is handled by the same argument with the empty constructible complement; the Axiom of Choice is assumed in the Statement and used exactly through [F10] and [F12], both of which declare it, while all remaining steps are choice-free. [F13, step 1.1, step 3.1, step 1.4, step 1.5] $□$

Depends on

Used by

Flat finite-presentation morphisms are open Theorem

Dependency tree · two levels

61 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

The Stacks Project, Topology, Lemma 5.23.6 (tag 0903) and Section 5.19 (tags 0062, 0065) (standard reference, not scraped)
The Stacks Project, Commutative Algebra, Section 10.41 (tags 00HY, 00I0, 00I1) (standard reference, not scraped)