TheoremStatement: 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.

Chevalley: images of constructible sets are constructible

Statement

Every morphism $f : X \to Y$ of classical varieties sends every constructible subset of $X$ to a constructible subset of $Y$ . In particular $f (X)$ 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.

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).

[F2]

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. (Constructible subsets form a Boolean algebra).

[F4]

The image of a dominant morphism $f : X \to Y$ between irreducible affine varieties contains a nonempty principal open subset of $Y$ . 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. (Dominant affine images contain a principal open).

[F5]

Every classical variety is Noetherian and has finitely many irreducible components. Every open or closed subvariety has a finite affine cover. 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. (Classical varieties have finite irreducible decompositions).

Proof

1.1

First prove, for fixed $f$ , that the image of every closed subvariety $T \subseteq X$ is constructible, by Noetherian induction on $T$ . The empty case has empty image. If $T$ is reducible, its finitely many proper irreducible components have constructible images by the induction hypothesis and their finite union is constructible. It remains to treat nonempty irreducible $T$ , assuming the result on its proper closed subsets.

F2F5

1.2

Put $Z = \overline{f (T)}$ , an irreducible closed subvariety, since a continuous image and its closure preserve irreducibility. Choose a nonempty affine chart $V \subseteq Z$ and a nonempty affine chart $W \subseteq T \cap f^{- 1} (V)$ . The restriction $W \to V$ is dominant: every nonempty target open has nonempty open inverse image in irreducible $T$ , which meets $W$ . The affine image lemma gives a nonempty open $O \subseteq V$ contained in $f (W)$ , hence in $f (T)$ . It is open in $Z$ and locally closed in $Y$ .

2.1

The subset $T_{0} = T ∖ f^{- 1} (O)$ is proper closed in $T$ , because $f$ factors through $Z$ and $O$ is open in $Z$ . Its image is constructible by induction. Thus $f (T) = O \cup f (T_{0})$ is constructible. Noetherianity validates the induction: a failure would have an inclusion-minimal closed counterexample, contradicted by these reductions.

F2F5step 1.1step 1.2

3.1

For a constructible $C \subseteq X$ , write it as a finite union of locally closed subsets $S_{j}$ . Each $S_{j}$ is itself a classical variety with a finite affine cover. Apply the result just proved to the whole source $S_{j}$ for the morphism $f ∣_{S_{j}} : S_{j} \to Y$ . Then $f (C) = ⋃_{j} f (S_{j})$ is constructible. This includes $C = \emptyset$ and $C = X$ .

F1F2F5step 2.1∎

Depends on

Used by

A dominant image contains a dense open Corollary

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

Milne Theorem 9.7 (standard reference, not scraped)