The diagonal relation in the banana Jacobian presentation

The image of (1, ..., 1) under the coordinate-divisor map is the principal divisor obtained by firing the common left endpoint once. The proof uses normalized strand slopes, so it treats arbitrary storage orientations and length-one strands uniformly.

theorem Bananas.bananaDiagonalRelation_image_eq_prin_leftEndpoint {g : ℕ} (B : Banana g) : (bananaCoordinateDivisorHom B) bananaDiagonalRelation = (prin (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (oneChip (leftEndpoint B))

The diagonal coordinate vector maps to the principal divisor obtained by firing the common left endpoint once.

theorem Bananas.bananaDiagonalRelation_image_principal {g : ℕ} (B : Banana g) : (bananaCoordinateDivisorHom B) bananaDiagonalRelation ∈ principalDivisors (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

Thus the diagonal relation maps to a principal divisor.

theorem Bananas.bananaDiagonalRelation_mem_relations {g : ℕ} (B : Banana g) : bananaDiagonalRelation ∈ bananaCoordinateRelations B

The diagonal generator belongs to the exact graph relation subgroup.