DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 2026-09-27

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.

Separated morphism of schemes

Definition

Let $f : X \to S$ be a morphism of schemes and let $Δ_{X / S} : X \to X \times_{S} X$ be its diagonal morphism (The diagonal morphism).

$f$ is separated if $Δ_{X / S}$ is a closed immersion (Closed immersions of schemes).
$f$ is quasi-separated if $Δ_{X / S}$ is a quasi-compact morphism (Quasi-compact and quasi-separated morphisms).

A scheme $Y$ is called separated, respectively quasi-separated, when the structure morphism $Y \to Spec Z$ is separated, respectively quasi-separated. The affine-intersection condition recorded under Quasi-compact and quasi-separated morphisms is the earlier definition; its equivalence to quasi-compactness of $Δ_{X / S}$ is proved in Quasi-separatedness and the diagonal on this page. Both properties are properties of the morphism $f$ and of its diagonal, and neither is a condition on the point-set topology of $X$ alone.

Depends on

Used by

A nonseparated affine cover can have nonaffine intersection Counterexample
Curves over a field Definition
Neron models, the Neron mapping property and weak Neron models Definition
Proper morphisms Definition
Rational maps of integral finite-type schemes Definition
Separated S-scheme Definition
Split augmented simplicial schemes and matching objects Definition
Valuative uniqueness diagram Definition
The empty morphism is finite, proper and projective Example
Affine morphisms are separated Lemma
An affine open in a smooth integral variety has Cartier boundary Lemma
An S-rational map defined after a faithfully flat smooth base change is defined Lemma
Chow lemma for proper Noetherian schemes Lemma
Closed gluing of two projective three-spaces is proper Lemma
Closed graphs over separated targets Lemma
Composite of a finite morphism and a proper morphism is proper Lemma
Effective fppf descent for separated locally quasi-finite morphisms Lemma
Finite projective complex for proper flat coherent cohomology Lemma
Finite-stage descent of properness for finitely presented schemes Lemma
Fpqc descent of properness components Lemma
Global sections commute with extension of scalars over a field Lemma
Higher direct images localize over an affine base Lemma
Large ample twists of a line bundle are very ample Lemma
Modification preserves open cohomology images Lemma
Monomorphisms and diagonals Lemma
Morphisms from a proper scheme to a separated one are proper Lemma
Open and closed immersions are separated Lemma
Properness is local on the target Lemma
Properness survives arbitrary base change Lemma
Properness survives composition Lemma
Pushforward and vanishing for an affine point blowup Lemma
Rational maps from a smooth curve to a proper scheme are morphisms Lemma
Rigidity for a proper geometrically integral factor Lemma
Schematic closure and agreement on a dense open Lemma
Separated minimal union and translations Lemma
Separated morphisms compose Lemma
Separatedness implies valuative uniqueness Lemma
Separatedness is local on the base Lemma
Separatedness survives base change Lemma
Smooth projective analytifications have rational Kähler forms Lemma

…and 20 more results.

Dependency tree · two levels

13 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, Schemes, Definition 26.21.3 (tag 01KK), printed p.40 (standard reference, not scraped)