Sums of relative effective Cartier divisors

The sum of effective Cartier divisors is represented by the product of their ideal sheaves. Over any base, sums of relative effective Cartier divisors are again relative effective Cartier. In particular, the multiples of a section divisor on a smooth relative curve remain relative effective Cartier, even when the sections coincide or the base is nonreduced. The absolute closure results TauCeti.isEffectiveCartier_mul, TauCeti.isEffectiveCartier_pow, and TauCeti.isEffectiveCartier_prod are provided by TauCeti.AlgebraicGeometry.EffectiveCartierDivisor.Basic. This module proves their relative counterparts: TauCeti.isRelativeEffectiveCartier_mul gives binary sums, TauCeti.isRelativeEffectiveCartier_pow gives multiples, and TauCeti.isRelativeEffectiveCartier_prod gives finite sums.

References

• Stacks Project, Divisors, Effective Cartier divisors and Relative effective Cartier divisors.
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, §1.1.

theorem TauCeti.isRelativeEffectiveCartier_mul {X S : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} {f : X ⟶ S} (hI : I.IsRelativeEffectiveCartier f) (hJ : J.IsRelativeEffectiveCartier f) : (I * J).IsRelativeEffectiveCartier f

The sum of two relative effective Cartier divisors is relative effective Cartier. No flatness of the ambient scheme, disjointness, reducedness, or noetherian hypothesis is needed.

theorem TauCeti.isRelativeEffectiveCartier_pow {X S : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {f : X ⟶ S} (hI : I.IsRelativeEffectiveCartier f) (n : ℕ) : (I ^ n).IsRelativeEffectiveCartier f

Every nonnegative multiple of a relative effective Cartier divisor is relative effective Cartier. This includes the empty divisor for multiplicity zero.

theorem TauCeti.isRelativeEffectiveCartier_prod {X S : AlgebraicGeometry.Scheme} {ι : Type u_1} {s : Finset ι} {I : ι → X.IdealSheafData} {f : X ⟶ S} (hI : ∀ i ∈ s, (I i).IsRelativeEffectiveCartier f) : (∏ i ∈ s, I i).IsRelativeEffectiveCartier f

A finite sum of relative effective Cartier divisors is relative effective Cartier, with no flatness assumption on the ambient scheme or restriction on intersections between the summands.