Complete linear systems of Weil divisors

This file adds the complete linear system |D| of a Weil divisor to the Jacobian roadmap's Layer A, on top of the formal Weil divisor group (TauCeti.AlgebraicGeometry.WeilDivisor.Basic) and the principal divisors and divisor class group of an order system (TauCeti.AlgebraicGeometry.WeilDivisor.Principal.Basic).

For an OrderSystem S on a type of points X, the complete linear system of a divisor D is the set of effective divisors linearly equivalent to D:

|D| = { E | E effective and E ∼ D }.

Classically |D| is the set of effective divisors of the form D + div f for a rational function f with D + div f ≥ 0; its members are the effective divisors in the linear equivalence class of D, and the associated projective space is ℙ(L(D)) for the Riemann–Roch space L(D). The vector-space structure of L(D) is Layer B and needs coherent cohomology, so it is deliberately not built here; this file supplies the set |D|, its description in terms of principal divisors, and the facts that make it well behaved: it depends only on the divisor class of D, every member shares the class and hence — when principal divisors have weighted degree zero — the weighted degree of D, a divisor of negative weighted degree has empty linear system, and a weighted-degree-zero divisor has only the zero effective representative.

Those facts are stated at the weighted level, for a weight w : X → ℤ, and are not restated for the unweighted degree. The unweighted statements are the constant weight w = fun _ => 1, where weightedDegree_one_eq_degree — a simp lemma — identifies weightedDegree (fun _ => 1) with degree, so a degree-shaped goal is reached from the weighted lemma by supplying that weight and normalising with it.

This advances the Tau Ceti Jacobian roadmap, Layer A, "Divisors on a curve" and "Degree": TauCetiRoadmap/JacobianChallenge/README.md. It reuses Tau Ceti's existing WeilDivisor and OrderSystem API and Mathlib's Set and quotient-group machinery; no external mathematics is vendored.

def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) (D : WeilDivisor X) : Set (WeilDivisor X)

The complete linear system |D| of a Weil divisor D with respect to an order system S: the set of effective divisors linearly equivalent to D.

Classically these are the divisors D + div f for a rational function f with D + div f effective; see mem_completeLinearSystem_iff_exists_principalDivisor.

Equations

• S.completeLinearSystem D = {E : TauCeti.AlgebraicGeometry.WeilDivisor X | E.IsEffective ∧ S.LinearlyEquivalent D E}

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D E : WeilDivisor X} : E ∈ S.completeLinearSystem D ↔ E.IsEffective ∧ S.LinearlyEquivalent D E

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

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

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.self_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D : WeilDivisor X} (hD : D.IsEffective) : D ∈ S.completeLinearSystem D

An effective divisor lies in its own complete linear system.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_completeLinearSystem_iff_divisorClass {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D E : WeilDivisor X} : E ∈ S.completeLinearSystem D ↔ E.IsEffective ∧ S.divisorClass D = S.divisorClass E

Membership in the complete linear system in terms of the divisor class: |D| consists of the effective divisors whose class equals that of D.

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

Every member of |D| has the same divisor class as D.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_completeLinearSystem_iff_exists_principalDivisor {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D E : WeilDivisor X} : E ∈ S.completeLinearSystem D ↔ E.IsEffective ∧ ∃ (g : G), E = D + S.principalDivisor g

The classical description of the complete linear system: its members are exactly the effective divisors D + div g obtained from D by adding a principal divisor.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.completeLinearSystem_eq_of_divisorClass_eq {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' : WeilDivisor X} (h : S.divisorClass D = S.divisorClass D') : S.completeLinearSystem D = S.completeLinearSystem D'

The complete linear system depends only on the divisor class: linearly equivalent divisors have the same complete linear system.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.completeLinearSystem_eq_of_linearlyEquivalent {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' : WeilDivisor X} (h : S.LinearlyEquivalent D D') : S.completeLinearSystem D = S.completeLinearSystem D'

The complete linear systems of linearly equivalent divisors coincide.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_completeLinearSystem_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {E : WeilDivisor X} : E ∈ S.completeLinearSystem 0 ↔ E.IsEffective ∧ ∃ (g : G), E = S.principalDivisor g

The complete linear system of the zero divisor consists of the effective principal divisors.

Degree along a complete linear system

When principal divisors have weighted degree zero (the geometric fact that a rational function has as many zeros as poles, counted with residue-field degrees), the weighted degree is constant on a complete linear system, so a negative-degree divisor has none.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegree_eq_of_mem_completeLinearSystem {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (h : S.IsWeightedDegreeZero w) {D E : WeilDivisor X} (hE : E ∈ S.completeLinearSystem D) : (weightedDegree w) E = (weightedDegree w) D

When principal divisors have weighted degree zero, every member of |D| has the same weighted degree as D.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.completeLinearSystem_eq_empty_of_weightedDegree_neg {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (hw : ∀ (x : X), 0 ≤ w x) (h : S.IsWeightedDegreeZero w) {D : WeilDivisor X} (hD : (weightedDegree w) D < 0) : S.completeLinearSystem D = ∅

With nonnegative weights and weighted-degree-zero principal divisors, a divisor of negative weighted degree has empty complete linear system.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.eq_zero_of_mem_completeLinearSystem_of_weightedDegree_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) (h : S.IsWeightedDegreeZero w) {D E : WeilDivisor X} (hE : E ∈ S.completeLinearSystem D) (hD : (weightedDegree w) D = 0) : E = 0

With positive weights and weighted-degree-zero principal divisors, every member of the complete linear system of a weighted-degree-zero divisor is zero.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mem_completeLinearSystem_iff_eq_zero_and_divisorClass_eq_zero_of_weightedDegree_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) (h : S.IsWeightedDegreeZero w) {D E : WeilDivisor X} (hD : (weightedDegree w) D = 0) : E ∈ S.completeLinearSystem D ↔ E = 0 ∧ S.divisorClass D = 0

With positive weights and weighted-degree-zero principal divisors, membership in the complete linear system of a weighted-degree-zero divisor is equivalent to being the zero divisor and the divisor class being zero.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.nonempty_completeLinearSystem_iff_divisorClass_eq_zero_of_weightedDegree_zero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) (h : S.IsWeightedDegreeZero w) {D : WeilDivisor X} (hD : (weightedDegree w) D = 0) : (S.completeLinearSystem D).Nonempty ↔ S.divisorClass D = 0

With positive weights and weighted-degree-zero principal divisors, nonemptiness of the complete linear system of a weighted-degree-zero divisor is equivalent to the divisor class being zero.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.completeLinearSystem_eq_singleton_zero_iff_divisorClass_eq_zero_of_isWeightedDegreeZero {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {w : X → ℤ} (hw : ∀ (x : X), 0 < w x) (h : S.IsWeightedDegreeZero w) {D : WeilDivisor X} : S.completeLinearSystem D = {0} ↔ S.divisorClass D = 0

With positive weights and weighted-degree-zero principal divisors, the complete linear system of D is {0} exactly when its divisor class is zero.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.nonempty_completeLinearSystem_iff {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D : WeilDivisor X} : (S.completeLinearSystem D).Nonempty ↔ ∃ (E : WeilDivisor X), E.IsEffective ∧ S.divisorClass E = S.divisorClass D

A complete linear system is nonempty exactly when the divisor class of D contains an effective divisor.