# Quasi-separated morphisms #

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. (AlgebraicGeometry.quasiSeparatedSpace_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 #

• AlgebraicGeometry.is_localization_basicOpen_of_qcqs (Qcqs lemma): If U is qcqs, then Γ(X, D(f)) ≃ Γ(X, U)_f for every f : Γ(X, U).

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

• diagonalQuasiCompact :

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

Instances

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

theorem AlgebraicGeometry.quasiSeparatedSpace_iff_affine :
QuasiSeparatedSpace X.toPresheafedSpace ∀ (U V : X.affineOpens), IsCompact (U V)
@[instance 900]
Equations
• =
instance AlgebraicGeometry.quasiSeparatedComp (f : X Y) (g : Y Z) :
Equations
• =
Equations
• =
Equations
• =
theorem AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated (f : X Y) [hY : QuasiSeparatedSpace Y.toPresheafedSpace] :
QuasiSeparatedSpace X.toPresheafedSpace
Equations
• =
theorem AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen (U : X.Opens) (hU : ) (f : (X.presheaf.obj (Opposite.op U))) (x : (X.presheaf.obj (Opposite.op (X.basicOpen f)))) :
∃ (n : ) (y : (X.presheaf.obj (Opposite.op U))), TopCat.Presheaf.restrictOpen y (X.basicOpen f) = TopCat.Presheaf.restrictOpen f (X.basicOpen f) ^ n * x
theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux {X : TopCat} (F : ) {U₁ : } {U₂ : } {U₃ : } {U₄ : } {U₅ : } {U₆ : } {U₇ : } {n₁ : } {n₂ : } {y₁ : (F.obj (Opposite.op U₁))} {y₂ : (F.obj (Opposite.op U₂))} {f : (F.obj (Opposite.op (U₁ U₂)))} {x : (F.obj (Opposite.op U₃))} (h₄₁ : U₄ U₁) (h₄₂ : U₄ U₂) (h₅₁ : U₅ U₁) (h₅₃ : U₅ U₃) (h₆₂ : U₆ U₂) (h₆₃ : U₆ U₃) (h₇₄ : U₇ U₄) (h₇₅ : U₇ U₅) (h₇₆ : U₇ U₆) (e₁ : TopCat.Presheaf.restrictOpen y₁ U₅ h₅₁ = TopCat.Presheaf.restrictOpen U₅ h₅₁ ^ n₁ * ) (e₂ : TopCat.Presheaf.restrictOpen y₂ U₆ h₆₂ = TopCat.Presheaf.restrictOpen U₆ h₆₂ ^ n₂ * ) :
TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen ( ^ n₂ * y₁) U₄ h₄₁) U₇ h₇₄ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen ( ^ n₁ * y₂) U₄ h₄₂) U₇ h₇₄
theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (S : X.affineOpens) (U₁ : X.Opens) (U₂ : X.Opens) {n₁ : } {n₂ : } {y₁ : (X.presheaf.obj (Opposite.op U₁))} {y₂ : (X.presheaf.obj (Opposite.op U₂))} {f : (X.presheaf.obj (Opposite.op (U₁ U₂)))} {x : (X.presheaf.obj (Opposite.op (X.basicOpen f)))} (h₁ : S U₁) (h₂ : S U₂) (e₁ : TopCat.Presheaf.restrictOpen y₁ (X.basicOpen ) = TopCat.Presheaf.restrictOpen (X.basicOpen ) ^ n₁ * TopCat.Presheaf.restrictOpen x (X.basicOpen ) ) (e₂ : TopCat.Presheaf.restrictOpen y₂ (X.basicOpen ) = TopCat.Presheaf.restrictOpen (X.basicOpen ) ^ n₂ * TopCat.Presheaf.restrictOpen x (X.basicOpen ) ) :
∃ (n : ), ∀ (m : ), n mTopCat.Presheaf.restrictOpen ( ^ (m + n₂) * y₁) (↑S) h₁ = TopCat.Presheaf.restrictOpen ( ^ (m + n₁) * y₂) (↑S) h₂
theorem AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (U : X.Opens) (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier) (f : (X.presheaf.obj (Opposite.op U))) (x : (X.presheaf.obj (Opposite.op (X.basicOpen f)))) :
∃ (n : ) (y : (X.presheaf.obj (Opposite.op U))), TopCat.Presheaf.restrictOpen y (X.basicOpen f) = TopCat.Presheaf.restrictOpen f (X.basicOpen f) ^ n * x
theorem AlgebraicGeometry.is_localization_basicOpen_of_qcqs {U : X.Opens} (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier) (f : (X.presheaf.obj (Opposite.op U))) :
IsLocalization.Away f (X.presheaf.obj (Opposite.op (X.basicOpen f)))

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.

theorem AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen [CompactSpace X.toPresheafedSpace] [QuasiSeparatedSpace X.toPresheafedSpace] (f : (X.presheaf.obj )) :
CategoryTheory.IsIso ((.app X).val.c.app )

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.