# mathlib3documentation

algebraic_geometry.morphisms.quasi_separated

# Quasi-separated morphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A morphism of schemes f : X ⟶ Y is quasi-separated if the diagonal morphism X ⟶ X ×[Y] X is quasi-compact.

A scheme is quasi-separated if the intersections of any two affine open sets is quasi-compact. (algebraic_geometry.quasi_separated_space_iff_affine)

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 #

• is_localization_basic_open_of_qcqs (Qcqs lemma): If U is qcqs, then Γ(X, D(f)) ≃ Γ(X, U)_f for every f : Γ(X, U).
@[class]
• diagonal_quasi_compact :

A morphism is quasi_separated if diagonal map is quasi-compact.

Instances of this typeclass

The affine_target_morphism_property corresponding to quasi_separated, asserting that the domain is a quasi-separated scheme.

Equations
@[protected, instance]
@[protected, instance]
theorem algebraic_geometry.quasi_separated.affine_open_cover_tfae {X Y : algebraic_geometry.Scheme} (f : X Y) :
[, (𝒰 : Y.open_cover) [_inst_1 : (i : 𝒰.J), , , (𝒰 : Y.open_cover) [_inst_2 : (i : 𝒰.J), (i : 𝒰.J), , {U : algebraic_geometry.Scheme} (g : U Y) [_inst_3 : [_inst_4 : , , (𝒰 : Y.open_cover) [_inst_5 : (i : 𝒰.J), (𝒰' : Π (i : 𝒰.J), (𝒰.map i)).open_cover) [_inst_6 : (i : 𝒰.J) (j : (𝒰' i).J), algebraic_geometry.is_affine ((𝒰' i).obj j)], (i : 𝒰.J) (j k : (𝒰' i).J), compact_space ((category_theory.limits.pullback ((𝒰' i).map j) ((𝒰' i).map k)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)].tfae
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem algebraic_geometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (S : (X.affine_opens)) {n₁ n₂ : } {y₁ : } {y₂ : } {f : } {x : } (h₁ : S.val U₁) (h₂ : S.val U₂)  :

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