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.

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

    Any flat morphism is generalizing.

    @[instance 100]

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

    Stacks Tag 01UA