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_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (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.Opens}, IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType

theorem AlgebraicGeometry.Scheme.Hom.finiteType_appLE {X Y : Scheme} (f : X ⟶ Y) [self : LocallyOfFiniteType f] {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (appLE f U V e)).FiniteType

Alias of AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE.

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.instLocallyOfFiniteTypeFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType g] : LocallyOfFiniteType (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType f] : LocallyOfFiniteType (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [LocallyOfFiniteType f] : LocallyOfFiniteType (f ∣_ V)

instance AlgebraicGeometry.instLocallyOfFiniteTypeResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [LocallyOfFiniteType f] : LocallyOfFiniteType (Scheme.Hom.resLE f V U e)

theorem AlgebraicGeometry.LocallyOfFiniteType.stalkMap {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] (x : ↥X) : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType

instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] : JacobsonSpace ↥(Spec ↧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

theorem AlgebraicGeometry.essentiallySmall_costructuredArrow_Spec {X : Scheme} (P : CategoryTheory.MorphismProperty Scheme) (hP : P ≤ @LocallyOfFiniteType) [P.RespectsIso] : CategoryTheory.EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ Scheme.Spec X)

The category of affine schemes locally of finite type over a fixed base scheme is essentially small. TODO: extend this to (relatively) quasi-compact schemes.