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
.
This implies that f
is topologically proper (AlgebraicGeometry.Scheme.Hom.isProperMap
).
We show that being universally closed is local at the target, and is stable under compositions and base changes.
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.topologically @IsClosedMap).universally f
Instances
theorem
AlgebraicGeometry.universallyClosed_iff
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.UniversallyClosed f ↔ (AlgebraicGeometry.topologically @IsClosedMap).universally f
theorem
AlgebraicGeometry.Scheme.Hom.isClosedMap
{X Y : AlgebraicGeometry.Scheme}
(f : X.Hom Y)
[AlgebraicGeometry.UniversallyClosed f]
:
IsClosedMap ⇑f.base
theorem
AlgebraicGeometry.isClosedMap_isStableUnderComposition :
(AlgebraicGeometry.topologically @IsClosedMap).IsStableUnderComposition
theorem
AlgebraicGeometry.UniversallyClosed.of_comp_surjective
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)]
[AlgebraicGeometry.Surjective f]
:
theorem
AlgebraicGeometry.universallyClosedTypeComp
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.UniversallyClosed f]
[hg : AlgebraicGeometry.UniversallyClosed g]
:
theorem
AlgebraicGeometry.universallyClosed_fst
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[hg : AlgebraicGeometry.UniversallyClosed g]
:
theorem
AlgebraicGeometry.universallyClosed_snd
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[hf : AlgebraicGeometry.UniversallyClosed f]
:
theorem
AlgebraicGeometry.compactSpace_of_universallyClosed
{X : AlgebraicGeometry.Scheme}
{K : Type u}
[Field K]
(f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
[AlgebraicGeometry.UniversallyClosed f]
:
CompactSpace ↑↑X.toPresheafedSpace
If X
is universally closed over a field, then X
is quasi-compact.
theorem
AlgebraicGeometry.Scheme.Hom.isProperMap
{X Y : AlgebraicGeometry.Scheme}
(f : X.Hom Y)
[AlgebraicGeometry.UniversallyClosed f]
:
IsProperMap ⇑f.base