mathlib3 documentation

algebraic_geometry.morphisms.universally_closed

Universally closed morphism #

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 universally closed if X ×[Y] Y' ⟶ Y' is a closed map for all base change Y' ⟶ Y.

We show that being universally closed is local at the target, and is stable under compositions and base changes.

source
theorem algebraic_geometry.universally_closed_iff {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
algebraic_geometry.universally_closed f ↔ (algebraic_geometry.morphism_property.topologically is_closed_map).universally f
source
@[class]
structure algebraic_geometry.universally_closed {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) :
Prop

A morphism of schemes f : X ⟶ Y is universally closed if the base change X ×[Y] Y' ⟶ Y' along any morphism Y' ⟶ Y is (topologically) a closed map.

Instances of this typeclass
source
theorem algebraic_geometry.universally_closed_eq  :
algebraic_geometry.universally_closed = (algebraic_geometry.morphism_property.topologically is_closed_map).universally
source
theorem algebraic_geometry.universally_closed_respects_iso  :
category_theory.morphism_property.respects_iso algebraic_geometry.universally_closed
source
theorem algebraic_geometry.universally_closed_stable_under_base_change  :
category_theory.morphism_property.stable_under_base_change algebraic_geometry.universally_closed
source
theorem algebraic_geometry.universally_closed_stable_under_composition  :
category_theory.morphism_property.stable_under_composition algebraic_geometry.universally_closed
source
@[protected, instance]
def algebraic_geometry.universally_closed_type_comp {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : algebraic_geometry.universally_closed f] [hg : algebraic_geometry.universally_closed g] :
algebraic_geometry.universally_closed (f ≫ g)
source
@[protected, instance]
def algebraic_geometry.universally_closed_fst {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : algebraic_geometry.universally_closed g] :
algebraic_geometry.universally_closed category_theory.limits.pullback.fst
source
@[protected, instance]
def algebraic_geometry.universally_closed_snd {X Y Z : algebraic_geometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf : algebraic_geometry.universally_closed f] :
algebraic_geometry.universally_closed category_theory.limits.pullback.snd
source
theorem algebraic_geometry.morphism_restrict_base {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (U : topological_space.opens ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :
⇑((f ∣_ U).val.base) = U.carrier.restrict_preimage ⇑(f.val)
source
theorem algebraic_geometry.universally_closed_is_local_at_target  :
algebraic_geometry.property_is_local_at_target algebraic_geometry.universally_closed
source
theorem algebraic_geometry.universally_closed.open_cover_iff {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.open_cover) :
algebraic_geometry.universally_closed f ↔ ∀ (i : 𝒰.J), algebraic_geometry.universally_closed category_theory.limits.pullback.snd