Quasi-separated morphisms #
A morphism of schemes
f : X ⟶ Y is quasi-separated if the diagonal morphism
X ⟶ X ×[Y] X is
A scheme is quasi-separated if the intersections of any two affine open sets is quasi-compact.
We show that a morphism is quasi-separated if the preimage of every affine open is quasi-separated.
We also show that this property is local at the target, and is stable under compositions and base-changes.
Main result #
- diagonal_quasi_compact : algebraic_geometry.quasi_compact (category_theory.limits.pullback.diagonal f)
A morphism is
quasi_separated if diagonal map is quasi-compact.
Instances of this typeclass
affine_target_morphism_property corresponding to
quasi_separated, asserting that the
domain is a quasi-separated scheme.
U is qcqs, then
Γ(X, D(f)) ≃ Γ(X, U)_f for every
f : Γ(X, U).
This is known as the Qcqs lemma in R. Vakil, The rising sea.