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
theorem AlgebraicGeometry.universallyClosed_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
AlgebraicGeometry.UniversallyClosed f ↔ (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).universally f
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.out {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.UniversallyClosed f] :
    (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).universally f
    source
    theorem AlgebraicGeometry.universallyClosed_eq :
    @AlgebraicGeometry.UniversallyClosed = (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).universally
    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.MorphismProperty.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
    theorem AlgebraicGeometry.topologically_isClosedMap_respectsIso :
    (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).RespectsIso
    source
    instance AlgebraicGeometry.universallyClosedFst {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
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.universallyClosedSnd {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
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.morphismRestrict_base {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) :
    ⇑(f ∣_ U).val.base = U.carrier.restrictPreimage ⇑f.val.base
    source
    theorem AlgebraicGeometry.universallyClosed_is_local_at_target :
    AlgebraicGeometry.PropertyIsLocalAtTarget @AlgebraicGeometry.UniversallyClosed
    source
    theorem AlgebraicGeometry.UniversallyClosed.openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) :
    AlgebraicGeometry.UniversallyClosed f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.UniversallyClosed CategoryTheory.Limits.pullback.snd