Structures · Geometry
AlgebraicGeometry.IsFinite
A morphism of schemes X ⟶ Y is finite if
the preimage of any affine open subset of Y is affine and the induced ring
hom is finite.
- Shape
- One type argument · adds finite_app
Extends1
Extended by2
Forgetful instances
Every AlgebraicGeometry.IsFinite is also a
- AlgebraicGeometry.IsIntegralHom
- AlgebraicGeometry.IsProper
- AlgebraicGeometry.LocallyOfFiniteType
- AlgebraicGeometry.LocallyQuasiFinite
Provided automatically by
Concrete types that are instances4
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- CategoryTheory.Limits.coprod
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso
- AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd
- AlgebraicGeometry.IsFinite.of_comp
- AlgebraicGeometry.Scheme.Hom.one_le_finrank_map
- AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback
- AlgebraicGeometry.IsFinite.finite_app
- AlgebraicGeometry.Scheme.Hom.finite_appTop
- AlgebraicGeometry.Scheme.Hom.finite_app
- AlgebraicGeometry.IsFinite.instIsIntegralHom
- AlgebraicGeometry.IsFinite.instCompScheme
- AlgebraicGeometry.IsFinite.instDescScheme
- AlgebraicGeometry.instIsProperOfIsFinite
- AlgebraicGeometry.IsProper.instOfIsFinite
- AlgebraicGeometry.Scheme.Hom.isIso_iff_finrank_eq
- AlgebraicGeometry.IsFinite.instSndScheme
- AlgebraicGeometry.Scheme.Hom.one_le_finrank_iff_surjective
- AlgebraicGeometry.IsFinite.comp_iff
- AlgebraicGeometry.instLocallyQuasiFiniteOfIsFinite
- AlgebraicGeometry.Scheme.Hom.isLocallyConstant_finrank
- AlgebraicGeometry.IsFinite.instLocallyOfFiniteType
- AlgebraicGeometry.IsFinite.instFstScheme
- AlgebraicGeometry.IsFinite.instMorphismRestrict
- AlgebraicGeometry.Scheme.Hom.finrank_pullback_fst
- AlgebraicGeometry.IsFinite.toIsAffineHom