Torsion on elliptic curves

Stream: FLT

[Stepan Nesterov]

Reading Kevin's lecture notes reminded me of the following question:
To prove that a Galois representation attached to an elliptic curve is 2-dimensional, we need to know that $E[n]$ has cardinality $n^2$. Currently in FLT this theorem has the following comment:

-- This theorem needs e.g. a theory of division polynomials. It's ongoing work of David Angdinata.
-- Please do not work on it without talking to KB and David first.
theorem WeierstrassCurve.n_torsion_card [IsSepClosed k] {n : ℕ} (hn : (n : k) ≠ 0) :
    Nat.card (E.n_torsion n) = n^2 := sorry

I see that the theory of division polynomials has made it into mathlib: https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.html. What is the status of WeierstrassCurve.n_torsion_card then? Is somebody working on getting it into mathlib?

[Kevin Buzzard]

It's a natural thing to try and get into mathlib and @David Ang was thinking about it but I don't know the status. He spoke about it at LT2025 IIRC

[David Ang]

I will get to it as soon as I’m back to work next week! You can check my PR on elliptic nets to see how it’s going; I’ve just been borked by thesis-related things all these months