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

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

    Instances For
      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.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.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.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))) :

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