mathlib3 documentation

algebraic_geometry.morphisms.quasi_separated

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 #

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) :