Example 1.11: the torsion order of a cycle

A cycle graph, marked at its two junction vertices, is exactly a genus-one banana B : Banana 1, marked at leftEndpoint B and rightEndpoint B, with the two strand lengths B.length 0 and B.length 1 playing the role of the paper's a and b.

The proof identifies the marked difference [rightEndpoint - leftEndpoint] with (B.length 0) • w in the graph Jacobian, where w is the first normalized coordinate step on strand 0 (bananaCoordinateStep B 0). Two facts from the banana Jacobian presentation (Proposition 2.14) pin down the order of w exactly:

• the diagonal relation (firing the shared left endpoint once) identifies w on strand 1 with -w on strand 0, so combining the two strand-length relations gives (B.length 0 + B.length 1) • w ~ 0;
• conversely, the exact relation lattice of Proposition 2.14 (not just a containment) shows that no smaller multiple of w is principal, via a homomorphism to ZMod (B.length 0 + B.length 1) that kills exactly the displayed relations.

Combining the two pins down the torsion order at (B.length 0 + B.length 1) / gcd (B.length 0) (B.length 1), matching eg:cycle.

def Bananas.cycleTorsionHom (n : ℕ) : (Fin 2 → ℤ) →+ ZMod n

The homomorphism (x0, x1) ↦ x0 - x1 from banana coordinates to ZMod n. For n = a + b this kills exactly the displayed relations of a genus-one banana's Jacobian presentation.

Equations

• Bananas.cycleTorsionHom n = { toFun := fun (x : Fin 2 → ℤ) => ↑(x 0) - ↑(x 1), map_zero' := ⋯, map_add' := ⋯ }

theorem Bananas.cycle_isTorsionOrder (B : Banana 1) : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) ((B.length 0 + B.length 1) / (B.length 0).gcd (B.length 1))

Example 1.11 (eg:cycle), torsion order half: for a cycle graph B : Banana 1, marked at its two junction vertices, the torsion order of (leftEndpoint, rightEndpoint) is (a + b) / gcd a b with a = B.length 0, b = B.length 1.

theorem Bananas.cycle_allSubmodular (B : Banana 1) : AllSubmodular (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B))

Example 1.11 (eg:cycle), all-submodularity half: a cycle graph is connected of genus one with distinct marks, so every divisor is submodular.

theorem Bananas.cycle_kGeneralTransmission (B : Banana 1) : KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (leftEndpoint B) (rightEndpoint B)) ((B.length 0 + B.length 1) / (B.length 0).gcd (B.length 1))

Example 1.11 (eg:cycle): a cycle graph, marked at its two junction vertices, has k-general transmission at k = (a + b) / gcd a b, where a and b are the lengths of the two paths joining the marks.