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

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

class AlgebraicGeometry.QuasiSeparated {X : AlgebraicGeometry.Scheme} {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.

def AlgebraicGeometry.QuasiSeparated.affineProperty : AlgebraicGeometry.AffineTargetMorphismProperty

The AffineTargetMorphismProperty corresponding to QuasiSeparated, asserting that the domain is a quasi-separated scheme.

Equations

• AlgebraicGeometry.QuasiSeparated.affineProperty x✝ = QuasiSeparatedSpace ↑↑X.toPresheafedSpace

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

theorem AlgebraicGeometry.quasi_compact_affineProperty_iff_quasiSeparatedSpace {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y) : AlgebraicGeometry.AffineTargetMorphismProperty.diagonal AlgebraicGeometry.QuasiCompact.affineProperty f ↔ QuasiSeparatedSpace ↑↑X.toPresheafedSpace

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

theorem AlgebraicGeometry.quasi_compact_affineProperty_diagonal_eq : AlgebraicGeometry.AffineTargetMorphismProperty.diagonal AlgebraicGeometry.QuasiCompact.affineProperty = AlgebraicGeometry.QuasiSeparated.affineProperty

theorem AlgebraicGeometry.quasiSeparated_eq_affineProperty_diagonal : @AlgebraicGeometry.QuasiSeparated = AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.AffineTargetMorphismProperty.diagonal AlgebraicGeometry.QuasiCompact.affineProperty)

theorem AlgebraicGeometry.quasiSeparated_eq_affineProperty : @AlgebraicGeometry.QuasiSeparated = AlgebraicGeometry.targetAffineLocally AlgebraicGeometry.QuasiSeparated.affineProperty

theorem AlgebraicGeometry.QuasiSeparated.affineProperty_isLocal : AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal AlgebraicGeometry.QuasiSeparated.affineProperty

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.quasiSeparated_stableUnderComposition : CategoryTheory.MorphismProperty.StableUnderComposition @AlgebraicGeometry.QuasiSeparated

theorem AlgebraicGeometry.quasiSeparated_stableUnderBaseChange : CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.QuasiSeparated

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.quasiSeparated_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.QuasiSeparated

theorem AlgebraicGeometry.QuasiSeparated.affine_openCover_TFAE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : List.TFAE [AlgebraicGeometry.QuasiSeparated f, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (_ : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)), ∀ (i : 𝒰.J), QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace, ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst : AlgebraicGeometry.IsOpenImmersion g], QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f g).toPresheafedSpace, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (_ : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)) (𝒰' : (i : 𝒰.J) → AlgebraicGeometry.Scheme.OpenCover (CategoryTheory.Limits.pullback f (𝒰.map i))) (_ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)), ∀ (i : 𝒰.J) (j k : (𝒰' i).J), CompactSpace ↑↑(CategoryTheory.Limits.pullback ((𝒰' i).map j) ((𝒰' i).map k)).toPresheafedSpace]

theorem AlgebraicGeometry.QuasiSeparated.is_local_at_target : AlgebraicGeometry.PropertyIsLocalAtTarget @AlgebraicGeometry.QuasiSeparated

theorem AlgebraicGeometry.QuasiSeparated.openCover_TFAE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : List.TFAE [AlgebraicGeometry.QuasiSeparated f, ∃ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y), ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (i : 𝒰.J), AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd, ∀ (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace), AlgebraicGeometry.QuasiSeparated (f ∣_ U), ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd, ∃ (ι : Type u) (U : ι → TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) (_ : iSup U = ⊤), ∀ (i : ι), AlgebraicGeometry.QuasiSeparated (f ∣_ U i)]

theorem AlgebraicGeometry.quasiSeparated_over_affine_iff {X : AlgebraicGeometry.Scheme} {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)

theorem AlgebraicGeometry.QuasiSeparated.affine_openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (f : X ⟶ Y) : AlgebraicGeometry.QuasiSeparated f ↔ ∀ (i : 𝒰.J), QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f (𝒰.map i)).toPresheafedSpace

theorem AlgebraicGeometry.QuasiSeparated.openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) (f : X ⟶ Y) : AlgebraicGeometry.QuasiSeparated f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated {X : AlgebraicGeometry.Scheme} {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

Equations

• ⋯ = ⋯

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

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

theorem AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (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.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₁ : TopologicalSpace.Opens ↑X} {U₂ : TopologicalSpace.Opens ↑X} {U₃ : TopologicalSpace.Opens ↑X} {U₄ : TopologicalSpace.Opens ↑X} {U₅ : TopologicalSpace.Opens ↑X} {U₆ : TopologicalSpace.Opens ↑X} {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 : AlgebraicGeometry.Scheme) (S : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (U₁ : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (U₂ : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) {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 : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (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 : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (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].