The coordinate map in the banana Jacobian presentation

This is the graph-level map used in Proposition 2.14 of the paper. A coordinate vector sends its alphath coordinate to the same multiple of the first normalized step on strand alpha, based at the left endpoint.

The file also supplies the exact quotient by the kernel of the induced map to divisor classes, and verifies the paper's strand-length relation generators. The remaining displayed generator (1, ..., 1) is the normalized first-neighbor form of firing the left endpoint; that finite Laplacian identity is kept separate from the pairwise path-prefix calculation below.

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

The degree-zero divisor representing one unit of the alphath coordinate in the paper's presentation.

Equations

• Bananas.bananaCoordinateStep B alpha = oneChip (Bananas.strandVertex B alpha ⟨1, ⋯⟩) - oneChip (Bananas.leftEndpoint B)

def Bananas.bananaCoordinateDivisorHom {g : ℕ} (B : Banana g) : (Fin (g + 1) → ℤ) →+ CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

The free coordinate-vector map tphi in the proof of Proposition 2.14.

Equations

• Bananas.bananaCoordinateDivisorHom B = { toFun := fun (a : Fin (g + 1) → ℤ) => ∑ alpha : Fin (g + 1), a alpha • Bananas.bananaCoordinateStep B alpha, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Bananas.degree_bananaCoordinateDivisorHom {g : ℕ} (B : Banana g) (a : Fin (g + 1) → ℤ) : CFDiv.degree ((bananaCoordinateDivisorHom B) a) = 0

Every coordinate vector maps to a divisor of degree zero.

def Bananas.bananaCoordinateClassHom {g : ℕ} (B : Banana g) : (Fin (g + 1) → ℤ) →+ CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) ⧸ principalDivisors (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

The coordinate map followed by passage to divisor classes. Its codomain is the additive quotient by principal divisors, i.e. the graph-level Picard group model used here. The preceding degree lemma shows that its image lies in the degree-zero (Jacobian) component.

Equations

• Bananas.bananaCoordinateClassHom B = (QuotientAddGroup.mk' (principalDivisors (Utilities.Certificate.SubdivisionGraph.Spec.graph B))).comp (Bananas.bananaCoordinateDivisorHom B)

def Bananas.bananaCoordinateRelations {g : ℕ} (B : Banana g) : AddSubgroup (Fin (g + 1) → ℤ)

The exact relation subgroup of the graph-level coordinate map. Showing that this kernel equals the paper's displayed lattice is the injectivity half of Proposition 2.14.

Equations

• Bananas.bananaCoordinateRelations B = (Bananas.bananaCoordinateClassHom B).ker

def Bananas.bananaPresentedClassHom {g : ℕ} (B : Banana g) : (Fin (g + 1) → ℤ) ⧸ bananaCoordinateRelations B →+ CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) ⧸ principalDivisors (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

The canonical map from coordinates modulo their exact graph relations to divisor classes.

Equations

• Bananas.bananaPresentedClassHom B = QuotientAddGroup.lift (Bananas.bananaCoordinateRelations B) (Bananas.bananaCoordinateClassHom B) ⋯

def Bananas.bananaCoordinateBasis {g : ℕ} (alpha : Fin (g + 1)) : Fin (g + 1) → ℤ

The standard coordinate vector e_alpha.

Equations

• Bananas.bananaCoordinateBasis alpha beta = if beta = alpha then 1 else 0

@[simp]

theorem Bananas.bananaCoordinateDivisorHom_basis {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) : (bananaCoordinateDivisorHom B) (bananaCoordinateBasis alpha) = bananaCoordinateStep B alpha

def Bananas.bananaStrandLengthRelation {g : ℕ} (B : Banana g) (beta : Fin (g + 1)) : Fin (g + 1) → ℤ

The displayed relation n_0 e_0 - n_beta e_beta.

Equations

• Bananas.bananaStrandLengthRelation B beta = ↑(B.length 0) • Bananas.bananaCoordinateBasis 0 - ↑(B.length beta) • Bananas.bananaCoordinateBasis beta

def Bananas.bananaDiagonalRelation {g : ℕ} : Fin (g + 1) → ℤ

The other displayed relation vector, (1, ..., 1).

Equations

• Bananas.bananaDiagonalRelation x✝ = 1

@[simp]

theorem Bananas.bananaCoordinateDivisorHom_diagonalRelation {g : ℕ} (B : Banana g) : (bananaCoordinateDivisorHom B) bananaDiagonalRelation = ∑ alpha : Fin (g + 1), bananaCoordinateStep B alpha

@[simp]

theorem Bananas.bananaCoordinateDivisorHom_strandLengthRelation {g : ℕ} (B : Banana g) (beta : Fin (g + 1)) : (bananaCoordinateDivisorHom B) (bananaStrandLengthRelation B beta) = ↑(B.length 0) • bananaCoordinateStep B 0 - ↑(B.length beta) • bananaCoordinateStep B beta

theorem Bananas.bananaCoordinateStep_length_linearEquiv_endpointDifference {g : ℕ} (B : Banana g) (alpha : Fin (g + 1)) : linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (↑(B.length alpha) • bananaCoordinateStep B alpha) (oneChip (rightEndpoint B) - oneChip (leftEndpoint B))

A full strand length advances the coordinate step from the left endpoint to the common right endpoint. This is Equation eq:multDiff at a=n_alpha.

theorem Bananas.bananaStrandLengthRelation_image_principal {g : ℕ} (B : Banana g) (beta : Fin (g + 1)) : (bananaCoordinateDivisorHom B) (bananaStrandLengthRelation B beta) ∈ principalDivisors (Utilities.Certificate.SubdivisionGraph.Spec.graph B)

Every displayed pairwise strand-length relation maps to a principal divisor.

theorem Bananas.bananaStrandLengthRelation_mem_relations {g : ℕ} (B : Banana g) (beta : Fin (g + 1)) : bananaStrandLengthRelation B beta ∈ bananaCoordinateRelations B

Hence the paper's pairwise strand-length generators belong to the exact relation subgroup of the graph-level class map.