def spanLattice (a b : ℂ) : AddSubgroup ℂ

The additive subgroup of $\mathbb{C}$ generated by two complex numbers $a$ and $b$, i.e. the (typically rank-2) lattice $\mathbb{Z}a + \mathbb{Z}b$.

def IsCyclicSublattice (L' L : AddSubgroup ℂ) : Prop

A sublattice $L' \leq L$ is called cyclic (Definition 20.1) if the quotient $L/L'$ is a cyclic abelian group. Cyclic sublattices correspond to cyclic isogenies of the associated complex tori.

def IsCyclicIsogeny {F : Type u_1} [Field F] [DecidableEq F] {E₁ E₂ : WeierstrassCurve.Affine F} (φ : Isogeny E₁ E₂) : Prop

An isogeny $\varphi : E_1 \to E_2$ between elliptic curves over a field $F$ is cyclic iff its kernel is a cyclic abelian group.

theorem isCyclicIsogeny_iff_isCyclicSublattice {E₁ E₂ : WeierstrassCurve.Affine ℂ} (φ : Isogeny E₁ E₂) (L₁ L₂ : AddSubgroup ℂ) (hL : L₁ ≤ L₂) : IsCyclicIsogeny φ ↔ IsCyclicSublattice L₁ L₂

Lemma 20.2 (cyclic isogeny ↔ cyclic sublattice): an isogeny of complex elliptic curves is cyclic iff the corresponding sublattice inclusion has cyclic quotient.

theorem sublattice_hermite_form (τ : ℂ) (hτ : 0 < τ.im) (L' : AddSubgroup ℂ) (hL' : L' ≤ spanLattice 1 τ) (hfin : L'.index ≠ 0) : ∃ (d : ℕ) (a : ℕ) (k : ℤ), 0 < d ∧ 0 < a ∧ L' = spanLattice (↑d) (↑a * τ + ↑k) ∧ a * d = L'.index

Hermite normal form for sublattices: every finite-index sublattice $L'$ of $\mathbb{Z} + \mathbb{Z}\tau$ admits a basis of the form $\{d, a\tau + k\}$ with $a, d > 0$ and $a \cdot d = [L : L']$.

theorem spanLattice_one_Ntau_sub (τ : ℂ) (hτ : 0 < τ.im) (N : ℕ) (hN : 0 < N) : spanLattice 1 (↑N * τ) ≤ spanLattice 1 τ

The lattice $\mathbb{Z} + \mathbb{Z}(N\tau)$ is contained in $\mathbb{Z} + \mathbb{Z}\tau$: stretching the second generator by $N$ produces a sublattice.

theorem spanLattice_one_Ntau_index (τ : ℂ) (hτ : 0 < τ.im) (N : ℕ) (hN : 0 < N) : (spanLattice 1 (↑N * τ)).index = N

The sublattice $\mathbb{Z} + \mathbb{Z}(N\tau)$ has index exactly $N$ in $\mathbb{Z} + \mathbb{Z}\tau$.

theorem spanLattice_N_taupk_sub (τ : ℂ) (hτ : 0 < τ.im) (N : ℕ) (hN : 0 < N) (k : Fin N) : spanLattice (↑N) (τ + ↑↑k) ≤ spanLattice 1 τ

For each $k \in \{0, \ldots, N-1\}$, the lattice $\mathbb{Z}N + \mathbb{Z}(\tau + k)$ is a sublattice of $\mathbb{Z} + \mathbb{Z}\tau$: scaling the first generator by $N$ and shifting the second produces a sublattice.

theorem spanLattice_N_taupk_index (τ : ℂ) (hτ : 0 < τ.im) (N : ℕ) (hN : 0 < N) (k : Fin N) : (spanLattice (↑N) (τ + ↑↑k)).index = N

The sublattice $\mathbb{Z}N + \mathbb{Z}(\tau + k)$ has index exactly $N$ in $\mathbb{Z} + \mathbb{Z}\tau$.

theorem index_prime_isAddCyclic (τ : ℂ) (hτ : 0 < τ.im) (N : ℕ) (hN : Nat.Prime N) (L' : AddSubgroup ℂ) (hL' : L' ≤ spanLattice 1 τ) (hidx : L'.index = N) : IsAddCyclic (↥(spanLattice 1 τ) ⧸ L'.addSubgroupOf (spanLattice 1 τ))

Any sublattice of prime index $p$ has cyclic quotient: every abelian group of prime order is cyclic.

theorem spanLattice_shift_k (τ : ℂ) (hτ : 0 < τ.im) (d : ℕ) (hd : 0 < d) (b : ℂ) (k : ℤ) : spanLattice (↑d) (b + ↑k) = spanLattice (↑d) (b + ↑(k % ↑d))

Modding the integer shift $k$ by $d$ does not change the lattice $\mathbb{Z}d + \mathbb{Z}(b+k)$, since subtracting a multiple of $d$ from the second generator stays in the lattice.

theorem spanLattice_one_tau_shift (τ : ℂ) (hτ : 0 < τ.im) (N : ℕ) (hN : 0 < N) (k : ℤ) : spanLattice 1 (↑N * τ + ↑k) = spanLattice 1 (↑N * τ)

An integer shift of the second generator does not change the lattice $\mathbb{Z} + \mathbb{Z}(N\tau)$, since the shift is itself an integer combination of the first generator.

theorem prime_mul_eq {a d N : ℕ} (hN : Nat.Prime N) (ha : 0 < a) (hd : 0 < d) (h : a * d = N) : a = 1 ∧ d = N ∨ a = N ∧ d = 1

If $a \cdot d = p$ for a prime $p$ with $a, d > 0$, then $(a,d) = (1,p)$ or $(a,d) = (p,1)$.

theorem cyclicSublattices_prime_index (τ : ℂ) (hτ : 0 < τ.im) (N : ℕ) (hN : Nat.Prime N) (L' : AddSubgroup ℂ) : IsCyclicSublattice L' (spanLattice 1 τ) ∧ L'.index = N ↔ L' = spanLattice 1 (↑N * τ) ∨ ∃ (k : Fin N), L' = spanLattice (↑N) (τ + ↑↑k)

Classification of cyclic sublattices of prime index $p$ in $\mathbb{Z} + \mathbb{Z}\tau$: they are exactly the $p+1$ lattices $\mathbb{Z} + \mathbb{Z}(p\tau)$ and $\mathbb{Z}p + \mathbb{Z}(\tau + k)$ for $k = 0, 1, \ldots, p-1$. This parametrizes the $p+1$ cyclic $p$-isogenies out of the complex torus $\mathbb{C}/(\mathbb{Z}+\mathbb{Z}\tau)$.