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 : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.UniversallyClosed f ↔ (AlgebraicGeometry.topologically @IsClosedMap).universally f
    source
    theorem AlgebraicGeometry.Scheme.Hom.isClosedMap {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.UniversallyClosed f] :
    IsClosedMap ⇑f.base
    source
    theorem AlgebraicGeometry.universallyClosed_eq :
    @AlgebraicGeometry.UniversallyClosed = (AlgebraicGeometry.topologically @IsClosedMap).universally
    source
    @[instance 900]
    instance AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersion {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] :
    AlgebraicGeometry.UniversallyClosed f
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.universallyClosed_respectsIso :
    CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.UniversallyClosed
    source
    instance AlgebraicGeometry.universallyClosed_isStableUnderBaseChange :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.UniversallyClosed
    Equations
    source
    instance AlgebraicGeometry.isClosedMap_isStableUnderComposition :
    (AlgebraicGeometry.topologically @IsClosedMap).IsStableUnderComposition
    Equations
    source
    instance AlgebraicGeometry.universallyClosed_isStableUnderComposition :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.UniversallyClosed
    Equations
    source
    theorem AlgebraicGeometry.UniversallyClosed.of_comp_surjective {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.Surjective f] :
    AlgebraicGeometry.UniversallyClosed g
    source
    instance AlgebraicGeometry.universallyClosedTypeComp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.UniversallyClosed f] [hg : AlgebraicGeometry.UniversallyClosed g] :
    AlgebraicGeometry.UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyClosed :
    CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.UniversallyClosed
    Equations
    source
    instance AlgebraicGeometry.universallyClosed_fst {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : AlgebraicGeometry.UniversallyClosed g] :
    AlgebraicGeometry.UniversallyClosed (CategoryTheory.Limits.pullback.fst f g)
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.universallyClosed_snd {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf : AlgebraicGeometry.UniversallyClosed f] :
    AlgebraicGeometry.UniversallyClosed (CategoryTheory.Limits.pullback.snd f g)
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.universallyClosed_isLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.UniversallyClosed
    Equations
    source
    theorem AlgebraicGeometry.compactSpace_of_universallyClosed {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.UniversallyClosed f] :
    CompactSpace ↑↑X.toPresheafedSpace

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

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

    Stacks Tag 04XU

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