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

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.

## Instances

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]
:

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

AlgebraicGeometry.UniversallyClosed CategoryTheory.Limits.pullback.fst

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

AlgebraicGeometry.UniversallyClosed CategoryTheory.Limits.pullback.snd

theorem
AlgebraicGeometry.morphismRestrict_base
{X : AlgebraicGeometry.Scheme}
{Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)
:

↑(f ∣_ U).val.base = Set.restrictPreimage U.carrier ↑f.val.base

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

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