Quasi-separated morphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
(algebraic_geometry.quasi_separated_space_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 #
is_localization_basic_open_of_qcqs(Qcqs lemma): IfUis qcqs, thenΓ(X, D(f)) ≃ Γ(X, U)_ffor everyf : Γ(X, U).
@[class]
- diagonal_quasi_compact : algebraic_geometry.quasi_compact (category_theory.limits.pullback.diagonal f)
A morphism is quasi_separated if diagonal map is quasi-compact.
Instances of this typeclass
The affine_target_morphism_property corresponding to quasi_separated, asserting that the
domain is a quasi-separated scheme.
Equations
theorem
algebraic_geometry.quasi_separated_space_iff_affine
(X : algebraic_geometry.Scheme) :
quasi_separated_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) ↔ ∀ (U V : ↥(X.affine_opens)), is_compact (↑U ∩ ↑V)
theorem
algebraic_geometry.quasi_compact_affine_property_iff_quasi_separated_space
{X Y : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine Y]
(f : X ⟶ Y) :
@[protected, instance]
def
algebraic_geometry.quasi_separated_of_mono
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y)
[category_theory.mono f] :
@[protected, instance]
def
algebraic_geometry.quasi_separated_comp
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[algebraic_geometry.quasi_separated f]
[algebraic_geometry.quasi_separated g] :
theorem
algebraic_geometry.quasi_separated.affine_open_cover_tfae
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y) :
[algebraic_geometry.quasi_separated f, ∃ (𝒰 : Y.open_cover) [_inst_1 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)], ∀ (i : 𝒰.J), quasi_separated_space ↥((category_theory.limits.pullback f (𝒰.map i)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), ∀ (𝒰 : Y.open_cover) [_inst_2 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (i : 𝒰.J), quasi_separated_space ↥((category_theory.limits.pullback f (𝒰.map i)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_3 : algebraic_geometry.is_affine U] [_inst_4 : algebraic_geometry.is_open_immersion g], quasi_separated_space ↥((category_theory.limits.pullback f g).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier), ∃ (𝒰 : Y.open_cover) [_inst_5 : ∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)] (𝒰' : Π (i : 𝒰.J), (category_theory.limits.pullback f (𝒰.map i)).open_cover) [_inst_6 : ∀ (i : 𝒰.J) (j : (𝒰' i).J), algebraic_geometry.is_affine ((𝒰' i).obj j)], ∀ (i : 𝒰.J) (j k : (𝒰' i).J), compact_space ↥((category_theory.limits.pullback ((𝒰' i).map j) ((𝒰' i).map k)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)].tfae
theorem
algebraic_geometry.quasi_separated.open_cover_tfae
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y) :
[algebraic_geometry.quasi_separated f, ∃ (𝒰 : Y.open_cover), ∀ (i : 𝒰.J), algebraic_geometry.quasi_separated category_theory.limits.pullback.snd, ∀ (𝒰 : Y.open_cover) (i : 𝒰.J), algebraic_geometry.quasi_separated category_theory.limits.pullback.snd, ∀ (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), algebraic_geometry.quasi_separated (f ∣_ U), ∀ {U : algebraic_geometry.Scheme} (g : U ⟶ Y) [_inst_1 : algebraic_geometry.is_open_immersion g], algebraic_geometry.quasi_separated category_theory.limits.pullback.snd, ∃ {ι : Type u} (U : ι → topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) (hU : supr U = ⊤), ∀ (i : ι), algebraic_geometry.quasi_separated (f ∣_ U i)].tfae
theorem
algebraic_geometry.quasi_separated.affine_open_cover_iff
{X Y : algebraic_geometry.Scheme}
(𝒰 : Y.open_cover)
[∀ (i : 𝒰.J), algebraic_geometry.is_affine (𝒰.obj i)]
(f : X ⟶ Y) :
theorem
algebraic_geometry.quasi_separated.open_cover_iff
{X Y : algebraic_geometry.Scheme}
(𝒰 : Y.open_cover)
(f : X ⟶ Y) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
algebraic_geometry.category_theory.category_struct.comp.quasi_separated
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[algebraic_geometry.quasi_separated f]
[algebraic_geometry.quasi_separated g] :
theorem
algebraic_geometry.quasi_separated_space_of_quasi_separated
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y)
[hY : quasi_separated_space ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)]
[algebraic_geometry.quasi_separated f] :
@[protected, instance]
theorem
algebraic_geometry.quasi_separated_of_comp
{X Y Z : algebraic_geometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[H : algebraic_geometry.quasi_separated (f ≫ g)] :
theorem
algebraic_geometry.exists_eq_pow_mul_of_is_affine_open
(X : algebraic_geometry.Scheme)
(U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))
(hU : algebraic_geometry.is_affine_open U)
(f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)))
(x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (X.basic_open f)))) :
∃ (n : ℕ) (y : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))), Top.presheaf.restrict_open y (X.basic_open f) _ = Top.presheaf.restrict_open f (X.basic_open f) _ ^ n * x
theorem
algebraic_geometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux
(X : algebraic_geometry.Scheme)
(S : ↥(X.affine_opens))
(U₁ U₂ : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))
{n₁ n₂ : ℕ}
{y₁ : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U₁))}
{y₂ : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U₂))}
{f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (U₁ ⊔ U₂)))}
{x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (X.basic_open f)))}
(h₁ : S.val ≤ U₁)
(h₂ : S.val ≤ U₂)
(e₁ : ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op) y₁ = ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op) (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le le_sup_left).op) f) ^ n₁ * ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op) x)
(e₂ : ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op) y₂ = ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op) (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le le_sup_right).op) f) ^ n₂ * ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le _).op) x) :
∃ (n : ℕ), ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le h₁).op) (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le le_sup_left).op) f ^ (n + n₂) * y₁) = ⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le h₂).op) (⇑(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.hom_of_le le_sup_right).op) f ^ (n + n₁) * y₂)
theorem
algebraic_geometry.exists_eq_pow_mul_of_is_compact_of_is_quasi_separated
(X : algebraic_geometry.Scheme)
(U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))
(hU : is_compact U.carrier)
(hU' : is_quasi_separated U.carrier)
(f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)))
(x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (X.basic_open f)))) :
∃ (n : ℕ) (y : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))), Top.presheaf.restrict_open y (X.basic_open f) _ = Top.presheaf.restrict_open f (X.basic_open f) _ ^ n * x
theorem
algebraic_geometry.is_localization_basic_open_of_qcqs
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : is_compact U.carrier)
(hU' : is_quasi_separated U.carrier)
(f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.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.