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.

theorem AlgebraicGeometry.locallyOfFiniteType_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (U : ↑(AlgebraicGeometry.Scheme.affineOpens Y)) (V : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (e : ↑V ≤ f⁻¹ᵁ ↑U), RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLe f e)

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.

• finiteType_of_affine_subset : ∀ (U : ↑(AlgebraicGeometry.Scheme.affineOpens Y)) (V : ↑(AlgebraicGeometry.Scheme.affineOpens X)) (e : ↑V ≤ f⁻¹ᵁ ↑U), RingHom.FiniteType (AlgebraicGeometry.Scheme.Hom.appLe f e)

theorem AlgebraicGeometry.locallyOfFiniteType_eq : @AlgebraicGeometry.LocallyOfFiniteType = AlgebraicGeometry.affineLocally @RingHom.FiniteType

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

Equations

• ⋯ = ⋯

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

Equations

• AlgebraicGeometry.locallyOfFiniteType_isStableUnderComposition = ⋯

instance AlgebraicGeometry.locallyOfFiniteTypeComp {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

• ⋯ = ⋯

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

theorem AlgebraicGeometry.LocallyOfFiniteType.affine_openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] (𝒰' : (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) → AlgebraicGeometry.Scheme.OpenCover ((AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).obj i)) [∀ (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)] : AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (i : (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f).J) (j : (𝒰' i).J), RingHom.FiniteType (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp ((𝒰' i).map j) CategoryTheory.Limits.pullback.snd).op)

theorem AlgebraicGeometry.LocallyOfFiniteType.source_openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) : AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)

theorem AlgebraicGeometry.LocallyOfFiniteType.openCover_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : AlgebraicGeometry.Scheme.OpenCover Y) : AlgebraicGeometry.LocallyOfFiniteType f ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.LocallyOfFiniteType CategoryTheory.Limits.pullback.snd

theorem AlgebraicGeometry.locallyOfFiniteType_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.LocallyOfFiniteType