LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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 form a Boolean algebra

Statement

Constructible subsets are closed under finite unions, finite intersections and complements. If $C$ is constructible in $X$ and $S \subseteq X$ is any subspace, $C \cap S$ is constructible in $S$ . If $S$ is locally closed and $C$ is constructible in $S$ , then $C$ is constructible in $X$ .

Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[F1]

A subset $S$ of a classical variety $X$ is locally closed if $S = U \cap Z$ for some open $U \subseteq X$ and closed $Z \subseteq X$ . A subset is constructible if it is a finite union of locally closed subsets. The empty union is allowed, so $\emptyset$ is constructible. Work over a fixed algebraically closed field $k$ , with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Locally closed and constructible subsets).

Proof

1.1

Finite unions are built into the definition. Intersections distribute over finite unions, and $(U \cap Z) \cap (V \cap W) = (U \cap V) \cap (Z \cap W)$ is locally closed. The complement of $U \cap Z$ is $(X ∖ U) \cup (X ∖ Z)$ , a union of a closed and an open set. De Morgan then handles the complement of any finite union using the intersection result. Empty unions and intersections give $\emptyset$ and $X$ .

2.1

Restricting $U \cap Z$ to $S$ replaces its factors by an open and a closed subset of $S$ . Conversely, write $S = U_{0} \cap Z_{0}$ , and a locally closed subset of $S$ as $(S \cap U_{1}) \cap (S \cap Z_{1})$ with $U_{1}$ open and $Z_{1}$ closed in $X$ . This equals $(U_{0} \cap U_{1}) \cap (Z_{0} \cap Z_{1})$ , locally closed in $X$ . Finite unions prove extension.

F1step 1.1∎

Depends on

Locally closed and constructible subsets

Used by

Chevalley: images of constructible sets are constructible Theorem

Dependency tree · two levels

2 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

Milne §9a p.200, paragraph preceding Proposition 9.6 (standard reference, not scraped)