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 and base change.

class AlgebraicGeometry.LocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) : Prop

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.

• finiteType_of_affine_subset (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).FiniteType

theorem AlgebraicGeometry.locallyOfFiniteType_iff {X Y : Scheme} (f : X ⟶ Y) : LocallyOfFiniteType f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).FiniteType

instance AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType : HasRingHomProperty @LocallyOfFiniteType fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FiniteType

@[instance 900]

instance AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : LocallyOfFiniteType f

instance AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType : CategoryTheory.MorphismProperty.IsStableUnderComposition @LocallyOfFiniteType

instance AlgebraicGeometry.locallyOfFiniteType_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : LocallyOfFiniteType f] [hg : LocallyOfFiniteType g] : LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.locallyOfFiniteType_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)] : LocallyOfFiniteType f

instance AlgebraicGeometry.instIsMultiplicativeSchemeLocallyOfFiniteType : CategoryTheory.MorphismProperty.IsMultiplicative @LocallyOfFiniteType

instance AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @LocallyOfFiniteType

instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] : JacobsonSpace ↥(Spec (CommRingCat.of R))

instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier {R : CommRingCat} [IsJacobsonRing ↑R] : JacobsonSpace ↥(Spec R)

theorem AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y] : JacobsonSpace ↥X