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

Proper morphisms are closed

Statement

Let $f : X \to S$ be a proper morphism of schemes. Then $f$ is a closed map of topological spaces: for every closed subset $Z \subseteq ∣ X ∣$ its image $f (Z)$ is closed in $∣ S ∣$ . In particular $f (X)$ is closed. Moreover, for every $S$ -scheme $T$ the base-changed projection $f_{T} : X \times_{S} T ⟶ T$ is closed, so the image of $X \times_{S} T$ , and of any closed subset of it, is closed in $∣ T ∣$ .

Facts & Assumptions

Given: A proper morphism $f : X \to S$ and an arbitrary morphism $T \to S$ .

[F1]

A morphism of schemes $f : X \to S$ is proper if and only if it is separated, of finite type, and universally closed. (Proper morphisms)

[F2]

A morphism $f : X \to S$ is universally closed if for every $S$ -scheme $T$ the base-changed projection $f_{T} : X \times_{S} T \to T$ is a closed map, and explicitly, for every closed subset $Z \subseteq ∣ X_{T} ∣$ , its image $f_{T} (∣ Z ∣)$ is closed in $∣ T ∣$ . (Universally closed morphisms)

[F3]

For an $S$ -scheme $f : X \to S$ and a morphism $h : S^{'} \to S$ , the base change is $X_{S^{'}} = X \times_{S} S^{'}$ , with structure map the second projection. (Base change of objects, morphisms and properties)

[F4]

A fibre product of $X \to S \leftarrow Y$ is a scheme $P$ with projections $p : P \to X$ and $q : P \to Y$ such that for every morphism $a : T \to X$ and $b : T \to Y$ with $f a = g b$ there is exactly one $h : T \to P$ satisfying $p h = a$ and $q h = b$ . (Fibre product of schemes)

Proof

technique · direct: closedness is universal closedness read at the identity base change

1.1F1

Since $f$ is proper, [F1] makes it universally closed, and in particular of finite type; only universal closedness is used below.

1.2F2F3F4

Take the $S$ -scheme $T = S$ , with structure morphism the identity, so that [F3] identifies the base-changed projection with $q : X \times_{S} S \to S$ . By [F2] this $q$ is a closed map. The universal property [F4] applies to $f : X \to S$ and the identity $g = {id}_{S}$ with test morphisms $a = {id}_{X}$ and $b = f$ : the required identity $f \circ a = {id}_{S} \circ f$ holds, so there is a unique $u : X \to X \times_{S} S$ with $p \circ u = {id}_{X}$ and $q \circ u = f$ . The same universal property applied to $p$ and $q$ in place of $a$ and $b$ shows that $u \circ p$ and ${id}_{X \times_{S} S}$ have the same composites with $p$ and $q$ , hence $u \circ p$ is the identity and $u$ is an isomorphism. Therefore $f = q \circ u$ is closed, so the image of every closed $Z \subseteq ∣ X ∣$ is closed in $∣ S ∣$ ; taking $Z = ∣ X ∣$ gives that $f (X)$ is closed.

1.3F2F3

Now let $T \to S$ be any $S$ -scheme. By [F2] the projection $f_{T} : X \times_{S} T \to T$ is closed, which by [F3] is exactly the assertion that the base change of $f$ along $T \to S$ maps closed subsets of $X \times_{S} T$ to closed subsets of $∣ T ∣$ . In particular the image of the closed subset $X \times_{S} T$ itself is closed in $∣ T ∣$ , and the same holds for every closed subset.

If $X$ is empty, then every image is empty and closed, and if $S$ is empty the identity base-change case of step 1.2 is the empty morphism; both are covered by the same argument. No step uses a choice principle, a Noetherian hypothesis, or a separatedness hypothesis beyond the one hidden in properness. ∎

Depends on

Used by

Dependency tree · two levels

9 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, Morphisms of Schemes, Definition 29.42.1 (tag 01W0) and Section 29.41 (standard reference, not scraped)
Vakil, The Rising Sea, Proposition 11.3.2 and the discussion of properness in §11.3 (standard reference, not scraped)