# Morphisms of finite type #

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.

A morphism of schemes is of finite type if it is both locally of finite type and quasi-compact.

We show that these properties are local, and are stable under compositions.

theorem AlgebraicGeometry.locallyOfFiniteType_iff (f : X Y) :
∀ (U : Y.affineOpens) (V : X.affineOpens) (e : V (TopologicalSpace.Opens.map f.val.base).obj U), RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLE f (U) (V) e)

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.

Instances
theorem AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset {f : X Y} [self : ] (U : Y.affineOpens) (V : X.affineOpens) (e : V (TopologicalSpace.Opens.map f.val.base).obj U) :
@[instance 900]
Equations
• =
instance AlgebraicGeometry.locallyOfFiniteType_comp (f : X Y) (g : Y Z) :
Equations
• =
theorem AlgebraicGeometry.LocallyOfFiniteType.affine_openCover_iff (f : X Y) (𝒰 : Y.OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (𝒰' : (i : (𝒰.pullbackCover f).J) → ((𝒰.pullbackCover f).obj i).OpenCover) [∀ (i : (𝒰.pullbackCover f).J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)] :
∀ (i : (𝒰.pullbackCover f).J) (j : (𝒰' i).J), RingHom.FiniteType ( (CategoryTheory.CategoryStruct.comp ((𝒰' i).map j) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))).op)
theorem AlgebraicGeometry.LocallyOfFiniteType.source_openCover_iff (f : X Y) (𝒰 : X.OpenCover) :
∀ (i : 𝒰.J),
theorem AlgebraicGeometry.LocallyOfFiniteType.openCover_iff (f : X Y) (𝒰 : Y.OpenCover) :
∀ (i : 𝒰.J),