A reduced-coordinate injectivity criterion for banana Jacobians

The paper represents a coordinate p_alpha by the divisor [v_{alpha,p_alpha}] - [left]. This file isolates the Jacobian argument from the remaining combinatorics of the paper's chosen fundamental domain: if the resulting divisor is reduced at the left endpoint, then it represents zero only when every coordinate is zero.

The missing step for the full injectivity half of Proposition 2.14 is now the concrete reducedness theorem: the paper's three conditions on the coordinates must be converted into the endpoint/semibreak normal form of Semibreak.lean.

def Bananas.bananaPositionCoordinateDivisor {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

The divisor attached in Proposition 2.14 to coordinates represented by positions on their respective strands.

Equations

• Bananas.bananaPositionCoordinateDivisor B p = ∑ alpha : Fin (g + 1), (oneChip (Bananas.strandVertex B alpha (p alpha)) - oneChip (Bananas.leftEndpoint B))

def Bananas.bananaPositionCoordinates {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : Fin (g + 1) → ℤ

Regard a vector of strand positions as the corresponding nonnegative integer coordinate vector.

Equations

• Bananas.bananaPositionCoordinates B p alpha = ↑↑(p alpha)

def Bananas.IsPaperReducedPositionCoordinates {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : Prop

The paper's three conditions for its preferred coordinate representatives. The bounds 0 ≤ a_alpha ≤ n_alpha are built into PathPosition; the two remaining clauses are recorded literally.

Equations

• Bananas.IsPaperReducedPositionCoordinates B p = ((∃ (alpha : Fin (g + 1)), ↑(p alpha) = 0) ∧ ∀ (alpha beta : Fin (g + 1)), ↑(p alpha) = B.length alpha → ↑(p beta) = 0 → alpha < beta)

theorem Bananas.bananaCoordinateDivisorHom_linearEquiv_positionDivisor {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) ((bananaCoordinateDivisorHom B) (bananaPositionCoordinates B p)) (bananaPositionCoordinateDivisor B p)

The position-coordinate divisor is the prefix-fired representative of the coordinate homomorphism.

theorem Bananas.bananaPositionCoordinates_eq_zero_of_qReduced_of_mem_relations {g : ℕ} (B : Banana g) (p : (alpha : Fin (g + 1)) → Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hReduced : qReduced (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (bananaPositionCoordinateDivisor B p)) (hKernel : bananaPositionCoordinates B p ∈ bananaCoordinateRelations B) : bananaPositionCoordinates B p = 0

A position-coordinate representative that is reduced at the left endpoint lies in the kernel of the coordinate class map only when all of its coordinates are zero.

This is the q-reduced uniqueness core of the injectivity argument in Proposition 2.14. The hypothesis hReduced is exactly the remaining bridge from the paper's elementary fundamental-domain inequalities to the formal semibreak API.