# 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 stating`f : 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 an`O_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.