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 ↔ CategoryTheory.MorphismProperty.universally (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap) 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_eq :
    @AlgebraicGeometry.UniversallyClosed = CategoryTheory.MorphismProperty.universally (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap)
    source
    theorem AlgebraicGeometry.universallyClosed_respectsIso :
    CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.UniversallyClosed
    source
    theorem AlgebraicGeometry.universallyClosed_stableUnderBaseChange :
    CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.UniversallyClosed
    source
    theorem AlgebraicGeometry.universallyClosed_stableUnderComposition :
    CategoryTheory.MorphismProperty.StableUnderComposition @AlgebraicGeometry.UniversallyClosed
    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.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 = Set.restrictPreimage U.carrier ⇑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) (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) :
    AlgebraicGeometry.UniversallyClosed f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.UniversallyClosed CategoryTheory.Limits.pullback.snd