Theta Lattice

The integer lattice in the paper's theta Jacobian presentation.

def Bananas.thetaLattice (a b c : ℕ) : AddSubgroup (ℤ × ℤ)

The theta Jacobian lattice generated by (a+c,c) and (-a,b) in the integer plane.

Equations

• Bananas.thetaLattice a b c = AddSubgroup.closure {(↑(a + c), ↑c), (-↑a, ↑b)}

theorem Bananas.thetaLattice_mem_iff (a b c : ℕ) (x y : ℤ) : (x, y) ∈ thetaLattice a b c ↔ ∃ (r : ℤ) (s : ℤ), x = r * ↑(a + c) - s * ↑a ∧ y = r * ↑c + s * ↑b

theorem Bananas.thetaLattice_evenlyMarked_multiple_mem_iff (a b c i j n : ℕ) (ha : 0 < a) (_hb : 0 < b) (hc : 0 < c) (hi : 0 < i) (hi' : i < a) (hj : 0 < j) (hj' : j < b) (hcross : a * j = b * i) : (↑(n * i), -↑(n * j)) ∈ thetaLattice a b c ↔ a / a.gcd i ∣ n