# 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.

- base_embedding : Topology.IsEmbedding ⇑f.base
- surj_on_stalks : ∀ (x : ↑↑X.toPresheafedSpace), Function.Surjective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
- isLocallyClosed_range : IsLocallyClosed (Set.range ⇑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`

.

## 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

- f.liftCoborder = AlgebraicGeometry.IsOpenImmersion.lift f.coborderRange.ι f ⋯

## Instances For

Any (locally-closed) immersion can be factored into a closed immersion followed by a (dominant) open immersion.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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.

## Equations

- ⋯ = ⋯