Structures · Geometry
AlgebraicGeometry.IsProper
A morphism is proper if it is separated, universally closed and locally of finite type.
- Shape
- One type argument
Extends3
Extended by1
Forgetful instances
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 by14
- AlgebraicGeometry.IsProper.of_comp
- AlgebraicGeometry.IsFinite.of_isProper_of_locallyQuasiFinite
- AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton
- AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
- AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage
- AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral
- AlgebraicGeometry.IsProper.instMorphismRestrict
- AlgebraicGeometry.IsProper.toLocallyOfFiniteType
- AlgebraicGeometry.IsProper.instSndScheme
- AlgebraicGeometry.IsProper.instFstScheme
- AlgebraicGeometry.IsProper.instCompScheme
- AlgebraicGeometry.IsProper.comp_iff
- AlgebraicGeometry.IsProper.toIsSeparated
- AlgebraicGeometry.IsProper.toUniversallyClosed