Hardly ramified representations
Let \((a,b,c,p)\) be a Frey package (so in particular \(p\geq5\) is prime and \(a^p+b^p=c^p\)), let \(E\) be the corresponding Frey curve over \(\mathbb{Q}\), and let \(\rho:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{Aut}(E(\overline{\mathbb{Q}})[p])\) be the 2-dimensional Galois representation on the \(p\)-torsion of \(E\). Recall that our goal is to prove that \(\rho\) is reducible.
What we need to leverage is the fact that \(\rho\) has very little ramification. To give a toy example before we start: if \(K\) is a number field (i.e., a finite extension of \(\mathbb{Q}\)) and if the extension \(K/\mathbb{Q}\) is unramified at all primes, then an old theorem of Minkowski tells us that \(K=\mathbb{Q}\). We want to prove a theorem in a similar vein, namely that if a 2-dimensional mod \(p\) Galois representation is “hardly ramified”, then it is reducible. Below, we give a precise definition of what it means for a continuous 2-dimensional representation \(\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(R)\) to be hardly ramified. Before we do that, we need to say precisely which topological rings \(R\) we will allow. We say that a topological ring is emphpro-Artinian if it is a projective limit of Artin local rings each equipped with the discrete topology, and if it has the projective limit topology. We are only concerned with local pro-Artinian rings with finite residue field; such things can be checked to be the same thing as topological local rings with finite residue field whose underlying topological space is profinite, and such that additive translates of open ideals form a basis for the topology. Let us call such rings “coefficient rings” for now.
Remark. We make some remarks to orient the reader.
- Any complete local Noetherian ring with finite residue field is a coefficient ring, if the ring is equipped with the \(\mathfrak{m}\)-adic topology where \(\mathfrak{m}\) is the maximal ideal. In this case, all powers of \(\mathfrak{m}\) are open.
- In particular finite fields, and integer rings of finite extensions of \(\mathbb{Q}_p\), are coefficient rings.
- If \(R\) is a coefficient ring then \(R\) is isomorphic to the projective limit of the finite rings \(R/I\) as \(I\) runs over the open ideals of \(R\).
- A non-Noetherian example of a coefficient ring is the projective limit over \(n\) of the rings \(\mathbb{Z}/p\mathbb{Z}[\varepsilon_1,\ldots,\varepsilon_n]/(\forall i,j,\varepsilon_i\varepsilon_j=0)\); these rings are convenient to include as coefficient rings for technical reasons; they make representability theorems easier.
- The category of coefficient rings is equivalent to the pro-category of the category of finite local rings.
- A coefficient ring is pseudocompact in the sense of Grothendieck. A pseudocompact local ring is however a more general concept as such a thing may have an infinite residue field and would thus not be profinite.
- If \(R\) is a coefficient ring with residue field of characteristic \(\ell\), then there is a unique continuous map \(\mathbb{Z}_\ell\to R\). Indeed, it suffices to prove that there is a unique continuous map \(\mathbb{Z}_\ell\to R/I\) for each open ideal \(I\), but \(R/I\) is a finite local ring with residue field of characteristic \(\ell\). \(R/I\) is hence Artinian, so some power of the maximal ideal is zero by Nakayama. This means that \(\ell^N=0\) for some sufficiently large \(N\), and hence \(R/I\) is a \(\mathbb{Z}/\ell^N\mathbb{Z}\)-algebra and thus admits admits a unique map from \(\mathbb{Z}_\ell\).
- It will be more convenient to fix once and for all the integer \(\mathcal{O}\) in a finite extension of \(\mathbb{Q}_\ell\) and consider “coefficient \(\mathcal{O}\)-algebras”, namely coefficient rings \(R\) equipped with a continuous map \(\mathcal{O}\to R\) which is a local homomorphism inducing an isomorphism on residue fields.
Because a coefficient ring \(R\) with residue field of characteristic \(\ell\) is naturally a \(\mathbb{Z}_\ell\)-algebra, we can talk about the \(\ell\)-adic cyclotomic character \(\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to R^\times\). We are now ready to define hardly ramified representations.
Definitionhardly_ramified#
Let \(R\) be a coefficient ring with finite residue field of characteristic \(\ell\geq3\). Let \(V\) be a finite free \(R\)-module of rank 2, equipped with the product topology. A continuous representation \(\rho: \operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to \operatorname{GL}_R(V)\) is said to be hardly ramified if it satisfies the following four conditions:
- \(\det(\rho):\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to R^\times\) is the cyclotomic character;
- \(\rho\) is unramified outside \(2\ell\);
- The restriction of \(\rho\) to \(\operatorname{Gal}(\overline{\mathbb{Q}}_2/\mathbb{Q}_2)\) is reducible (more precisely, there is a short exact sequence \(0\to R\to V\to R\to 0\) which is stable under the action of \(\operatorname{Gal}(\overline{\mathbb{Q}}_2/\mathbb{Q}_2)\)) and the Galois action on the 1-dimensional quotient is an unramified representation of \(\operatorname{Gal}(\overline{\mathbb{Q}}_2/\mathbb{Q}_2)\) whose square is trivial;
- The restriction of \(\rho\) to \(\operatorname{Gal}(\overline{\mathbb{Q}}_\ell/\mathbb{Q}_\ell)\) is flat, by which we mean that for all open ideals \(I\) of \(R\), the (finite image) representation \(\rho\) mod \(I:\operatorname{Gal}(\overline{\mathbb{Q}}_\ell/\mathbb{Q}_\ell)\to \operatorname{GL}_{R/I}(V/I)\) comes from a finite flat group scheme.
A well-known result, which basically goes back to Frey, is the following:
TheoremFrey_curve_hardly_ramified#
The \(\ell\)-torsion \(\rho:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(\mathbb{Z}/\ell\mathbb{Z})\) in the Frey curve associated to a Frey package \((a,b,c,\ell)\) is hardly ramified.
Proof
This was well-known in the 1980s. A proof sketch is as follows. First note that \(\ell\geq5>3\) by definition of a Frey package. Let \(\rho\) denote the Galois representation on the \(\ell\)-torsion of the Frey curve. The fact that \(\rho\) is 2-dimensional is Corollary III.6.4(b) of (Silverman 2009), and the fact that its determinant is cyclotomic is Proposition III.8.3 of the same reference. These results hold for elliptic curves in general. The remaining claims are specific to the Frey curve and lie deeper. The fact that \(\rho\) is unramified outside \(2\ell\) is a consequence of (4.1.12) and (4.1.13) of (Serre 1987). The fact that \(\rho\) at 2 has an unramified 1-dimensional quotient of order at most 2 follows from the fact that the Frey curve is semistable at 2 (see (4.1.5) of (Serre 1987)) and the theory of the Tate curve. Finally, the claim that \(\rho\) is flat at \(\ell\) is Proposition 5 and (4.1.13) of (Serre 1987).
Lean
Stated as FreyCurve.torsion_isHardlyRamified; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
Note that irreducibility and absolute irreducibility for hardly ramified mod \(\ell\) representations are the same, because our assumptions that \(\ell\geq3\) and that the determinant is cyclotomic imply that the image of complex conjugation has distinct eigenvalues defined over the ground field.
The key theorem about hardly ramified representations is the following.
Theoremhardly_ramified_reducible#
If \(\ell\geq 3\) is a prime and \(\rho:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(\mathbb{Z}/\ell\mathbb{Z})\) is hardly ramified, then \(\rho\) is reducible.
Proof
Assume for a contradiction that \(\overline{\rho}\) is irreducible. By theorem hardly_ramified_lifts, \(\overline{\rho}\) lifts to a hardly ramified \(\ell\)-adic reprepresentation \(\rho\). By theorem hardly_ramified_spreads_out, \(\rho\) is part of a compatible family of \(q\)-adic Galois representations. By theorem hardly_ramified_3adic_reducible, any 3-adic member \(\rho_3\) of this family has semisimplification \(1\oplus\chi_3\) and in particular for \(p\nmid 6\) we have that the characteristic polynomial of \(\rho_3(\operatorname{Frob}_p)=(X-p)(X-1).\) By compatibility of the family we deduce that for \(p\nmid 6\ell\) the characteristic polynomial of \(\rho(\operatorname{Frob}_p)\) is \((X-p)(X-1)\), and thus the characteristic polynomial of \(\overline{\rho}(\operatorname{Frob}_p)\) is \((X-p)(X-1)\). By the Cebotarev density theorem, \(\overline{\rho}\) and \(1\oplus\chi\) have the same characteristic polynomials everywhere (here \(\chi\) is the mod \(\ell\) cyclotomic character). Thus by the Brauer-Nesbitt theorem, \(\overline{\rho}\) is reducible, the contradiction we seek.
Lean
Stated as FreyCurve.torsion_not_isIrreducible; the blueprint marks no proof of it as formalized.
Sources
Uses 3 · Used by 1
Note that this (deep) claim is a consequence of Serre's conjecture (Serre 1987), now a theorem of Khare and Wintenberger (Khare and Wintenberger 2009), and indeed we shall use methods introduced by Khare and Wintenberger to prove this special case of Serre's conjecture. Given this result, we can deduce Theorem Wiles,Taylor–Wiles, Ribet,… (which we restate here) easily:
TheoremWiles_Frey_again#
If \(\overline{\rho}\) is the mod \(p\) Galois representation associated to a Frey package \((a,b,c,p)\) then \(\overline{\rho}\) is reducible.
Proof
Indeed, \(\rho\) is hardly ramified by theorem Frey_curve_hardly_ramified and thus reducible by theorem hardly_ramified_reducible.
Lean
Stated as FLT.Bosses.B4_proof; the blueprint marks no proof of it as formalized.
Sources
Uses 2
Our job of reducing FLT to theorems of the 1980s is hence reduced to proving Theorem hardly_ramified_reducible.
Hardly ramified mod \(p\) representations are reducible
In this section we will state three theorems, from which Theorem hardly_ramified_reducible easily follows.
Firstly, we claim that an irreducible hardly ramified mod \(\ell\) representation lifts to an \(\ell\)-adic representation.
Theoremhardly_ramified_lifts#
If \(\ell\geq3\) is prime and \(\overline{\rho}:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(\mathbb{Z}/\ell\mathbb{Z})\) is hardly ramified and irreducible, then there exists a finite extension \(K\) of \(\mathbb{Q}_\ell\) with integer ring \(\mathcal{O}\) and maximal ideal \(\mathfrak{m}\) and a hardly ramified representation \(\rho:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(\mathcal{O})\) whose reduction modulo \(\mathfrak{m}\) is isomorphic to \(\rho\).
Proof
Omitted for now TODO
Lean
Stated as GaloisRepresentation.IsHardlyRamified.lifts; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
Next we claim that a hardly ramified \(\ell\)-adic representation “spreads out” to a compatible family of hardly ramified \(q\)-adic representations for all odd primes \(q\) (note that we have not made a definition of a hardly ramified 2-adic representation).
Theoremhardly_ramified_spreads_out#
If \(\ell\geq3\) is prime, \(K\) is a finite extension of \(\mathbb{Q}_\ell\) with integers \(\mathcal{O}\) and if \(\rho:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(\mathcal{O})\) is a hardly ramified representation whose reduction is irreducible, then there exists a number field \(M\) and, for each finite place \(\mu\) of \(M\) of characteristic prime to 2, with completion \(M_\mu\) having integer ring \(R_\mu\), a hardly ramified semisimple representation \(\rho_\mu:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(R_\mu)\) (by which we mean the generic fibre is semisimple), with the following properties:
- There is some \(\lambda\mid\ell\) of \(M\) such that \(\rho_\lambda\cong\rho\), the isomorphism happening over some appropriate local field containing a copy of \(M_\lambda\) and a copy of \(K\);
- If \(\mu_1\) and \(\mu_2\) are two finite places of \(M\) with odd residue characteristics \(m_1\) and \(m_2\), and if \(p\nmid 2m_1m_2\) is prime, then \(\rho_{\mu_1}\) and \(\rho_{\mu_2}\) are both unramified at \(p\) and the characteristic polynomials \(\rho_{\mu_1}(\operatorname{Frob}_p)\) and \(\rho_{\mu_2}(\operatorname{Frob}_p)\) lie in \(M[X]\) and are equal.
Proof
Omitted for now TODO
Lean
Stated as GaloisRepresentation.IsHardlyRamified.mem_isCompatible; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
In particular, we can “move” from an irreducible hardly ramified mod \(\ell\) representation to a hardly ramified 3-adic representation, and hence to a hardly ramified mod 3 representation.
However, we can essentially completely classify the hardly ramified mod 3 Galois representations:
Theoremhardly_ramified_mod3_reducible#
Suppose \(k\) is a finite field of characteristic 3, and suppose \(\overline{rho}:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(k)\) is hardly ramified. Then \(\overline{\rho}\) is an extension of the cyclotomic character by the trivial representation.
Proof
Omitted for now. TODO
Lean
Stated as GaloisRepresentation.IsHardlyRamified.mod_three; the blueprint marks no proof of it as formalized.
Sources
Uses 1 · Used by 1
And we can use this to essentially completely classify the hardly ramified 3-adic Galois representations:
Theoremhardly_ramified_3adic_reducible#
Suppose \(L/\mathbb{Q}_3\) is a finite extension, with integer ring \(\mathcal{O}_L\), and suppose \(\rho_3:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(\mathcal{O}_L)\) is hardly ramified. Then (considered as a representation to \(\operatorname{GL}_2(L)\)) \(\rho_3^{ss}=1\oplus\chi_3\) where \(1\) is the trivial character and \(\chi_3\) is the 3-adic cyclotomic character.
Proof
Omitted for now TODO
Lean
Stated as GaloisRepresentation.IsHardlyRamified.three_adic; the blueprint marks no proof of it as formalized.
Sources
Uses 2 · Used by 1
Theorem hardly_ramified_reducible (if \(\ell\geq 3\) is a prime and \(\overline{\rho}:\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to\operatorname{GL}_2(\mathbb{Z}/\ell\mathbb{Z})\) is hardly ramified, then \(\overline{\rho}\) is reducible) is an easy consequence of these theorems, as we now show.
The proof of Theorem hardly_ramified_reducible is shown with its statement.
What remains then (modulo several results which were known in the 1980s), is to prove the three theorems hardly_ramified_lifts, hardly_ramified_spreads_out and hardly_ramified_3adic_reducible. By far the easiest is theorem hardly_ramified_3adic_reducible; this follows from old estimates of Fontaine (ultimately relying on bounds for root discriminants due to Odlyzko and Poitou), originally developed to prove that there was no nontrivial abelian scheme over \(\mathbb{Z}.\) The other two theorems are deeper, and both use modern variants of Wiles' \(R=T\) machinery.
We have not yet written any more LaTeX on how to proceed further; the rest of this blueprint should be considered as more unfocussed thoughts.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.