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 of affines are induced by surjective ring maps
- Show closed immersions are stable under pullback
- 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 : ClosedEmbedding ⇑f.val.base
- surj_on_stalks : ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
Instances
Equations
- ⋯ = ⋯
Isomorphisms are closed immersions.
Equations
- ⋯ = ⋯
Composition of closed immersions is a closed immersion.
Equations
- ⋯ = ⋯
Composition with an isomorphism preserves closed immersions.
Equations
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.
Equations
- ⋯ = ⋯
Any morphism between affine schemes that is surjective on global sections is a closed immersion.
If f ≫ g
is a closed immersion, then f
is a closed immersion.
Equations
- ⋯ = ⋯
Being a closed immersion is local at the target.