Documentation

Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Universally closed morphism #

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. This implies that f is topologically proper (AlgebraicGeometry.Scheme.Hom.isProperMap).

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

source
class AlgebraicGeometry.UniversallyClosed {X Y : 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
    source
    theorem AlgebraicGeometry.universallyClosed_iff {X Y : Scheme} (f : X ⟶ Y) :
    UniversallyClosed f ↔ (topologically @IsClosedMap).universally f
    source
    theorem AlgebraicGeometry.Scheme.Hom.isClosedMap {X Y : Scheme} (f : X ⟶ Y) [UniversallyClosed f] :
    IsClosedMap ⇑f
    source
    theorem AlgebraicGeometry.universallyClosed_eq :
    @UniversallyClosed = (topologically @IsClosedMap).universally
    source
    @[instance 900]
    instance AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersion {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] :
    UniversallyClosed f
    source
    theorem AlgebraicGeometry.universallyClosed_respectsIso :
    CategoryTheory.MorphismProperty.RespectsIso @UniversallyClosed
    source
    instance AlgebraicGeometry.universallyClosed_isStableUnderBaseChange :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @UniversallyClosed
    source
    instance AlgebraicGeometry.isClosedMap_isStableUnderComposition :
    (topologically @IsClosedMap).IsStableUnderComposition
    source
    instance AlgebraicGeometry.universallyClosed_isStableUnderComposition :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @UniversallyClosed
    source
    theorem AlgebraicGeometry.UniversallyClosed.of_comp_surjective {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)] [Surjective f] :
    UniversallyClosed g
    source
    instance AlgebraicGeometry.universallyClosedTypeComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : UniversallyClosed f] [hg : UniversallyClosed g] :
    UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)
    source
    instance AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyClosed :
    CategoryTheory.MorphismProperty.IsMultiplicative @UniversallyClosed
    source
    instance AlgebraicGeometry.universallyClosed_fst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : UniversallyClosed g] :
    UniversallyClosed (CategoryTheory.Limits.pullback.fst f g)
    source
    instance AlgebraicGeometry.universallyClosed_snd {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf : UniversallyClosed f] :
    UniversallyClosed (CategoryTheory.Limits.pullback.snd f g)
    source
    instance AlgebraicGeometry.universallyClosed_isZariskiLocalAtTarget :
    IsZariskiLocalAtTarget @UniversallyClosed
    source
    instance AlgebraicGeometry.instUniversallyClosedMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [UniversallyClosed f] :
    UniversallyClosed (f ∣_ V)
    source
    theorem AlgebraicGeometry.compactSpace_of_universallyClosed {X : Scheme} {K : Type u} [Field K] (f : X ⟶ Spec ↧K) [UniversallyClosed f] :
    CompactSpace ↥X

    If X is universally closed over a field, then X is quasi-compact.

    source
    theorem AlgebraicGeometry.Scheme.Hom.isProperMap {X Y : Scheme} (f : X ⟶ Y) [UniversallyClosed f] :
    IsProperMap ⇑f

    Stacks Tag 04XU

    source
    @[instance 900]
    instance AlgebraicGeometry.instQuasiCompactOfUniversallyClosed {X Y : Scheme} (f : X ⟶ Y) [UniversallyClosed f] :
    QuasiCompact f
    source
    theorem AlgebraicGeometry.universallyClosed_eq_universallySpecializing :
    @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ @QuasiCompact
    source
    @[instance 100]
    instance AlgebraicGeometry.Surjective.of_universallyClosed_of_isDominant {X Y : Scheme} (f : X ⟶ Y) [UniversallyClosed f] [IsDominant f] :
    Surjective f