Finiteness of relative effective Cartier divisors on relative curves

Let f : X ⟶ S be locally of finite type with fibres of dimension at most one, for instance a smooth relative curve, and let D be a relative effective Cartier divisor on X over S. Then D ⟶ S is locally quasi-finite. By Zariski's main theorem, D is therefore finite over S exactly when it is proper over S; in particular every relative effective Cartier divisor on a proper relative curve is finite over the base. Finiteness is thus a consequence of properness and not part of the definition of a relative effective Cartier divisor.

A finite relative effective Cartier divisor is flat over S by definition, and locally of finite presentation over S when X is, so it is finite locally free over S. Its degree is the locally constant rank Scheme.Hom.finrank of D ⟶ S.

The fibrewise input is absolute: on a locally Noetherian scheme of dimension at most one, an effective Cartier divisor is locally Artinian. Locally its ring is R ⧸ (a) for a Noetherian ring R of dimension at most one and a nonzerodivisor a, and dim R ⧸ (a) + 1 ≤ dim R. The fibre of D over a point s of S is the divisor on the fibre X_s obtained by base change, which is again effective Cartier because D is flat over S, so it is discrete and D ⟶ S has discrete fibres.

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.isLocallyArtinian_subscheme: an effective Cartier divisor on a locally Noetherian scheme of dimension at most one is locally Artinian.
• AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.locallyQuasiFinite: a relative effective Cartier divisor on a morphism locally of finite type of relative dimension at most one is locally quasi-finite over the base.
• AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isFinite_iff_isProper: such a divisor is finite over the base if and only if it is proper over the base.
• AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isFinite: on a proper morphism of relative dimension at most one, every relative effective Cartier divisor is finite over the base.
• AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.isFinite_subschemeι_comp: on a proper curve over a field, every effective Cartier divisor is finite over the field.
• AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isLocallyConstant_finrank: the degree of a proper relative effective Cartier divisor on a morphism locally of finite presentation of relative dimension at most one is locally constant on the base.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.2.
• Stacks Project, Tag 02LS: a morphism is finite if and only if it is proper and locally quasi-finite, Mathlib's AlgebraicGeometry.IsFinite.iff_isProper_and_locallyQuasiFinite.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.isLocallyArtinian_subscheme {X : Scheme} {I : X.IdealSheafData} [IsLocallyNoetherian X] (hX : topologicalKrullDim ↥X ≤ 1) (hI : I.IsEffectiveCartier) : IsLocallyArtinian I.subscheme

An effective Cartier divisor on a curve is zero-dimensional. On a locally Noetherian scheme of dimension at most one, the closed subscheme of an effective Cartier divisor is locally Artinian, so in particular it is a discrete topological space.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.locallyQuasiFinite {X S : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} [LocallyOfFiniteType f] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f] (hI : I.IsRelativeEffectiveCartier f) : LocallyQuasiFinite (CategoryTheory.CategoryStruct.comp I.subschemeι f)

Relative effective Cartier divisors on relative curves are locally quasi-finite. If f : X ⟶ S is locally of finite type with fibres of dimension at most one, then the closed subscheme of a relative effective Cartier divisor on X over S is locally quasi-finite over S.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isFinite_iff_isProper {X S : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} [LocallyOfFiniteType f] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f] (hI : I.IsRelativeEffectiveCartier f) : IsFinite (CategoryTheory.CategoryStruct.comp I.subschemeι f) ↔ IsProper (CategoryTheory.CategoryStruct.comp I.subschemeι f)

A relative effective Cartier divisor on a relative curve is finite exactly when it is proper. If f : X ⟶ S is locally of finite type with fibres of dimension at most one, then the closed subscheme of a relative effective Cartier divisor on X over S is finite over S if and only if it is proper over S.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isFinite {X S : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} [IsProper f] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f] (hI : I.IsRelativeEffectiveCartier f) : IsFinite (CategoryTheory.CategoryStruct.comp I.subschemeι f)

Relative effective Cartier divisors on proper relative curves are finite. If f : X ⟶ S is proper with fibres of dimension at most one, then the closed subscheme of every relative effective Cartier divisor on X over S is finite over S.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.isFinite_subschemeι_comp {X S : Scheme} {I : X.IdealSheafData} [Subsingleton ↥S] [IsIntegral S] {f : X ⟶ S} [IsProper f] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f] (hI : I.IsEffectiveCartier) : IsFinite (CategoryTheory.CategoryStruct.comp I.subschemeι f)

Effective Cartier divisors on proper curves over a field are finite. If S is an integral scheme with a single point, for instance the spectrum of a field, and f : X ⟶ S is proper with fibres of dimension at most one, then the closed subscheme of every effective Cartier divisor on X is finite over S: over such a base every effective Cartier divisor is relative.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsRelativeEffectiveCartier.isLocallyConstant_finrank {X S : Scheme} {I : X.IdealSheafData} {f : X ⟶ S} [LocallyOfFinitePresentation f] [TauCeti.AlgebraicGeometry.RelativeDimensionLE 1 f] [IsProper (CategoryTheory.CategoryStruct.comp I.subschemeι f)] (hI : I.IsRelativeEffectiveCartier f) : IsLocallyConstant (Hom.finrank (CategoryTheory.CategoryStruct.comp I.subschemeι f))

The degree of a relative effective Cartier divisor is locally constant. If f : X ⟶ S is locally of finite presentation with fibres of dimension at most one, and the closed subscheme of a relative effective Cartier divisor on X over S is proper over S, then that subscheme is finite locally free over S, and its rank Scheme.Hom.finrank, the degree of the divisor, is a locally constant function on S.