Finite presentation of effective Cartier divisors

The closed immersion of an effective Cartier divisor is locally of finite presentation: its local principal equations give finitely generated defining ideals. Consequently, on a scheme locally of finite presentation over a base, the divisor is also locally of finite presentation over that base. No noetherian hypothesis is needed.

In particular, for a relative effective Cartier divisor on a smooth relative curve, this supplies the finite-presentation condition required in addition to finiteness and flatness for a finite locally free structure morphism.

References

• Stacks Project, Divisors, Effective Cartier divisors, Tag 01WQ.

theorem TauCeti.locallyOfFinitePresentation_subschemeι_of_isEffectiveCartier {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier) : AlgebraicGeometry.LocallyOfFinitePresentation I.subschemeι

The inclusion of an effective Cartier divisor is locally of finite presentation over an arbitrary ambient scheme.

theorem TauCeti.locallyOfFinitePresentation_subschemeι_comp_of_isEffectiveCartier {X S : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} (hI : I.IsEffectiveCartier) {f : X ⟶ S} [AlgebraicGeometry.LocallyOfFinitePresentation f] : AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.CategoryStruct.comp I.subschemeι f)

An effective Cartier divisor on a scheme locally of finite presentation over S is locally of finite presentation over S.