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.

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

source
class AlgebraicGeometry.UniversallyClosed {X : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.UniversallyClosed f ↔ (AlgebraicGeometry.topologically @IsClosedMap).universally f
    source
    theorem AlgebraicGeometry.UniversallyClosed.out {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.UniversallyClosed f] :
    (AlgebraicGeometry.topologically @IsClosedMap).universally f
    source
    theorem AlgebraicGeometry.universallyClosed_eq :
    @AlgebraicGeometry.UniversallyClosed = (AlgebraicGeometry.topologically @IsClosedMap).universally
    source
    @[instance 900]
    instance AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] :
    AlgebraicGeometry.UniversallyClosed f
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.universallyClosed_respectsIso :
    CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.UniversallyClosed
    source
    theorem AlgebraicGeometry.universallyClosed_stableUnderBaseChange :
    CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.UniversallyClosed
    source
    instance AlgebraicGeometry.isClosedMap_isStableUnderComposition :
    (AlgebraicGeometry.topologically @IsClosedMap).IsStableUnderComposition
    Equations
    source
    instance AlgebraicGeometry.universallyClosed_isStableUnderComposition :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.UniversallyClosed
    Equations
    source
    instance AlgebraicGeometry.universallyClosedTypeComp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {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