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 : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

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

• diagonalQuasiCompact : AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)

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

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

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

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

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

instance AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceαTopologicalSpaceCarrierCommRingCat : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.QuasiSeparated fun (X x : AlgebraicGeometry.Scheme) (x_1 : X ⟶ x) (x : AlgebraicGeometry.IsAffine x) => QuasiSeparatedSpace ↑↑X.toPresheafedSpace

@[instance 900]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : AlgebraicGeometry.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.restrictOpenCommRingCat y (X.basicOpen f) ⋯ = TopCat.Presheaf.restrictOpenCommRingCat f (X.basicOpen f) ⋯ ^ n * x

theorem AlgebraicGeometry.is_localization_basicOpen_of_qcqs {X : AlgebraicGeometry.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.

theorem AlgebraicGeometry.exists_of_res_eq_of_qcqs {X : AlgebraicGeometry.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.restrictOpenCommRingCat f (X.basicOpen s) ⋯ = TopCat.Presheaf.restrictOpenCommRingCat g (X.basicOpen s) ⋯) : ∃ (n : ℕ), s ^ n * f = s ^ n * g

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

theorem AlgebraicGeometry.exists_of_res_zero_of_qcqs {X : AlgebraicGeometry.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.restrictOpenCommRingCat f (X.basicOpen s) ⋯ = 0) : ∃ (n : ℕ), s ^ n * f = 0

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

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