Documentation

Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Universally open morphism #

A morphism of schemes f : X ⟶ Y is universally open if X ×[Y] Y' ⟶ Y' is an open map for all base change Y' ⟶ Y.

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

source
class AlgebraicGeometry.UniversallyOpen {X Y : Scheme} (f : X ⟶ Y) :
Prop

A morphism of schemes f : X ⟶ Y is universally open if the base change X ×[Y] Y' ⟶ Y' along any morphism Y' ⟶ Y is (topologically) an open map.

Instances
    source
    theorem AlgebraicGeometry.universallyOpen_iff {X Y : Scheme} (f : X ⟶ Y) :
    UniversallyOpen f ↔ (topologically @IsOpenMap).universally f
    source
    theorem AlgebraicGeometry.Scheme.Hom.isOpenMap {X Y : Scheme} (f : X ⟶ Y) [UniversallyOpen f] :
    IsOpenMap ⇑f
    source
    theorem AlgebraicGeometry.UniversallyOpen.eq :
    @UniversallyOpen = (topologically @IsOpenMap).universally
    source
    @[instance 900]
    instance AlgebraicGeometry.UniversallyOpen.instOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :
    UniversallyOpen f
    source
    instance AlgebraicGeometry.UniversallyOpen.instRespectsIsoScheme :
    CategoryTheory.MorphismProperty.RespectsIso @UniversallyOpen
    source
    instance AlgebraicGeometry.UniversallyOpen.instIsStableUnderBaseChangeScheme :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @UniversallyOpen
    source
    instance AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionSchemeTopologicallyIsOpenMap :
    (topologically @IsOpenMap).IsStableUnderComposition
    source
    instance AlgebraicGeometry.UniversallyOpen.instIsStableUnderCompositionScheme :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @UniversallyOpen
    source
    instance AlgebraicGeometry.UniversallyOpen.instCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : UniversallyOpen f] [hg : UniversallyOpen g] :
    UniversallyOpen (CategoryTheory.CategoryStruct.comp f g)
    source
    instance AlgebraicGeometry.UniversallyOpen.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @UniversallyOpen
    source
    instance AlgebraicGeometry.UniversallyOpen.fst {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hg : UniversallyOpen g] :
    UniversallyOpen (CategoryTheory.Limits.pullback.fst f g)
    source
    instance AlgebraicGeometry.UniversallyOpen.snd {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [hf : UniversallyOpen f] :
    UniversallyOpen (CategoryTheory.Limits.pullback.snd f g)
    source
    instance AlgebraicGeometry.UniversallyOpen.instIsZariskiLocalAtTarget :
    IsZariskiLocalAtTarget @UniversallyOpen
    source
    instance AlgebraicGeometry.UniversallyOpen.instIsZariskiLocalAtSource :
    IsZariskiLocalAtSource @UniversallyOpen
    source
    theorem AlgebraicGeometry.isOpenMap_of_generalizingMap {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap ⇑f) :
    IsOpenMap ⇑f

    A generalizing morphism, locally of finite presentation is open.

    source
    theorem AlgebraicGeometry.Flat.generalizingMap {X Y : Scheme} (f : X ⟶ Y) [Flat f] :
    GeneralizingMap ⇑f

    Any flat morphism is generalizing.

    source
    @[instance 100]
    instance AlgebraicGeometry.UniversallyOpen.of_flat {X Y : Scheme} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] :
    UniversallyOpen f

    A flat morphism, locally of finite presentation is universally open.

    source
    @[instance 100]
    instance AlgebraicGeometry.instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat {X Y : Scheme} (f : X ⟶ Y) [IsIntegral Y] [Subsingleton ↥Y] :
    UniversallyOpen f