Morphisms of finite presentation

A morphism of schemes f : X ⟶ Y is locally of finite presentation if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite presentation.

A morphism of schemes is of finite presentation if it is both locally of finite presentation and quasi-compact. We do not provide a separate declaration for this, instead simply assume both conditions.

We show that these properties are local, and are stable under compositions.

class AlgebraicGeometry.LocallyOfFinitePresentation {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes f : X ⟶ Y is locally of finite presentation if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite presentation.

• finitePresentation_of_affine_subset : ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), RingHom.FinitePresentation (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

theorem AlgebraicGeometry.locallyOfFinitePresentation_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.LocallyOfFinitePresentation f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), RingHom.FinitePresentation (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

theorem AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.LocallyOfFinitePresentation f] (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : RingHom.FinitePresentation (AlgebraicGeometry.Scheme.Hom.appLE f (↑U) (↑V) e)

instance AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.LocallyOfFinitePresentation fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FinitePresentation

Equations

• AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFinitePresentation : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.LocallyOfFinitePresentation

Equations

• AlgebraicGeometry.instIsStableUnderCompositionSchemeLocallyOfFinitePresentation = ⋯

instance AlgebraicGeometry.locallyOfFinitePresentation_comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.LocallyOfFinitePresentation f] [hg : AlgebraicGeometry.LocallyOfFinitePresentation g] : AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp f g)

Equations

• ⋯ = ⋯

theorem AlgebraicGeometry.locallyOfFinitePresentation_stableUnderBaseChange : CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.LocallyOfFinitePresentation