The two-coordinate theta Jacobian presentation

The general banana presentation has three coordinates in genus two. This file formalizes the paper's further quotient by the diagonal coordinate via the projection (x, y, z) ↦ (x - z, y - z). Its image relation lattice is generated by (a + c, c) and (-a, b), exactly as in the paper.

def Bananas.thetaCoordinateProjection : (Fin 3 → ℤ) →+ ℤ × ℤ

The projection from the three banana coordinates to the paper's two theta coordinates.

Equations

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

def Bananas.thetaCoordinateSection : ℤ × ℤ →+ Fin 3 → ℤ

The section of thetaCoordinateProjection obtained by setting the last coordinate to zero.

Equations

• Bananas.thetaCoordinateSection = { toFun := fun (x : ℤ × ℤ) (i : Fin 3) => if i = 0 then x.1 else if i = 1 then x.2 else 0, map_zero' := Bananas.thetaCoordinateSection._proof_1, map_add' := ⋯ }

@[simp]

theorem Bananas.thetaCoordinateProjection_section (x : ℤ × ℤ) : thetaCoordinateProjection (thetaCoordinateSection x) = x

theorem Bananas.thetaCoordinateProjection_mem_thetaLattice_of_mem_displayedRelations (B : Banana 2) (x : Fin 3 → ℤ) (hx : x ∈ bananaDisplayedRelations B) : thetaCoordinateProjection x ∈ thetaLattice (B.length 0) (B.length 1) (B.length 2)

Every displayed three-coordinate relation projects into the paper's two-dimensional theta lattice.

theorem Bananas.mem_bananaDisplayedRelations_of_thetaCoordinateProjection_mem (B : Banana 2) (x : Fin 3 → ℤ) (hx : thetaCoordinateProjection x ∈ thetaLattice (B.length 0) (B.length 1) (B.length 2)) : x ∈ bananaDisplayedRelations B

Conversely, the full preimage of the theta lattice is the displayed three-coordinate relation lattice. This is the kernel calculation in the paper's passage from three coordinates to two.

theorem Bananas.thetaCoordinateProjection_mem_thetaLattice_iff (B : Banana 2) (x : Fin 3 → ℤ) : thetaCoordinateProjection x ∈ thetaLattice (B.length 0) (B.length 1) (B.length 2) ↔ x ∈ bananaDisplayedRelations B

Exact preimage form of the theta lattice calculation.

def Bananas.thetaPresentedProjectionHom (B : Banana 2) : (Fin 3 → ℤ) ⧸ bananaDisplayedRelations B →+ (ℤ × ℤ) ⧸ thetaLattice (B.length 0) (B.length 1) (B.length 2)

The quotient map induced by (x,y,z) ↦ (x-z,y-z).

Equations

• One or more equations did not get rendered due to their size.

def Bananas.thetaPresentedSectionHom (B : Banana 2) : (ℤ × ℤ) ⧸ thetaLattice (B.length 0) (B.length 1) (B.length 2) →+ (Fin 3 → ℤ) ⧸ bananaDisplayedRelations B

The quotient map induced by the section (x,y) ↦ (x,y,0).

Equations

• One or more equations did not get rendered due to their size.

theorem Bananas.thetaPresentedSectionHom_leftInverse (B : Banana 2) : Function.LeftInverse ⇑(thetaPresentedSectionHom B) ⇑(thetaPresentedProjectionHom B)

theorem Bananas.thetaPresentedSectionHom_rightInverse (B : Banana 2) : Function.RightInverse ⇑(thetaPresentedSectionHom B) ⇑(thetaPresentedProjectionHom B)

def Bananas.thetaPresentedQuotientEquiv (B : Banana 2) : (Fin 3 → ℤ) ⧸ bananaDisplayedRelations B ≃+ (ℤ × ℤ) ⧸ thetaLattice (B.length 0) (B.length 1) (B.length 2)

The exact quotient isomorphism in the theta-Jacobian paragraph of the paper.

Equations

• Bananas.thetaPresentedQuotientEquiv B = { toFun := ⇑(Bananas.thetaPresentedProjectionHom B), invFun := ⇑(Bananas.thetaPresentedSectionHom B), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

noncomputable def Bananas.thetaLatticeQuotientEquivClassRange (B : Banana 2) : (ℤ × ℤ) ⧸ thetaLattice (B.length 0) (B.length 1) (B.length 2) ≃+ ↥(bananaCoordinateClassRange B)

Theta Jacobian presentation. The paper's two-coordinate quotient is additively isomorphic to the degree-zero divisor-class range of the theta graph.

Equations

• Bananas.thetaLatticeQuotientEquivClassRange B = (Bananas.thetaPresentedQuotientEquiv B).symm.trans (Bananas.bananaDisplayedQuotientEquivClassRange B)

theorem Bananas.thetaLatticeQuotientEquivClassRange_mk (B : Banana 2) (x : ℤ × ℤ) : (thetaLatticeQuotientEquivClassRange B) ((QuotientAddGroup.mk' (thetaLattice (B.length 0) (B.length 1) (B.length 2))) x) = ⟨(bananaCoordinateClassHom B) (thetaCoordinateSection x), ⋯⟩

Under the theta presentation, [x,y] is represented by the general banana coordinate vector (x,y,0), exactly as in the paper's construction.