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 #

• AlgebraicGeometry.is_localization_basicOpen_of_qcqs (Qcqs lemma): If U is qcqs, then Γ(X, D(f)) ≃ Γ(X, U)_f for every f : Γ(X, U).
• diagonalQuasiCompact :

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

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

Instances

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

Instances For
theorem AlgebraicGeometry.quasiSeparatedSpace_iff_affine :
QuasiSeparatedSpace X.toPresheafedSpace ∀ (U V : ), IsCompact (U V)
instance AlgebraicGeometry.quasiSeparatedComp (f : X Y) (g : Y Z) :
theorem AlgebraicGeometry.QuasiSeparated.affine_openCover_TFAE (f : X Y) :
List.TFAE [, 𝒰 x, ∀ (i : 𝒰.J), QuasiSeparatedSpace (CategoryTheory.Limits.pullback f ()).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∀ (𝒰 : ) [inst : ∀ (i : 𝒰.J), ] (i : 𝒰.J), QuasiSeparatedSpace ().toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, ∀ {U : AlgebraicGeometry.Scheme} (g : U Y) [inst : ] [inst : ], QuasiSeparatedSpace ().toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace, 𝒰 x 𝒰' x, ∀ (i : 𝒰.J) (j k : (𝒰' i).J), CompactSpace (CategoryTheory.Limits.pullback () ()).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace]
theorem AlgebraicGeometry.QuasiSeparated.openCover_TFAE (f : X Y) :
List.TFAE [, 𝒰, ∀ (i : 𝒰.J), AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd, ∀ (𝒰 : ) (i : 𝒰.J), AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd, ∀ (U : TopologicalSpace.Opens Y.toPresheafedSpace), , ∀ {U : AlgebraicGeometry.Scheme} (g : U Y) [inst : ], AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd, ι U x, ∀ (i : ι), ]
theorem AlgebraicGeometry.QuasiSeparated.affine_openCover_iff [∀ (i : 𝒰.J), ] (f : X Y) :
∀ (i : 𝒰.J), QuasiSeparatedSpace ().toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace
theorem AlgebraicGeometry.QuasiSeparated.openCover_iff (f : X Y) :
∀ (i : 𝒰.J), AlgebraicGeometry.QuasiSeparated CategoryTheory.Limits.pullback.snd
theorem AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated (f : X Y) [hY : QuasiSeparatedSpace Y.toPresheafedSpace] :
QuasiSeparatedSpace X.toPresheafedSpace
theorem AlgebraicGeometry.IsAffineOpen.isQuasiSeparated {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : ) :
theorem AlgebraicGeometry.exists_eq_pow_mul_of_isAffineOpen (U : TopologicalSpace.Opens X.toPresheafedSpace) (hU : ) (f : ↑(X.presheaf.obj ())) (x : ↑(X.presheaf.obj ())) :
n y,
theorem AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux (S : ) (U₁ : TopologicalSpace.Opens X.toPresheafedSpace) (U₂ : TopologicalSpace.Opens X.toPresheafedSpace) {n₁ : } {n₂ : } {y₁ : ↑(X.presheaf.obj ())} {y₂ : ↑(X.presheaf.obj ())} {f : ↑(X.presheaf.obj (Opposite.op (U₁ U₂)))} {x : ↑(X.presheaf.obj ())} (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) )).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) )).op) x) :
n, ↑(X.presheaf.map ().op) (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₁ U₁ U₂)).op) f ^ (n + n₂) * y₁) = ↑(X.presheaf.map ().op) (↑(X.presheaf.map (CategoryTheory.homOfLE (_ : U₂ U₁ U₂)).op) f ^ (n + n₁) * y₂)
theorem AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (U : TopologicalSpace.Opens X.toPresheafedSpace) (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier) (f : ↑(X.presheaf.obj ())) (x : ↑(X.presheaf.obj ())) :
n y,
theorem AlgebraicGeometry.is_localization_basicOpen_of_qcqs {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : IsCompact U.carrier) (hU' : IsQuasiSeparated U.carrier) (f : ↑(X.presheaf.obj ())) :
IsLocalization.Away f ↑(X.presheaf.obj ())

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