Addition of relative effective Cartier divisors in families

Relative effective Cartier divisors on each base change X_T form a commutative monoid: the empty divisor is the identity, and addition multiplies ideal sheaves. Pullback along T' ⟶ T preserves this operation, including when the base change is not flat. This is the monoid structure used by the Abel map and by the degree components of the divisor functor.

The construction follows the description of addition of effective Cartier divisors in the Stacks Project, Divisors, Section "Effective Cartier divisors".

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.instCommMonoidObjOppositeOverSchemeToFunctorRelativeEffectiveCartierSubfunctor {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (T : (CategoryTheory.Over S)ᵒᵖ) : CommMonoid ((relativeEffectiveCartierSubfunctor f).toFunctor.obj T)

Pointwise addition of relative effective Cartier divisors is a commutative monoid.

theorem TauCeti.AlgebraicGeometry.relativeEffectiveCartier_map_one {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') : (CategoryTheory.ConcreteCategory.hom ((relativeEffectiveCartierSubfunctor f).toFunctor.map φ)) 1 = 1

Pullback of relative effective Cartier divisors preserves the empty divisor.

theorem TauCeti.AlgebraicGeometry.relativeEffectiveCartier_map_mul {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) {T T' : (CategoryTheory.Over S)ᵒᵖ} (φ : T ⟶ T') (D E : (relativeEffectiveCartierSubfunctor f).toFunctor.obj T) : (CategoryTheory.ConcreteCategory.hom ((relativeEffectiveCartierSubfunctor f).toFunctor.map φ)) (D * E) = (CategoryTheory.ConcreteCategory.hom ((relativeEffectiveCartierSubfunctor f).toFunctor.map φ)) D * (CategoryTheory.ConcreteCategory.hom ((relativeEffectiveCartierSubfunctor f).toFunctor.map φ)) E

Pullback of relative effective Cartier divisors preserves their sum.