Documentation

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Closed immersions of schemes #

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

Main definitions #

TODO #

A morphism of schemes X ⟶ Y is a closed immersion if the underlying topological map is a closed embedding and the induced stalk maps are surjective.

Instances

    Given two commutative rings R S : CommRingCat and a surjective morphism f : R ⟶ S, the induced scheme morphism specObj S ⟶ specObj R is a closed immersion.

    For any ideal I in a commutative ring R, the quotient map specObj R ⟶ specObj (R ⧸ I) is a closed immersion.

    Any morphism between affine schemes that is surjective on global sections is a closed immersion.

    If f ≫ g and g are closed immersions, then f is a closed immersion. Also see IsClosedImmersion.of_comp for the general version where g is only required to be separated.

    If f : X ⟶ Y is a morphism of schemes with quasi-compact source and affine target, f has a closed image and f induces an injection on global sections, then f is surjective.

    theorem AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X Y} [CompactSpace X.toPresheafedSpace] (hfopen : IsOpenMap f.base) (hfinj₁ : Function.Injective f.base) (hfinj₂ : Function.Injective (AlgebraicGeometry.Scheme.Hom.appTop f).hom) (x : X.toPresheafedSpace) :

    If f : X ⟶ Y is open, injective, X is quasi-compact and Y is affine, then f is stalkwise injective if it is injective on global sections.

    If f is a closed immersion with affine target such that the induced map on global sections is injective, f is an isomorphism.

    If f is a closed immersion with affine target, the source is affine and the induced map on global sections is surjective.

    On morphisms with affine target, being a closed immersion is precisely having affine source and being surjective on global sections.