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

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

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

• diagonalQuasiCompact : 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)) _auto✝

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

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 : IsAffine x) => CompactSpace ↑↑X.toPresheafedSpace) f ↔ QuasiSeparatedSpace ↑↑X.toPresheafedSpace

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 : IsAffine x) => QuasiSeparatedSpace ↑↑X.toPresheafedSpace

@[instance 900]

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

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

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

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

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

theorem AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated (X : Scheme) : QuasiSeparatedSpace ↑↑X.toPresheafedSpace ↔ 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)

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

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

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

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

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

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

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

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

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.is_localization_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.toPresheafedSpace} (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.toPresheafedSpace] [QuasiSeparatedSpace ↑↑X.toPresheafedSpace] {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.toPresheafedSpace} (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.toPresheafedSpace] [QuasiSeparatedSpace ↑↑X.toPresheafedSpace] {f s : ↑(X.presheaf.obj (Opposite.op ⊤))} (hf : TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = 0) : ∃ (n : ℕ), s ^ n * f = 0

theorem AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen {X : Scheme} [CompactSpace ↑↑X.toPresheafedSpace] [QuasiSeparatedSpace ↑↑X.toPresheafedSpace] (f : ↑(X.presheaf.obj (Opposite.op ⊤))) : CategoryTheory.IsIso ((ΓSpec.adjunction.unit.app X).c.app (Opposite.op (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].