Documentation

Mathlib.AlgebraicGeometry.Morphisms.Preimmersion

Preimmersions of schemes #

A morphism of schemes f : X ⟶ Y is a preimmersion if the underlying map of topological spaces is an embedding and the induced morphisms of stalks are all surjective. This is not a concept seen in the literature but it is useful for generalizing results on immersions to other maps including Spec 𝒪_{X, x} ⟶ X and inclusions of fibers κ(x) ×ₓ Y ⟶ Y.

TODO #

A morphism of schemes f : X ⟶ Y is a preimmersion if the underlying map of topological spaces is an embedding and the induced morphisms of stalks are all surjective.

Instances
    @[deprecated AlgebraicGeometry.Scheme.Hom.isEmbedding]

    Alias of AlgebraicGeometry.Scheme.Hom.isEmbedding.

    Being surjective on stalks is local at the target.