There are several proofs in the textbooks. The proof being worked on uses the theory of division polynomials; the formalisation is ongoing work of David Angdinata, and it will be part of his PhD thesis.

The result is obvious if \(n=1\), so we may assume \(n{\gt}1\). One proof would be to write \(A\) as \(\prod _{i=1}^t(\mathbb {Z}/a_i\mathbb {Z})\) with \(a_i\mid a_{i+1}\) (this is possible by the structure theorem for finite abelian groups), and then to apply our hypothesis firstly with \(d=a_1\) to deduce \(t=r\) and then with \(d=a_t\) to deduce \(a_1=a_t\).

This follows from the previous group-theoretic lemma 3.2 and theorem 3.1.

This presumably should be done via the Weil pairing. I have not yet put any thought into a feasible way to formalise this.

The reduction mod \(p\) of the equation defining the Frey curve is still a smooth plane cubic, because the three roots \(0\), \(a^\ell \) and \(-b^\ell \) are distinct modulo \(p\) (note that the difference between \(a^\ell \) and \(-b^\ell \) is \(c^\ell \)).

One approach would be by showing that the \(n\)-torsion in the integral model of \(E\) over \(\mathcal{O}_{N,P}\) is an etale finite flat group scheme. There might be simpler approaches however. It’s worth looking to see what Silverman does.

Indeed, the kernel of the \(p\)-torsion on a good integral model is finite and flat. Checking this claim formally will probably involve a fair amount of work.

The hypothesis \(p\mid abc\) implies that precisely two of the three roots \(0\), \(a^\ell \) and \(-b^\ell \) of the cubic are equal mod \(p\). Call \(x\in \mathbb {Z}/p\mathbb {Z}\) this common value. Then the reduction mod \(p\) of the curve is smooth away from the point \((x,0)\), and has an ordinary double point at \((x,0)\). Hence the Frey curve has multiplicative reduction at \(p\).

Indeed, the change of variables \(X=4X'\) and \(Y=8Y'+4X'\) transforms the equation to \(64Y'^2+64X'Y'=64X'^3+16X'^2(b^\ell -a^\ell -1)-4X'a^\ell b^\ell \) and, because \(\ell \geq 5\), \(b\) is even and \(a=3\) mod 4, we see that the 64s cancel, giving an equation over \(\mathbb {Z}\) which reduces mod 2 to \(Y'^2+X'Y'=X'^3+cX'^2\) for some \(c\in \{ 0,1\} \). This cubic is smooth away from an ordinary double point at \((0,0)\). Hence the Frey curve has multiplicative reduction at 2.

See  [ 13 ] , Theorems V.3.1, Remark V.3.1.2 (we don’t need surjectivity), and Theorem V.5.3. This is a lot of work and is a good target for breaking down into many smaller lemmas.

After a quadratic twist we may assume that \(E\) has split multiplicative reduction. The result then follows from the uniformisation theorem and an explicit computation. Note that even if we do not prove surjectivity of Tate’s uniformisation, we still know that it’s surjective on the \(n\)-torsion, because we know that there are \(n^2\) points in the \(n\)-torsion of \(E\) over \(K^{\operatorname{sep}}\), and they are all accounted for by the \(n\)-torsion in \((K^{\operatorname{sep}})^\times /q^{\mathbb {Z}}\).

Indeed, \(E\) has good reduction at \(p\), and hence \(\rho \) is unramified at \(p\) by 3.9.

Apply the explicit formula (presumably already in mathlib)

Indeed \(p\) does not divide \(2^8\) as \(p{\gt}2\), and (using the notation of the previous theorem) \(p\) does not divide \(C^2-AB\) either, because it divides precisely one of \(A\), \(B\) and \(C\). Hence \(v_p(j)=-2v_p(a^\ell b^\ell c^\ell )=-2\ell v_p(abc)\) is a multiple of \(\ell \).

After an unramified quadratic twist we may assume the curve is split at \(p\). The theory of the Tate curve tells us that the extension of \(\mathbb {Q}_p\) cut out by the \(\ell \)-torsion of the Frey curve is \(\mathbb {Q}_p(\mu _\ell ,\sqrt[\ell ]{q})\), with \(\mu _\ell \) the set of \(\ell \)th roots of unity in \(\overline{\mathbb {Q}}_p\). Because \(\ell \not=p\) the extension \(\mathbb {Q}_p(\mu _\ell )\) is unramified at \(p\). And because \(p\not=2\) divides \(abc\), theorem 3.21 shows us that the \(j\)-invariant of the Frey curve has \(p\)-adic valuation a multiple of \(\ell \). Thus the extension can be written \(\mathbb {Q}_p(\mu _\ell ,\sqrt[\ell ]{u})\), where \(u\in \mathbb {Q}_p^\times \) is a unit. The extension is hence unramified (because, for example, Hensel’s Lemma shows that the \(\ell \)th root of \(u\) is in the maximal unramified extension of \(\mathbb {Q}_p\)).

Follows from 3.19 and 3.22.

After a quadratic twist to make the curve have split multiplicative reduction, the theory of the Tate curve shows us that \(\rho \) is an extension of the trivial character by the cyclotomic character. Hence the semisimplification of this representation is the direct sum of two unramified characters and is hence unramified.

The Frey curve either has good reduction at \(\ell \) (case 1 of FLT) or multiplicative reduction at \(\ell \) (case 2 of FLT). In the first case the \(\ell \)-torsion is finite and flat at \(\ell \) by theorem 3.10. In the second case the theory of the Tate curve shows that the \(\ell \)-torsion is (up to quadratic twist) an extension of the trivial character by the cyclotomic character corresponding (via Hilbert 90) to the \(\ell \)th power of an \(\ell \)-adic unit. This extension is known to be finite and flat; see for example Proposition 8.2 of  [ 6 ] . Note that the proof in  [ 6 ] uses fppf cohomology, although one can write down a much more elementary proof of this using arguments in  [ 8 ] .

This follows from the results above. The fact that \(\ell \geq 5\) follows from the definition of a Frey package. The first condition is theorem 3.4, and the second is theorem 3.23. The third condition is theorem 3.24, and the fourth is theorem 3.25.

This is the main theorem of  [ 9 ] . Formalising this result will be a highly non-trivial project; note that this theorem is used in all known proofs of FLT, so there seems to be no way around it.

We have seen in theorem 3.23 that \(\rho \) is unramified at all primes \(p\not=2,\ell \), so the characters \(\alpha \) and \(\beta \) are unramified at all such primes. If \(p=2\) then the semisimplification of the restriction of \(\rho \) to \(\operatorname{Gal}(\overline{\mathbb {Q}}_2/\mathbb {Q}_2)\) is unramified by corollary 3.24, so \(\alpha \) and \(\beta \) are unramified at 2.

In the multiplicative case this follows immediately from the theory of the Tate curve. In the good reduction case, the \(\ell \)-torsion is finite and flat at \(\ell \) by theorem 3.25, so we now need to understand what such representations look like. If the reduction is supersingular, then \(\rho \) is necessarily irreducible, contradicting our assumption. If however the reduction is ordinary, then the theory of the canonical subgroup shows that the \(\ell \)-torsion is an extension of an unramified character by an unramified twist of the cyclotomic character (see Proposition 11 on p273 of  [ 11 ] ).

The previous two theorems show that one of \(\alpha \) and \(\beta \) is a character unramified at all primes, and hence cuts out an extension unramified at all primes, so by Minkowski’s theorem this character is trivial.

Follows from the above.

Indeed, the trivial 1-dimensional submodule is a Galois-invariant subgroup of \(E[\ell ]\), so it corresponds to a Galois-stable point of order \(\ell \).

We have just seen that in this case, the Frey curve has a point of order \(\ell \). It also has three points of order 2, meaning that its torsion subgroup has order at least \(4\ell \geq 20\), contradicting Mazur’s theorem 3.27.

Brian Conrad suggested the following approach, applicable as well for abelian schemes \(A\to S\) over a base. Let \(G\) be a finite locally free \(S\)-subgroup of \(A\), say \(G\) with constant rank \(n {\gt} 0\) by working locally on the base, so \(G\) is contained in \(A[n]\). Then \(n: A \to A\) is the fppf quotient of the source by \(A[n]\), so it expresses \(A\) as an \(A[n]\)-torsor over itself. The problem of building \(A/G\) as an abelian scheme is then seen to be the “same” as that of constructing the quotient of this \(A[n]\)-torsor by the G-action.

In other words, the problem them becomes one having nothing specific to do with abelian schemes, at the cost of working over a base (such as the original target \(A\)) even when \(S\) was the spectrum of a field in the application. The question is now: for a finite locally free commutative \(S\)-group \(H\) and a closed locally free \(S\)-subgroup \(G\), build a reasonable quotient \(H/G\). One approach is to look at the Cartier dual \(H^\vee \to G^\vee \), show that it’s faithfully flat, and then deduce that the Cartier dual of the kernel of this map does the job. Note that one input for this proof is the claim that inclusions of Hopf algebras over fields are flat, proved nicely in Waterhouse’s book.

\(\rho \) has a Galois-stable submodule \(C\). The quotient curve \(E/C\) now has a trivial 1-dimensional submodule, and also three points of order 2 (the images of the three 2-torsion points in \(E\)). Hence the torsion subgroup of \(E/C\) has order at least \(4\ell \geq 20\), again contradicting Mazur’s theorem.

Follows from theorem 3.32, corollary 3.34 and corollary 3.36.