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 #
IsClosedImmersion
: The property of scheme morphisms statingf : X ⟶ Y
is a closed immersion.
TODO #
- Show closed immersions are precisely the proper monomorphisms
- Define closed immersions of locally ringed spaces, where we also assume that the kernel of
O_X → f_*O_Y
is locally generated by sections as anO_X
-module, and relate it to this file. See https://stacks.math.columbia.edu/tag/01HJ.
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.
- base_closed : Topology.IsClosedEmbedding ⇑f.base
- surj_on_stalks (x : ↑↑X.toPresheafedSpace) : Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x).hom
Instances
Alias of AlgebraicGeometry.Scheme.Hom.isClosedEmbedding
.
Isomorphisms are closed immersions.
Composition of closed immersions is a closed immersion.
Composition with an isomorphism preserves closed immersions.
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.
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.
Being a closed immersion is local at the target.
On morphisms with affine target, being a closed immersion is precisely having affine source and being surjective on global sections.
Being a closed immersion is stable under base change.
Closed immersions are locally of finite type.
A surjective closed immersion is an isomorphism when the target is reduced.