Negative divisor classes on an interior-marked theta strand #
This file formalizes the divisor-class bijection asserted in paper Theorem
3.4. The source library exposes linear equivalence as an equivalence relation
but does not package its quotient, so we first introduce the corresponding
divisor-class type. The main Set.BijOn theorem is stated in the raw
subdivision orientation, the coordinate system consumed by the existing exact
interval theorem. Generic divisor-algebra wrappers keep its surjectivity
proof away from the concrete oneChip elaboration blowup.
Linear equivalence regarded as a setoid on graph divisors.
Equations
- Bananas.divisorLinearEquivSetoid G = { r := linearEquiv G, iseqv := ⋯ }
Instances For
The Picard quotient of all divisors on G. Degree components can be
recovered because linear equivalence preserves degree.
Equations
Instances For
Classes which possess a representative with negative marked rank
difference. This is literally the paper's set {[D] : Δ(D) < 0}.
Equations
- Bananas.negativeRankDeltaClasses M = {c : Bananas.DivisorClass M.graph | ∃ (D : CFDiv M.graph), Bananas.divisorClass M.graph D = c ∧ Bananas.rankDelta M D < 0}
Instances For
The missing forward direction of the displayed map in Theorem 3.4, in the raw path orientation used by the interval calculation.
Every exceptional position k gives precisely the advertised negative
divisor v_k + v_i. The endpoint k = length is included; its one-chip
deletion calculation is the subinterval-reflection firing script.
The advertised class-valued map of Theorem 3.4, restricted to its interior same-strand branch and written in raw path coordinates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The advertised map takes the exceptional set into the negative-class set.
Distinct path positions give distinct divisor classes after adding the fixed marked chip.
A negative divisor has the degree-one normal-form auxiliary vertex used in the paper, after adding the first marked chip back abstractly.
Rank zero and the three deletion ranks supplied by a negative theta divisor. Factoring this away keeps later coordinate proofs syntactic.
The normal-form auxiliary vertex satisfies exactly the two rank-zero conditions consumed by the same-strand interval theorem, and is not the second marked vertex.
Representative-level surjectivity of the displayed Theorem 3.4 map.
Every negative divisor is equivalent to v_k + v_i for an exceptional
position k.
The class map is surjective from exceptional positions onto negative divisor classes.
Theorem 3.4, class-valued bijection (raw-coordinate interior branch).
The displayed map k ↦ [v_k + v_i] restricts to a bijection from the paper's
exceptional set onto the set of linear-equivalence classes with negative
marked rank difference.