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
theorem AlgebraicGeometry.locallyOfFiniteType_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (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)
source
class AlgebraicGeometry.LocallyOfFiniteType {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.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.finiteType_of_affine_subset {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.LocallyOfFiniteType f] (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)
    source
    instance AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType :
    AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.LocallyOfFiniteType fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FiniteType
    Equations
    source
    @[instance 900]
    instance AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] :
    AlgebraicGeometry.LocallyOfFiniteType f
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.locallyOfFiniteType_comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.LocallyOfFiniteType f] [hg : AlgebraicGeometry.LocallyOfFiniteType g] :
    AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.locallyOfFiniteType_of_comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)] :
    AlgebraicGeometry.LocallyOfFiniteType f
    source
    theorem AlgebraicGeometry.locallyOfFiniteType_stableUnderBaseChange :
    CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.LocallyOfFiniteType