Structures · Geometry
AlgebraicGeometry.UniversallyClosed
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.
- Shape
- One type argument · adds universally_isClosedMap
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Every AlgebraicGeometry.UniversallyClosed is also a
Provided automatically by
Concrete types that are instances3
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.Proj
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- AlgebraicGeometry.Scheme.Hom.isClosedMap
- AlgebraicGeometry.UniversallyClosed.universally_isClosedMap
- AlgebraicGeometry.UniversallyClosed.of_comp_surjective
- AlgebraicGeometry.isIntegral_appTop_of_universallyClosed
- AlgebraicGeometry.isField_of_universallyClosed
- AlgebraicGeometry.UniversallyClosed.of_comp_of_isSeparated
- AlgebraicGeometry.compactSpace_of_universallyClosed
- AlgebraicGeometry.universallyClosed_snd
- AlgebraicGeometry.instUniversallyClosedMorphismRestrict
- AlgebraicGeometry.Surjective.of_universallyClosed_of_isDominant
- AlgebraicGeometry.instQuasiCompactOfUniversallyClosed
- AlgebraicGeometry.Scheme.Hom.isProperMap
- AlgebraicGeometry.universallyClosed_fst
- AlgebraicGeometry.finite_appTop_of_universallyClosed
- AlgebraicGeometry.instUniversallyClosedToNormalization
- AlgebraicGeometry.instUniversallyClosedToImage
- AlgebraicGeometry.UniversallyClosed.out
- AlgebraicGeometry.universallyClosedTypeComp