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.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), (Scheme.Hom.appLE f (↑U) (↑V) e).hom.FiniteType
    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.instJacobsonSpaceαTopologicalSpaceCarrierCommRingCatSpecOfOfIsJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] :
    JacobsonSpace ↑↑(Spec (CommRingCat.of R)).toPresheafedSpace
    source
    instance AlgebraicGeometry.instJacobsonSpaceαTopologicalSpaceCarrierCommRingCatSpecOfIsJacobsonRingCarrier {R : CommRingCat} [IsJacobsonRing ↑R] :
    JacobsonSpace ↑↑(Spec R).toPresheafedSpace
    source
    theorem AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace ↑↑Y.toPresheafedSpace] :
    JacobsonSpace ↑↑X.toPresheafedSpace