---
tag: TGN01264C4
kind: statement
role: theorem
name: Chevalley's theorem on constructible sets
msc: [14A15]
uses: [JXRKH6P1Z4, ND6XEY68P4, AHTE5DVX61, 8SQK7RTB63]
about: [AHTE5DVX61]
sources:
  - url: https://en.wikipedia.org/wiki/Constructible_set_(topology)
---

## Statement

Let $Y$ be a [[Noetherian scheme|ND6XEY68P4]] and let $f \colon X \to Y$ be a [[morphism|JXRKH6P1Z4]] [[of finite type|AHTE5DVX61]].
A subset of a Noetherian scheme is *constructible* if it is a finite union of sets $U \cap Z$.
Here each $U$ is open and each $Z$ is closed in the [[Zariski topology|8SQK7RTB63]].
Then $f(C)$ is a constructible subset of $Y$ for every constructible subset $C$ of $X$.
In particular, the image $f(X)$ is constructible.

## Remarks

The proof reduces to the case where $Y = \operatorname{Spec} A$ is affine and integral and $X$ is affine.
The key step shows that if $f(X)$ is dense in $Y$, then $f(X)$ contains a nonempty open subset of $Y$.
This follows from generic freeness or from Noether normalization over the fraction field of $A$.
Noetherian induction on the closed complement then finishes the proof.
For example, over a field $k$, the morphism $\mathbb{A}^2_k \to \mathbb{A}^2_k$ given by $(x, y) \mapsto (x, xy)$ has image $\set{u \ne 0} \cup \set{(0, 0)}$.
This image is constructible but neither open nor closed, so constructible sets are the right class for images.
Without the finite type hypothesis the image can fail to be constructible.
For instance, $\operatorname{Spec} \Q \to \operatorname{Spec} \Z$ has image the generic point alone, which is not constructible.

## Explanations

### L1 human

The image of an algebraic map need not be open or closed.
Chevalley's theorem says that it is never much worse than that.
It is always built from finitely many pieces, each the part of a closed set that lies in an open set.
In the language of logic, the projection of a set defined by polynomial equations and inequations is again of that form.

### L2 human

Over an algebraically closed field, the theorem is the geometric form of quantifier elimination for algebraically closed fields.
It is used to show that properties of the fibres of a morphism hold on constructible sets of the base.
Together with generic flatness, it gives the usual stratifications of the base of a family into finitely many pieces over which the family is well behaved.
A general version holds for morphisms of finite presentation between arbitrary schemes, with a suitable definition of constructible sets.