Addition in complete linear systems of Weil divisors

This file adds the additive calculus for the complete linear systems defined in TauCeti.AlgebraicGeometry.WeilDivisor.LinearSystem.Basic.

For an order system S, linear equivalence is compatible with addition of divisors. Hence members of complete linear systems add:

E ∈ |D|, F ∈ |D'| imply E + F ∈ |D + D'|.

The finite-sum version is the formal divisor bookkeeping used before symmetric powers and Abel maps are available: a finite collection of effective representatives in divisor classes adds to an effective representative in the sum class. The file also records that translating the indexing divisor of a complete linear system by a principal divisor does not change the system.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve" and "Degree", by extending the existing abstract complete-linear-system API needed before the scheme-theoretic symmetric-power and Abel-map layers. No external mathematics is vendored; the proofs use Tau Ceti's WeilDivisor/OrderSystem API and Mathlib's additive subgroup and finite-sum lemmas.

Addition of complete linear systems

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.add_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' E E' : WeilDivisor X} (hE : E ∈ S.completeLinearSystem D) (hE' : E' ∈ S.completeLinearSystem D') : E + E' ∈ S.completeLinearSystem (D + D')

Members of complete linear systems add to a member of the complete linear system of the sum class.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.add_mem_completeLinearSystem_left {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' E E' : WeilDivisor X} (hE : E ∈ S.completeLinearSystem D) : E' ∈ S.completeLinearSystem D' → E + E' ∈ S.completeLinearSystem (D + D')

Left addition by a fixed member of |D| sends |D'| into |D + D'|.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.add_mem_completeLinearSystem_right {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' E E' : WeilDivisor X} (hE' : E' ∈ S.completeLinearSystem D') : E ∈ S.completeLinearSystem D → E + E' ∈ S.completeLinearSystem (D + D')

Right addition by a fixed member of |D'| sends |D| into |D + D'|.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.nonempty_completeLinearSystem_add {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' : WeilDivisor X} (hD : (S.completeLinearSystem D).Nonempty) (hD' : (S.completeLinearSystem D').Nonempty) : (S.completeLinearSystem (D + D')).Nonempty

If two complete linear systems are nonempty, then the complete linear system of the sum of their divisor classes is nonempty.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.add_effective_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D A E : WeilDivisor X} (hA : A.IsEffective) (hE : E ∈ S.completeLinearSystem D) : E + A ∈ S.completeLinearSystem (D + A)

Translating a member of |D| by an effective divisor A gives a member of |D + A|.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mapsTo_add_effective_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D A : WeilDivisor X} (hA : A.IsEffective) : Set.MapsTo (fun (E : WeilDivisor X) => E + A) (S.completeLinearSystem D) (S.completeLinearSystem (D + A))

Translation by an effective divisor A sends |D| into |D + A|.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.nonempty_completeLinearSystem_add_effective {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D A : WeilDivisor X} (hA : A.IsEffective) (hD : (S.completeLinearSystem D).Nonempty) : (S.completeLinearSystem (D + A)).Nonempty

Adding an effective divisor to the indexing divisor preserves nonemptiness of complete linear systems.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.sum_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} {ι : Type u_3} [AddCommGroup G] (S : OrderSystem X G) (s : Finset ι) {D E : ι → WeilDivisor X} (h : ∀ i ∈ s, E i ∈ S.completeLinearSystem (D i)) : ∑ i ∈ s, E i ∈ S.completeLinearSystem (∑ i ∈ s, D i)

A finite sum of members of complete linear systems is a member of the complete linear system of the finite sum of the indexing divisors.

Principal translates

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.completeLinearSystem_add_principalDivisor_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) (g : G) : S.completeLinearSystem (D + S.principalDivisor g) = S.completeLinearSystem D

Adding a principal divisor to the indexing divisor does not change the complete linear system.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.completeLinearSystem_sub_principalDivisor_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) (g : G) : S.completeLinearSystem (D - S.principalDivisor g) = S.completeLinearSystem D

Subtracting a principal divisor from the indexing divisor does not change the complete linear system.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.add_principalDivisor_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) (g : G) (hEff : (D + S.principalDivisor g).IsEffective) : D + S.principalDivisor g ∈ S.completeLinearSystem D

An effective principal translate of D is a member of the complete linear system |D|.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.sub_principalDivisor_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) (g : G) (hEff : (D - S.principalDivisor g).IsEffective) : D - S.principalDivisor g ∈ S.completeLinearSystem D

An effective negative principal translate of D is a member of the complete linear system |D|.