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

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

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

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.

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

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)

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, ∃ 𝒰 x, ∀ (i : 𝒰.J), QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∀ (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [inst : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (i : 𝒰.J), QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.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, ∃ 𝒰 x 𝒰' x, ∀ (i : 𝒰.J) (j k : (𝒰' i).J), CompactSpace ↑↑(CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) j) (AlgebraicGeometry.Scheme.OpenCover.map (𝒰' i) 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, ∃ 𝒰, ∀ (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, ∃ ι U x, ∀ (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 (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)] (f : X ⟶ Y) : AlgebraicGeometry.QuasiSeparated f ↔ ∀ (i : 𝒰.J), QuasiSeparatedSpace ↑↑(CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.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

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

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)

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

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 (AlgebraicGeometry.Scheme.basicOpen X f)))) : ∃ n y, TopCat.Presheaf.restrictOpen y (AlgebraicGeometry.Scheme.basicOpen X f) = TopCat.Presheaf.restrictOpen f (AlgebraicGeometry.Scheme.basicOpen X f) ^ n * x

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 (AlgebraicGeometry.Scheme.basicOpen X f)))} (h₁ : ↑S ≤ U₁) (h₂ : ↑S ≤ U₂) (e₁ : ↑(X.presheaf.map (CategoryTheory.homOfLE (_ : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₁ ≤ U₁ ⊔ U₂)).op) f) ≤ U₁)).op) y₁ = ↑(X.presheaf.map (CategoryTheory.homOfLE (_ : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₁ ≤ U₁ ⊔ U₂)).op) f) ≤ U₁)).op) (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₁ ≤ U₁ ⊔ U₂)).op) f) ^ n₁ * ↑(X.presheaf.map (CategoryTheory.homOfLE (_ : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₁ ≤ U₁ ⊔ U₂)).op) f) ≤ AlgebraicGeometry.Scheme.basicOpen X f)).op) x) (e₂ : ↑(X.presheaf.map (CategoryTheory.homOfLE (_ : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₂ ≤ U₁ ⊔ U₂)).op) f) ≤ U₂)).op) y₂ = ↑(X.presheaf.map (CategoryTheory.homOfLE (_ : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₂ ≤ U₁ ⊔ U₂)).op) f) ≤ U₂)).op) (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₂ ≤ U₁ ⊔ U₂)).op) f) ^ n₂ * ↑(X.presheaf.map (CategoryTheory.homOfLE (_ : AlgebraicGeometry.Scheme.basicOpen X (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₂ ≤ U₁ ⊔ U₂)).op) f) ≤ AlgebraicGeometry.Scheme.basicOpen X f)).op) x) : ∃ n, ↑(X.presheaf.map (CategoryTheory.homOfLE h₁).op) (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₁ ≤ U₁ ⊔ U₂)).op) f ^ (n + n₂) * y₁) = ↑(X.presheaf.map (CategoryTheory.homOfLE h₂).op) (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₂ ≤ U₁ ⊔ U₂)).op) f ^ (n + n₁) * y₂)

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 (AlgebraicGeometry.Scheme.basicOpen X f)))) : ∃ n y, TopCat.Presheaf.restrictOpen y (AlgebraicGeometry.Scheme.basicOpen X f) = TopCat.Presheaf.restrictOpen f (AlgebraicGeometry.Scheme.basicOpen X 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 (AlgebraicGeometry.Scheme.basicOpen X 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].