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
    theorem AlgebraicGeometry.Scheme.Hom.stalkMap_surjective {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.IsPreimmersion f] (x : ↑↑X.toPresheafedSpace) :
    Function.Surjective ⇑(f.stalkMap x)