Structures · Geometry
AlgebraicGeometry.LocallyOfFiniteType
A morphism of schemes f : X ⟶ Y is locally of finite type if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite type.
- Shape
- One type argument · adds finiteType_appLE
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by5
Forgetful instances
Concrete types that are instances4
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.Spec
- AlgebraicGeometry.Proj
How is a type an instance?
Loading the hierarchy index…
Assumed by71
- AlgebraicGeometry.residueFieldIsoBase
- AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus
- AlgebraicGeometry.pointOfClosedPoint
- AlgebraicGeometry.Scheme.Hom.finiteType_appLE
- AlgebraicGeometry.pointEquivClosedPoint
- AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk
- AlgebraicGeometry.spread_out_of_isGermInjective'
- AlgebraicGeometry.pointOfClosedPoint_comp
- AlgebraicGeometry.LocallyQuasiFinite.of_finite_preimage_singleton
- AlgebraicGeometry.Scheme.exists_hom_comp_eq_comp_of_locallyOfFiniteType
- AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv
- AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace
- AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber
- AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian
- AlgebraicGeometry.ext_of_apply_closedPoint_eq
- AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt.isClopen_singleton_asFiber
- AlgebraicGeometry.Scheme.Hom.exists_isIso_morphismRestrict_toNormalization
- AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk
- AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff
- AlgebraicGeometry.spread_out_of_isGermInjective
- AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE
- AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage
- AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_eq
- AlgebraicGeometry.exists_etale_isCompl_of_quasiFiniteAt
- AlgebraicGeometry.locallyQuasiFinite_iff_isDiscrete_preimage_singleton
- AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top
- AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints
- AlgebraicGeometry.pointOfClosedPoint_apply
- AlgebraicGeometry.Scheme.RationalMap.ofFunctionField
- AlgebraicGeometry.Scheme.Hom.exists_mem_and_isIso_morphismRestrict_toNormalization
- AlgebraicGeometry.LocallyOfFiniteType.stalkMap
- AlgebraicGeometry.Scheme.PartialMap.mem_domain_ofFromSpecStalk
- AlgebraicGeometry.ext_of_apply_eq
- AlgebraicGeometry.smooth_of_grpObj
- AlgebraicGeometry.FormallyUnramified.instIsSeparableCarrierResidueFieldCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfLocallyOfFiniteType
- AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme
- AlgebraicGeometry.instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType
- AlgebraicGeometry.instIsOpenImmersionToNormalizationOfLocallyQuasiFiniteOfLocallyOfFiniteType
- AlgebraicGeometry.instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus
- AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict
- AlgebraicGeometry.locallyOfFiniteType_comp
- AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme
- AlgebraicGeometry.instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective
- AlgebraicGeometry.pointOfClosedPoint.congr_simp
- AlgebraicGeometry.pointEquivClosedPoint_apply_coe
- AlgebraicGeometry.Scheme.Hom.mem_quasiFiniteLocus
- AlgebraicGeometry.pointEquivClosedPoint_symm_apply_coe
- AlgebraicGeometry.locallyQuasiFinite_iff_finite_preimage_singleton
- AlgebraicGeometry.Scheme.RationalMap.equivFunctionField
- AlgebraicGeometry.IsProper.of_valuativeCriterion
Ancestors0
No ancestors.