Immersions of schemes #
A morphism of schemes f : X ⟶ Y
is an immersion if the underlying map of topological spaces
is a locally closed embedding, and the induced morphisms of stalks are all surjective. This is true
if and only if it can be factored into a closed immersion followed by an open immersion.
Main result #
isImmersion_iff_exists
: A morphism is a (locally-closed) immersion if and only if it can be factored into a closed immersion followed by a (dominant) open immersion.
A morphism of schemes f : X ⟶ Y
is an immersion if
- the underlying map of topological spaces is an embedding
- the range of the map is locally closed
- the induced morphisms of stalks are all surjective.
- isLocallyClosed_range : IsLocallyClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))
Instances
Given an immersion f : X ⟶ Y
, this is the biggest open set U ⊆ Y
containing the image of X
such that X
is closed in U
.
Equations
- f.coborderRange = { carrier := coborder (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)), is_open' := ⋯ }
Instances For
The first part of the factorization of an immersion f : X ⟶ Y
to a closed immersion
f.liftCoborder : X ⟶ f.coborderRange
and a dominant open immersion f.coborderRange.ι
.
Equations
Instances For
Any (locally-closed) immersion can be factored into a closed immersion followed by a (dominant) open immersion.
A morphism is a (locally-closed) immersion if and only if it can be factored into a closed immersion followed by an open immersion.
The diagonal morphism is always an immersion.