Finite presentation of closed immersions

A closed immersion is locally of finite presentation exactly when its kernel ideal sheaf is locally finitely generated. We give both the affine-open and neighbourhood formulations, without a noetherian hypothesis. Applied to I.subschemeι, whose kernel is I, these criteria let local equations establish finite presentation of divisor inclusions over arbitrary bases.

References

• Stacks Project, Morphisms of Schemes, closed immersions of finite presentation, Tag 01TV.
• Stacks Project, Morphisms of Schemes, affine-local criteria for finite presentation, Tag 01TQ.

theorem AlgebraicGeometry.IsClosedImmersion.locallyOfFinitePresentation_morphismRestrict_iff {X Y : Scheme} {f : X ⟶ Y} [IsClosedImmersion f] {U : ↑Y.affineOpens} : LocallyOfFinitePresentation (f ∣_ ↑U) ↔ ((Scheme.Hom.ker f).ideal U).FG

Over an affine open, a closed immersion is of finite presentation exactly when its kernel ideal of sections is finitely generated.

theorem AlgebraicGeometry.IsClosedImmersion.locallyOfFinitePresentation_iff {X Y : Scheme} {f : X ⟶ Y} [IsClosedImmersion f] : LocallyOfFinitePresentation f ↔ ∀ (U : ↑Y.affineOpens), ((Scheme.Hom.ker f).ideal U).FG

A closed immersion is locally of finite presentation exactly when its kernel ideal on every affine open of the target is finitely generated.

theorem AlgebraicGeometry.IsClosedImmersion.locallyOfFinitePresentation_iff_exists_fg {X Y : Scheme} {f : X ⟶ Y} [IsClosedImmersion f] : LocallyOfFinitePresentation f ↔ ∀ (y : ↥Y), ∃ (U : ↑Y.affineOpens), y ∈ ↑U ∧ ((Scheme.Hom.ker f).ideal U).FG

Finite presentation of a closed immersion can be checked on one affine open with finitely generated kernel ideal near each point of the target.