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.isLocalization_basicOpen_of_qcqs (Qcqs lemma): If U is qcqs, then Γ(X, D(f)) ≃ Γ(X, U)_f for every f : Γ(X, U).

class AlgebraicGeometry.QuasiSeparated {X Y : Scheme} (f : X ⟶ Y) : Prop

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

• quasiCompact_diagonal : QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)

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

theorem AlgebraicGeometry.quasiSeparated_iff {X Y : Scheme} (f : X ⟶ Y) : QuasiSeparated f ↔ autoParam (QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)) QuasiSeparated.quasiCompact_diagonal._autoParam

@[deprecated AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal (since := "2025-10-15")]

theorem AlgebraicGeometry.QuasiSeparated.diagonalQuasiCompact {X Y : Scheme} {f : X ⟶ Y} [self : QuasiSeparated f] : QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)

Alias of AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal.

---

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

theorem AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens {X : Scheme} : QuasiSeparatedSpace ↥X ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

@[deprecated AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens (since := "2025-10-15")]

theorem AlgebraicGeometry.quasiSeparatedSpace_iff_affine {X : Scheme} : QuasiSeparatedSpace ↥X ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Alias of AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens.

theorem AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) : AffineTargetMorphismProperty.diagonal (fun (X x : Scheme) (x_1 : X ⟶ x) (x_2 : IsAffine x) => CompactSpace ↥X) f ↔ QuasiSeparatedSpace ↥X

theorem AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact : @QuasiSeparated = CategoryTheory.MorphismProperty.diagonal @QuasiCompact

instance AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat : HasAffineProperty @QuasiSeparated fun (X x : Scheme) (x_1 : X ⟶ x) (x_2 : IsAffine x) => QuasiSeparatedSpace ↥X

@[instance 900]

instance AlgebraicGeometry.instQuasiSeparatedOfMonoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.Mono f] : QuasiSeparated f

instance AlgebraicGeometry.quasiSeparated_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @QuasiSeparated

instance AlgebraicGeometry.instIsMultiplicativeSchemeQuasiSeparated : CategoryTheory.MorphismProperty.IsMultiplicative @QuasiSeparated

instance AlgebraicGeometry.quasiSeparated_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @QuasiSeparated

instance AlgebraicGeometry.quasiSeparated_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated f] [QuasiSeparated g] : QuasiSeparated (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated (X : Scheme) : QuasiSeparatedSpace ↥X ↔ QuasiSeparated (CategoryTheory.Limits.terminal.from X)

instance AlgebraicGeometry.instQuasiSeparatedFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiSeparated g] : QuasiSeparated (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instQuasiSeparatedSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [QuasiSeparated f] : QuasiSeparated (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.instQuasiSeparatedMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [QuasiSeparated f] : QuasiSeparated (f ∣_ V)

instance AlgebraicGeometry.instQuasiSeparatedResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [QuasiSeparated f] : QuasiSeparated (Scheme.Hom.resLE f V U e)

theorem AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated {X Y : Scheme} (f : X ⟶ Y) [hY : QuasiSeparatedSpace ↥Y] [QuasiSeparated f] : QuasiSeparatedSpace ↥X

theorem AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparated f] {U : Y.Opens} (hU : IsQuasiSeparated ↑U) : IsQuasiSeparated ↑((TopologicalSpace.Opens.map f.base).obj U)

instance AlgebraicGeometry.quasiSeparatedSpace_of_isAffine (X : Scheme) [IsAffine X] : QuasiSeparatedSpace ↥X

theorem AlgebraicGeometry.IsAffineOpen.isQuasiSeparated {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) : IsQuasiSeparated ↑U

instance AlgebraicGeometry.instQuasiSeparatedToSpecΓOfQuasiSeparatedSpaceCarrierCarrierCommRingCat {X : Scheme} [QuasiSeparatedSpace ↥X] : QuasiSeparated X.toSpecΓ

theorem AlgebraicGeometry.Scheme.quasiSeparatedSpace_of_isOpenCover {X : Scheme} {I : Type u_1} (U : I → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (hU₁ : ∀ (i : I), IsAffineOpen (U i)) (hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))) : QuasiSeparatedSpace ↥X

theorem AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift {X : Scheme} : QuasiSeparatedSpace ↥X ↔ QuasiCompact (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))

instance AlgebraicGeometry.instQuasiCompactLiftSchemeIdOfQuasiSeparatedSpaceCarrierCarrierCommRingCat {X : Scheme} [QuasiSeparatedSpace ↥X] : QuasiCompact (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))

instance AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat {X Y : Scheme} [QuasiSeparatedSpace ↥Y] (f g : X ⟶ Y) : QuasiCompact (CategoryTheory.Limits.equalizer.ι f g)

instance AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace {X Y : Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥Y] (f g : X ⟶ Y) : CompactSpace ↥(CategoryTheory.Limits.equalizer f g)

theorem AlgebraicGeometry.QuasiSeparated.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated (CategoryTheory.CategoryStruct.comp f g)] : QuasiSeparated f

@[instance 100]

instance AlgebraicGeometry.QuasiSeparated.of_quasiSeparatedSpace {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥X] : QuasiSeparated f

theorem AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥Y] : QuasiSeparated f ↔ QuasiSeparatedSpace ↥X

@[deprecated AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace (since := "2025-10-15")]

theorem AlgebraicGeometry.quasiSeparated_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥Y] : QuasiSeparated f ↔ QuasiSeparatedSpace ↥X

Alias of AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace.

instance AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiSeparatedTopMorphismProperty : CategoryTheory.MorphismProperty.HasOfPostcompProperty @QuasiSeparated ⊤

instance AlgebraicGeometry.instHasOfPostcompPropertySchemeQuasiCompactQuasiSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @QuasiCompact @QuasiSeparated

theorem AlgebraicGeometry.QuasiCompact.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiCompact (CategoryTheory.CategoryStruct.comp f g)] [QuasiSeparated g] : QuasiCompact f

@[instance 100]

instance AlgebraicGeometry.quasiCompact_of_compactSpace {X Y : Scheme} (f : X ⟶ Y) [CompactSpace ↥X] [QuasiSeparatedSpace ↥Y] : QuasiCompact f

theorem AlgebraicGeometry.quasiCompact_iff_compactSpace {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥Y] [CompactSpace ↥Y] : QuasiCompact f ↔ CompactSpace ↥X

@[deprecated AlgebraicGeometry.quasiCompact_iff_compactSpace (since := "2025-10-15")]

theorem AlgebraicGeometry.quasiCompact_over_affine_iff {X Y : Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥Y] [CompactSpace ↥Y] : QuasiCompact f ↔ CompactSpace ↥X

Alias of AlgebraicGeometry.quasiCompact_iff_compactSpace.

theorem AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen (X : Scheme) (U : X.Opens) (hU : IsAffineOpen U) (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 : TopCat.Presheaf CommRingCat X) {U₁ U₂ U₃ U₄ U₅ U₆ U₇ : TopologicalSpace.Opens ↑X} {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 (TopCat.Presheaf.restrictOpen f U₁ ⋯) U₅ h₅₁ ^ n₁ * TopCat.Presheaf.restrictOpen x U₅ h₅₃) (e₂ : TopCat.Presheaf.restrictOpen y₂ U₆ h₆₂ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯) U₆ h₆₂ ^ n₂ * TopCat.Presheaf.restrictOpen x U₆ h₆₃) : TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯ ^ n₂ * y₁) U₄ h₄₁) U₇ h₇₄ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯ ^ n₁ * y₂) U₄ h₄₂) U₇ h₇₄

theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (X : Scheme) (S : ↑X.affineOpens) (U₁ 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 f U₁ ⋯)) ⋯ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯) (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯ ^ n₁ * TopCat.Presheaf.restrictOpen x (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯) (e₂ : TopCat.Presheaf.restrictOpen y₂ (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯) (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ ^ n₂ * TopCat.Presheaf.restrictOpen x (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯ ^ (m + n₂) * y₁) (↑S) h₁ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯ ^ (m + n₁) * y₂) (↑S) h₂

theorem AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme) (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.isLocalization_basicOpen_of_qcqs {X : Scheme} {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][RisingSea].

theorem AlgebraicGeometry.exists_of_res_eq_of_qcqs {X : Scheme} {U : TopologicalSpace.Opens ↥X} (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier) {f g s : ↑(X.presheaf.obj (Opposite.op U))} (hfg : TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = TopCat.Presheaf.restrictOpen g (X.basicOpen s) ⋯) : ∃ (n : ℕ), s ^ n * f = s ^ n * g

theorem AlgebraicGeometry.exists_of_res_eq_of_qcqs_of_top {X : Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥X] {f g s : ↑(X.presheaf.obj (Opposite.op ⊤))} (hfg : TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = TopCat.Presheaf.restrictOpen g (X.basicOpen s) ⋯) : ∃ (n : ℕ), s ^ n * f = s ^ n * g

theorem AlgebraicGeometry.exists_of_res_zero_of_qcqs {X : Scheme} {U : TopologicalSpace.Opens ↥X} (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier) {f s : ↑(X.presheaf.obj (Opposite.op U))} (hf : TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = 0) : ∃ (n : ℕ), s ^ n * f = 0

theorem AlgebraicGeometry.exists_of_res_zero_of_qcqs_of_top {X : Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥X] {f s : ↑(X.presheaf.obj (Opposite.op ⊤))} (hf : TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = 0) : ∃ (n : ℕ), s ^ n * f = 0

instance AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen {X : Scheme} [CompactSpace ↥X] [QuasiSeparatedSpace ↥X] (f : ↑(X.presheaf.obj (Opposite.op ⊤))) : CategoryTheory.IsIso (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.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][RisingSea].