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 Y : 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_appLE {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)).FinitePresentation

theorem AlgebraicGeometry.locallyOfFinitePresentation_iff {X Y : Scheme} (f : X ⟶ Y) : LocallyOfFinitePresentation 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)).FinitePresentation

theorem AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE {X Y : Scheme} (f : X ⟶ Y) [self : LocallyOfFinitePresentation 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)).FinitePresentation

Alias of AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE.

@[deprecated AlgebraicGeometry.Scheme.Hom.finitePresentation_appLE (since := "2026-01-20")]

theorem AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_of_affine_subset {X Y : Scheme} (f : X ⟶ Y) [self : LocallyOfFinitePresentation 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)).FinitePresentation

Alias of AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE.

---

Alias of AlgebraicGeometry.LocallyOfFinitePresentation.finitePresentation_appLE.

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

@[instance 900]

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

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

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

instance AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @LocallyOfFinitePresentation

instance AlgebraicGeometry.instLocallyOfFinitePresentationFstScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [LocallyOfFinitePresentation g] : LocallyOfFinitePresentation (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instLocallyOfFinitePresentationSndScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [LocallyOfFinitePresentation f] : LocallyOfFinitePresentation (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.instLocallyOfFinitePresentationMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [LocallyOfFinitePresentation f] : LocallyOfFinitePresentation (f ∣_ V)

instance AlgebraicGeometry.instLocallyOfFinitePresentationResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [LocallyOfFinitePresentation f] : LocallyOfFinitePresentation (Scheme.Hom.resLE f V U e)

instance AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] : LocallyOfFiniteType f

theorem AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image {X Y : Scheme} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X} (hs : Topology.IsLocallyConstructible s) : Topology.IsLocallyConstructible (⇑(CategoryTheory.ConcreteCategory.hom f.base) '' s)

Chevalley's Theorem: The image of a locally constructible set under a morphism of finite presentation is locally constructible.

theorem AlgebraicGeometry.Scheme.Hom.isConstructible_image {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [QuasiCompact f] [CompactSpace ↥Y] [QuasiSeparatedSpace ↥Y] {s : Set ↥X} (hs : Topology.IsConstructible s) : Topology.IsConstructible (⇑(CategoryTheory.ConcreteCategory.hom f.base) '' s)

Chevalley's Theorem: The image of a constructible set under a morphism of finite presentation into a qcqs scheme is constructible.

theorem AlgebraicGeometry.Scheme.Hom.isConstructible_preimage {X Y : Scheme} (f : X ⟶ Y) {s : Set ↥Y} (hs : Topology.IsConstructible s) : Topology.IsConstructible (⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' s)

Stacks Tag 054I