Cancellation for morphisms locally of finite presentation

Let f : X ⟶ Y and g : Y ⟶ Z be morphisms of schemes. If f ≫ g is locally of finite presentation and g is locally of finite type, then f is locally of finite presentation (AlgebraicGeometry.locallyOfFinitePresentation_of_comp). In particular, every morphism over Z between two schemes locally of finite presentation over Z is locally of finite presentation.

This is the scheme version of RingHom.FinitePresentation.of_comp_finiteType, to which the proof reduces on affine opens. It parallels Mathlib's AlgebraicGeometry.locallyOfFiniteType_of_comp, which needs no hypothesis on g; for finite presentation the hypothesis on g cannot be dropped.

Main results

• AlgebraicGeometry.locallyOfFinitePresentation_of_comp: if f ≫ g is locally of finite presentation and g is locally of finite type, then f is locally of finite presentation.

References

• The Stacks Project, Tag 02FV.

theorem AlgebraicGeometry.locallyOfFinitePresentation_of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hfg : LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp f g)] [hg : LocallyOfFiniteType g] : LocallyOfFinitePresentation f

Cancellation for morphisms locally of finite presentation (Stacks, Tag 02FV). If f ≫ g is locally of finite presentation and g is locally of finite type, then f is locally of finite presentation.