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.
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.
- out : (topologically @IsOpenMap).universally f
Instances
@[instance 900]
instance
AlgebraicGeometry.UniversallyOpen.instOfIsOpenImmersion
{X Y : Scheme}
(f : X ⟶ Y)
[IsOpenImmersion f]
:
instance
AlgebraicGeometry.UniversallyOpen.instCompScheme
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : UniversallyOpen f]
[hg : UniversallyOpen g]
:
instance
AlgebraicGeometry.UniversallyOpen.fst
{X Y Z : Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[hg : UniversallyOpen g]
:
instance
AlgebraicGeometry.UniversallyOpen.snd
{X Y Z : Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[hf : UniversallyOpen f]
:
theorem
AlgebraicGeometry.isOpenMap_of_generalizingMap
{X Y : Scheme}
(f : X ⟶ Y)
[LocallyOfFinitePresentation f]
(hf : GeneralizingMap ⇑(CategoryTheory.ConcreteCategory.hom f.base))
:
A generalizing morphism, locally of finite presentation is open.
Any flat morphism is generalizing.
@[instance 100]
instance
AlgebraicGeometry.UniversallyOpen.of_flat
{X Y : Scheme}
(f : X ⟶ Y)
[Flat f]
[LocallyOfFinitePresentation f]
:
A flat morphism, locally of finite presentation is universally open.