Documentation

Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

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 #

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

Instances
    theorem AlgebraicGeometry.quasiSeparatedSpace_iff_affine (X : AlgebraicGeometry.Scheme) :
    QuasiSeparatedSpace X.toPresheafedSpace ∀ (U V : X.affineOpens), IsCompact (U V)
    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.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₆₃) :
    theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (X : AlgebraicGeometry.Scheme) (S : X.affineOpens) (U₁ : X.Opens) (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 mTopCat.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 : 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 : 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][RisingSea].

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