Mazur's torsion theorem

TheoremMazur's torsion theorem#●ready to prove

Let \(E\) be an elliptic curve over \(\mathbb{Q}\). The torsion subgroup of the group \(E(\mathbb{Q})\) of rational points of \(E\) is finite and has at most \(16\) elements.

Only this bound is stated, not Mazur's full list of the fifteen possible torsion subgroups.

theorem_wanted mazur_torsion_ncard_le (E : WeierstrassCurve ℚ) [E.IsElliptic] :
    (AddCommGroup.torsion (E⁄ℚ).Point : Set (E⁄ℚ).Point).Finite ∧
      (AddCommGroup.torsion (E⁄ℚ).Point : Set (E⁄ℚ).Point).ncard ≤ 16

Sources

• B. Mazur, Modular curves and the Eisenstein ideal, Publ. Math. IHÉS 47 (1977), 33–186, doi:10.1007/BF02684339, https://www.numdam.org/item/?id=PMIHES_1977__47__33_0.

DefinitionThe Mazur class of abelian groups#✓fully proved

An abelian group \(T\) is in the Mazur class when it is isomorphic to \(\mathbb{Z}/n\mathbb{Z}\) for some \(n \in \{1, 2, \ldots, 10, 12\}\), or to \(\mathbb{Z}/2\mathbb{Z} \times \mathbb{Z}/2m\mathbb{Z}\) for some \(m \in \{1, 2, 3, 4\}\).

def IsInMazurClass (T : Type*) [AddCommGroup T] : Prop :=
  (∃ n ∈ ({1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12} : Finset ℕ),
      Nonempty (T ≃+ ZMod n)) ∨
  (∃ m ∈ ({2, 4, 6, 8} : Finset ℕ),
      Nonempty (T ≃+ (ZMod 2 × ZMod m)))

Used by 1

Used byMazur's torsion theorem

TheoremMazur's torsion theorem#●ready to prove

Let \(E\) be an elliptic curve over \(\mathbb{Q}\), given by a Weierstrass equation. The torsion subgroup of the group \(E(\mathbb{Q})\) of rational points of \(E\) is in the Mazur class: it is isomorphic to \(\mathbb{Z}/n\mathbb{Z}\) for some \(n \in \{1, 2, \ldots, 10, 12\}\), or to \(\mathbb{Z}/2\mathbb{Z} \times \mathbb{Z}/2m\mathbb{Z}\) for some \(m \in \{1, 2, 3, 4\}\).

public theorem_wanted mazur_torsion (E : WeierstrassCurve ℚ) [E.IsElliptic] :
    IsInMazurClass ↥(AddCommGroup.torsion (WeierstrassCurve.Affine.Point E))

Sources

• B. Mazur, Modular curves and the Eisenstein ideal, Publ. IHÉS 47 (1977). Knill, Some fundamental theorems in mathematics, §139. Problem mazur_torsion of the lean-eval benchmark.

Uses 1

Statement usesThe Mazur class of abelian groups

1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.