Documentation

Mathlib.AlgebraicGeometry.Morphisms.FiniteType

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.

source
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.

Instances
    source
    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
    source
    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.

    source
    @[deprecated AlgebraicGeometry.Scheme.Hom.finiteType_appLE (since := "2026-01-20")]
    theorem AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset {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 (Scheme.Hom.appLE f U V e)).FiniteType

    Alias of AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE.

    Alias of AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE.

    source
    instance AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType :
    HasRingHomProperty @LocallyOfFiniteType fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FiniteType
    source
    @[instance 900]
    instance AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] :
    LocallyOfFiniteType f
    source
    instance AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFiniteType :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @LocallyOfFiniteType
    source
    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)
    source
    theorem AlgebraicGeometry.locallyOfFiniteType_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)] :
    LocallyOfFiniteType f
    source
    instance AlgebraicGeometry.instIsMultiplicativeSchemeLocallyOfFiniteType :
    CategoryTheory.MorphismProperty.IsMultiplicative @LocallyOfFiniteType
    source
    instance AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @LocallyOfFiniteType
    source
    instance AlgebraicGeometry.instLocallyOfFiniteTypeFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType g] :
    LocallyOfFiniteType (CategoryTheory.Limits.pullback.fst f g)
    source
    instance AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [LocallyOfFiniteType f] :
    LocallyOfFiniteType (CategoryTheory.Limits.pullback.snd f g)
    source
    instance AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [LocallyOfFiniteType f] :
    LocallyOfFiniteType (f ∣_ V)
    source
    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)
    source
    theorem AlgebraicGeometry.LocallyOfFiniteType.stalkMap {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] (x : ↥X) :
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType
    source
    instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] :
    JacobsonSpace ↥(Spec (CommRingCat.of R))
    source
    instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier {R : CommRingCat} [IsJacobsonRing ↑R] :
    JacobsonSpace ↥(Spec R)
    source
    theorem AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↥Y] :
    JacobsonSpace ↥X
    source
    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.