# Universally closed morphism #

A morphism of schemes `f : X ⟶ Y`

is universally closed if `X ×[Y] Y' ⟶ Y'`

is a closed map
for all base change `Y' ⟶ Y`

.

We show that being universally closed is local at the target, and is stable under compositions and base changes.

theorem
AlgebraicGeometry.universallyClosed_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:

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

A morphism of schemes `f : X ⟶ Y`

is universally closed if the base change `X ×[Y] Y' ⟶ Y'`

along any morphism `Y' ⟶ Y`

is (topologically) a closed map.

- out : (AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).universally f

## Instances

theorem
AlgebraicGeometry.UniversallyClosed.out
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{f : X ⟶ Y}
[self : AlgebraicGeometry.UniversallyClosed f]
:

(AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).universally f

instance
AlgebraicGeometry.isClosedMap_isStableUnderComposition :

(AlgebraicGeometry.MorphismProperty.topologically @IsClosedMap).IsStableUnderComposition

instance
AlgebraicGeometry.universallyClosedTypeComp
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.UniversallyClosed f]
[hg : AlgebraicGeometry.UniversallyClosed g]
:

## Equations

- ⋯ = ⋯

instance
AlgebraicGeometry.universallyClosedFst
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[hg : AlgebraicGeometry.UniversallyClosed g]
:

## Equations

- ⋯ = ⋯

instance
AlgebraicGeometry.universallyClosedSnd
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
{Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.UniversallyClosed f]
:

## Equations

- ⋯ = ⋯

theorem
AlgebraicGeometry.UniversallyClosed.openCover_iff
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(𝒰 : Y.OpenCover)
:

AlgebraicGeometry.UniversallyClosed f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.UniversallyClosed (CategoryTheory.Limits.pullback.snd f (𝒰.map i))