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

• (_ : AlgebraicGeometry.QuasiSeparated f) = (_ : AlgebraicGeometry.QuasiSeparated f)

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

• (_ : AlgebraicGeometry.QuasiSeparated (CategoryTheory.CategoryStruct.comp f g)) = (_ : AlgebraicGeometry.QuasiSeparated (CategoryTheory.CategoryStruct.comp f g))

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)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (i : 𝒰.J), QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f (𝒰.map i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∀ {U : AlgebraicGeometry.Scheme} (g : U ⟶ Y) [inst : AlgebraicGeometry.IsAffine U] [inst : AlgebraicGeometry.IsOpenImmersion g], QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f g).toLocallyRingedSpace.toSheafedSpace.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)).toLocallyRingedSpace.toSheafedSpace.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)).toLocallyRingedSpace.toSheafedSpace.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

• (_ : AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.fst) = (_ : AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.fst)

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

• (_ : AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd) = (_ : AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd)

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

• (_ : AlgebraicGeometry.QuasiSeparated (CategoryTheory.CategoryStruct.comp f g)) = (_ : AlgebraicGeometry.QuasiSeparated (CategoryTheory.CategoryStruct.comp f g))

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

• (_ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace) = (_ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace)

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.toPrefunctor.obj (Opposite.op U))) (x : ↑(X.presheaf.toPrefunctor.obj (Opposite.op (X.basicOpen f)))) : ∃ (n : ℕ) (y : ↑(X.presheaf.toPrefunctor.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.toPrefunctor.obj (Opposite.op U₁))} {y₂ : ↑(F.toPrefunctor.obj (Opposite.op U₂))} {f : ↑(F.toPrefunctor.obj (Opposite.op (U₁ ⊔ U₂)))} {x : ↑(F.toPrefunctor.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₅ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁) U₅ ^ n₁ * TopCat.Presheaf.restrictOpen x U₅) (e₂ : TopCat.Presheaf.restrictOpen y₂ U₆ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂) U₆ ^ n₂ * TopCat.Presheaf.restrictOpen x U₆) : TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ^ n₂ * y₁) U₄) U₇ = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ^ n₁ * y₂) U₄) U₇

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.toPrefunctor.obj (Opposite.op U₁))} {y₂ : ↑(X.presheaf.toPrefunctor.obj (Opposite.op U₂))} {f : ↑(X.presheaf.toPrefunctor.obj (Opposite.op (U₁ ⊔ U₂)))} {x : ↑(X.presheaf.toPrefunctor.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 = TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ^ (m + n₁) * y₂) ↑S

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.toPrefunctor.obj (Opposite.op U))) (x : ↑(X.presheaf.toPrefunctor.obj (Opposite.op (X.basicOpen f)))) : ∃ (n : ℕ) (y : ↑(X.presheaf.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) : IsLocalization.Away f ↑(X.presheaf.toPrefunctor.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].