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.isLocalization_basicOpen_of_qcqs(Qcqs lemma): IfUis qcqs, thenΓ(X, D(f)) ≃ Γ(X, U)_ffor everyf : Γ(X, U).
A morphism is QuasiSeparated if diagonal map is quasi-compact.
- diagonalQuasiCompact : QuasiCompact (CategoryTheory.Limits.pullback.diagonal f)
A morphism is
QuasiSeparatedif diagonal map is quasi-compact.
Instances
theorem
AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace
{X Y : Scheme}
[IsAffine Y]
(f : X ⟶ Y)
:
AffineTargetMorphismProperty.diagonal
(fun (X x : Scheme) (x_1 : X ⟶ x) (x : IsAffine x) => CompactSpace ↑↑X.toPresheafedSpace) f ↔ QuasiSeparatedSpace ↑↑X.toPresheafedSpace
instance
AlgebraicGeometry.instHasAffinePropertyQuasiSeparatedQuasiSeparatedSpaceCarrierCarrierCommRingCat :
HasAffineProperty @QuasiSeparated fun (X x : Scheme) (x_1 : X ⟶ x) (x : IsAffine x) =>
QuasiSeparatedSpace ↑↑X.toPresheafedSpace
@[instance 900]
instance
AlgebraicGeometry.quasiSeparatedOfMono
{X Y : Scheme}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
instance
AlgebraicGeometry.quasiSeparatedComp
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[QuasiSeparated f]
[QuasiSeparated g]
:
instance
AlgebraicGeometry.instQuasiSeparatedFstScheme
{X Y S : Scheme}
(f : X ⟶ S)
(g : Y ⟶ S)
[QuasiSeparated g]
:
instance
AlgebraicGeometry.instQuasiSeparatedSndScheme
{X Y S : Scheme}
(f : X ⟶ S)
(g : Y ⟶ S)
[QuasiSeparated f]
:
theorem
AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated
{X Y : Scheme}
(f : X ⟶ Y)
[hY : QuasiSeparatedSpace ↑↑Y.toPresheafedSpace]
[QuasiSeparated f]
:
theorem
AlgebraicGeometry.IsAffineOpen.isQuasiSeparated
{X : Scheme}
{U : X.Opens}
(hU : IsAffineOpen U)
:
instance
AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat
{X Y : Scheme}
[QuasiSeparatedSpace ↑↑Y.toPresheafedSpace]
(f g : X ⟶ Y)
:
instance
AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace
{X Y : Scheme}
[CompactSpace ↑↑X.toPresheafedSpace]
[QuasiSeparatedSpace ↑↑Y.toPresheafedSpace]
(f g : X ⟶ Y)
:
theorem
AlgebraicGeometry.QuasiSeparated.of_comp
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[QuasiSeparated (CategoryTheory.CategoryStruct.comp f g)]
:
theorem
AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen
(X : Scheme)
(U : X.Opens)
(hU : 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₁ 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.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 : 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.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 : 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.isLocalization_basicOpen_of_qcqs
{X : 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.
@[deprecated AlgebraicGeometry.isLocalization_basicOpen_of_qcqs (since := "2025-03-01")]
theorem
AlgebraicGeometry.is_localization_basicOpen_of_qcqs
{X : 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)))
Alias of AlgebraicGeometry.isLocalization_basicOpen_of_qcqs.
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 : 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.restrictOpen f (X.basicOpen s) ⋯ = TopCat.Presheaf.restrictOpen g (X.basicOpen s) ⋯)
:
theorem
AlgebraicGeometry.exists_of_res_eq_of_qcqs_of_top
{X : Scheme}
[CompactSpace ↑↑X.toPresheafedSpace]
[QuasiSeparatedSpace ↑↑X.toPresheafedSpace]
{f g s : ↑(X.presheaf.obj (Opposite.op ⊤))}
(hfg : TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = TopCat.Presheaf.restrictOpen g (X.basicOpen s) ⋯)
:
theorem
AlgebraicGeometry.exists_of_res_zero_of_qcqs
{X : 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.restrictOpen f (X.basicOpen s) ⋯ = 0)
:
theorem
AlgebraicGeometry.exists_of_res_zero_of_qcqs_of_top
{X : Scheme}
[CompactSpace ↑↑X.toPresheafedSpace]
[QuasiSeparatedSpace ↑↑X.toPresheafedSpace]
{f s : ↑(X.presheaf.obj (Opposite.op ⊤))}
(hf : TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = 0)
:
theorem
AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen
{X : Scheme}
[CompactSpace ↑↑X.toPresheafedSpace]
[QuasiSeparatedSpace ↑↑X.toPresheafedSpace]
(f : ↑(X.presheaf.obj (Opposite.op ⊤)))
:
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.