Surjectivity of the banana coordinate map in degree zero

This file proves the surjectivity half of the graph-level Jacobian presentation in Proposition 2.14. Every vertex difference from the left endpoint is represented by a multiple of one strand coordinate. Expanding a degree-zero divisor as a sum of these differences then gives a coordinate vector whose image is linearly equivalent to that divisor.

theorem Bananas.exists_bananaCoordinate_linearEquiv_vertexDifference {g : ℕ} (B : Banana g) (v : (Utilities.Certificate.SubdivisionGraph.Spec.graph B).V) : ∃ (a : Fin (g + 1) → ℤ), linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) ((bananaCoordinateDivisorHom B) a) (oneChip v - oneChip (leftEndpoint B))

Every difference between a banana vertex and the left endpoint is represented by a strand-coordinate vector.

theorem Bananas.exists_bananaCoordinate_linearEquiv_of_degree_zero {g : ℕ} (B : Banana g) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hDegree : CFDiv.degree D = 0) : ∃ (a : Fin (g + 1) → ℤ), linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) ((bananaCoordinateDivisorHom B) a) D

Graph-level surjectivity onto the degree-zero component: every degree-zero divisor class has a representative in the image of the banana coordinate map. This is the surjectivity half of Proposition 2.14 before packaging the codomain as a degree-zero subgroup of the divisor-class quotient.