# Separated morphisms #

A morphism of schemes is separated if its diagonal morphism is a closed immmersion.

## TODO #

- Show separated is stable under composition and base change (this is immediate if we show that closed immersions are stable under base change).
- Show separated is local at the target.
- Show affine morphisms are separated.

class
AlgebraicGeometry.IsSeparated
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:

A morphism is separated if the diagonal map is a closed immersion.

- diagonal_isClosedImmersion : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
A morphism is separated if the diagonal map is a closed immersion.

## Instances

theorem
AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{f : X ⟶ Y}
[self : AlgebraicGeometry.IsSeparated f]
:

A morphism is separated if the diagonal map is a closed immersion.

@[instance 900]

instance
AlgebraicGeometry.IsSeparated.isSeparated_of_mono
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:

Monomorphisms are separated.

## Equations

- ⋯ = ⋯

@[instance 900]

instance
AlgebraicGeometry.IsSeparated.instQuasiSeparated
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsSeparated f]
:

## Equations

- ⋯ = ⋯