Formalising the statement of Ribet's Lemma

Stream: FLT

[Stepan Nesterov]

I am tring to formalise the following argument for use in the file threeadic.lean :
"Let rho be a 3-adic hardly ramified representation. By ModThree.lean, the reduction of rho is an extension of trivial by cyclo. If rho is irreducible, then by Ribet's lemma (https://people.brandeis.edu/~jbellaic/RibetHawaii2.pdf Prop 1.4, note that this was known in the 1980s), there is an invariant lattice of rho such that the reduction of rho wrt this lattice is a nonsplit extension of cyclo by trivial. This contradicts ModThree.lean. Therefore, rho is reducible. Let rho^ss = chi_1 + chi_2, reduction of chi_1 trivial, reduction of chi_2 cyclo. By the definition of hardly ramified and Kronecker-Weber theorem, chi_1 and chi_2 are trivial and cyclo."
I am facing the following issue:
This informal proof tacitly assumed that rho is over a field. The definition of GaloisRep.IsIrreducible also assumes that the coefficient ring is a field. However, it would be illegal to consider GaloisRep.baseChange (FractionField R) rho, because there is no instance of a topological ring on FractionField R (where R is a finite free Z_3-algebra, which is, say, a local domain). I have at least the following options:

• Try to put an instance of a topological ring on FractionField R is this generality;
• Modify the definition of GaloisRep.IsIrreducible to work over rings (I'm thinking "a representation on a finite free R-module is reducible if it is an extension of two representations on nonzero finite free R-modules");
• Modify the theorem in threeadic.lean and its use in Frey.lean so that it deals with representations over a finite extension of Q_3. Then state and prove by knownin1980s the existence of an invariant lattice, Ribet's lemma and proceed with the proof.
  Which of these options seems easier to do in terms of the formalization work required?

[Michael Rothgang]

Meta point: you can use double dollars $$ around LaTeX code to render it nicely

[Kevin Buzzard]

I guess we're talking about the theorem in FLT/GaloisRepresentation/HardlyRamified/Threeadic.lean. I guess I didn't even put the hypothesis that R is an integral domain in the statement, but one can reduce to this case assuming all kinds of things which are true but not formalized such as if R -> S is a reasonable surjection then the base change of a hardly-ramified rep is hardly-ramified. This feels like a different question to the one you're asking though, so one approach is just to add in the integral domain hypothesis.

Note that, the way I set things up, it doesn't make sense for a Galois rep to GL_2(Q_p) to be hardly ramified, and the reason for this is that the flatness condition as it's currently formalized needs a choice of a lattice, and formally it could be the case that one lattice gives you something flat but another does not. This again isn't really the question you're asking either.

I would just make the base change, assume R is an ID, not attempt to prove that anything is hardly ramified, and put a topology on the field of fractions to make it a GaloisRep.

I think that extending the definition of "irreducible" is dangerous; in my mind no representation of any group on $V:=\mathbb{Z}_p^2$ is ever irreducible, because $pV$ is a nontrivial Galois-stable sub. Your definition is an interesting idea though, but I am a bit scared about it because it's somehow not used in the literature.

I think that modifying the theorem so that it works over Q_3 is also dangerous because this will open up a real can of worms regarding what flatness means.

Here are some proposals for the topology on FractionField R: (1) the Z_3-module topology (2) R is a Z_3-algebra free as a module and local so nonzero, so Frac(R) is a Q_3-algebra. You could use the Q_3-module topology.

The second approach looks far more complicated to me. So this brings us to a mathematics question. Let $K$ be a finite extension of $$\Q_p$$ with its usual topology. Then $K$ is a $\Z_3$-module. Is $K$'s topology the $\Z_3$-module topology?

I think the answer is yes, but I know of no references in the literature to the module topology. The map from Z_p to Q_p is continuous and open, so of_continuous_isOpenMap_algebraMap in FLT/Mathlib/Topology/Algebra/Module/ModuleTopology.lean shows that Q_p has the Z_p-module topology. Certainly K has the Q_p-module topology. Does this then imply that K has the Z_p-module topology? Hmm, I can only see this in FLT under an added finiteness assumption which is not true in our case. But basically I am wondering whether you should just say that Frac(R) gets the Z_3-module topology.

[Stepan Nesterov]

Yea I think it’s easier to just assume everywhere that R is an integral domain for uniformity’s sake. We’re not even constructing the required compatible family and appeal to “knownin1980s”

[Stepan Nesterov]

I don’t think I need to talk about the representation over Q_3 being hardly ramified if I’m taking the first approach, I just want to do a case split by whether it’s irreducible or not

[Stepan Nesterov]

What’s a Z_3-module topology for an infinitely generated Z_3-module?
My first idea for a definition was “decompose $M \otimes \mathbb{Q}_3$ into $M$-cosets and give it the disjoint union topology”

[Kevin Buzzard]

If you move from GaloisRep to Representation then you lose that the action is continuous but you can speak about irreducibility immediately.

[Stepan Nesterov]

But it doesn’t seem to be a standard mathematical construction and I didn’t feel like developing a bunch of API for it

[Stepan Nesterov]

Kevin Buzzard said:

If you move from GaloisRep to Representation then you lose that the action is continuous but you can speak about irreducibility immediately.

Well but can I classify discontinuous Galois characters when it’s reducible into two discontinuous such

[Stepan Nesterov]

Saying $M$ is $\mathbb{Z}_3^n$ so $M \otimes \mathbb{Q}_3$ is $\mathbb{Q}_3^n$ also works mathematically

[Kevin Buzzard]

The Z_3-module topology for an infinitely-generated Z_3-module is just docs#moduleTopology; see the extensive docstring at the top of that file. It would not surprise me if the Z_p-module topology on a finite extension of Q_p was the usual one but I would have to think a little about how best to justify this (if indeed it's true).

Re: irreducibility: if you have a continuous Galois action on a finite-dimensional topological vector space and as an abstract Galois rep it's not irreducible then I bet that the Galois action on the sub and quotient is automatically continuous.

[Stepan Nesterov]

Kevin Buzzard said:

Re: irreducibility: if you have a continuous Galois action on a finite-dimensional topological vector space and as an abstract Galois rep it's not irreducible then I bet that the Galois action on the sub and quotient is automatically continuous.

Well but even if true it requires me to put an instance of a topological space on $M \otimes \mathbf{Q}_3$ anyway

[Stepan Nesterov]

Just to state this fact

[Kevin Buzzard]

For GaloisRep you only need a topology on the coefficient ring, not the module (the module gets the module topology). But in general I am suggesting that you put the Z_3-module topology on M tensor Q_3 and that this will be the same as the Q_3-module topology, but this is only a gut feeling and I don't have time to do the maths right now.

[Stepan Nesterov]

Ah right

[Kevin Buzzard]

Actually I think this might be easy: if R is an open subring of a topological ring A and if A acts on a module M, then the relevant question is which topologies on M make addition on M continuous and also the action of R (or A) continuous. If the action of A is continuous then certainly the action of R is continuous; conversely if the action of R is continuous then because R is open I think this will force the action of A to be continuous because presumably continuity of a ring action can just be checked near a neighbourhood of zero so can be checked on R.

[Kevin Buzzard]

In particular IsModuleTopology.of_continuous_isOpenMap_algebraMap in the FLT repo should probably be beefed-up to say that if R -> A is a continuous open map then the R-module and A-module topologies on an A-module M coincide. The current statement of the result can then be deduced from docs#IsTopologicalSemiring.toIsModuleTopology .

[Stepan Nesterov]

Very interesting topology

[Stepan Nesterov]

Yes so the only question now is if $\mathbb{Z}_3$ is open in $\mathbb{Q}_3$ with its $\mathbb{Z}_3$-module topology

[Stepan Nesterov]

I suppose that the residue field of R also carries the R-module topology. And I deduce that it is discrete from the fact that the quotient maps between modules are open and the maximal ideal of R is open.
Neat

[Kevin Buzzard]

Stepan Nesterov said:

Yes so the only question now is if $\mathbb{Z}_3$ is open in $\mathbb{Q}_3$ with its $\mathbb{Z}_3$-module topology

This is true because the Z_3-module topology on Q_3 is the Q_3-module topology which is Q_3's topology.

[Stepan Nesterov]

Can I just assume by knownin1980s that in a compatible family of representations, if one representation is reducible, then so is every other representation?
This would massively simplify the work in Threeadic.lean and Frey.lean. I just say that the 3-adic representation is reducible by the Ribet's lemma argument, and therefore the p-adic representation in the same family is reducible.

[Stepan Nesterov]

Ok I tried formalizing it and the way compatible families are currently set up would only give me that the p-torsion of the Frey curve is geometrically reducible

[Kevin Buzzard]

Stepan Nesterov said:

Can I just assume by knownin1980s that in a compatible family of representations, if one representation is reducible, then so is every other representation?

What's the maths proof?

My instinct at this point is: if you can knock of a maths proof which is a paragraph long and uses only things known in the 1980s, then sure. But I can only prove "if one repn has trace equal to 1+cyclo then they all do".

[Kevin Buzzard]

Stepan Nesterov said:

Ok I tried formalizing it and the way compatible families are currently set up would only give me that the p-torsion of the Frey curve is geometrically reducible

Because p>=3 you can use complex conjugation to prove geom red iff red.

[Stepan Nesterov]

Kevin Buzzard said:

Stepan Nesterov said:

Can I just assume by knownin1980s that in a compatible family of representations, if one representation is reducible, then so is every other representation?

What's the maths proof?

My instinct at this point is: if you can knock of a maths proof which is a paragraph long and uses only things known in the 1980s, then sure. But I can only prove "if one repn has trace equal to 1+cyclo then they all do".

I meant "compatible family of 2-dimensional representations"
By [Serre, "Abelian l-adic Representations and Elliptic Curves, III.3] any 1-dimensional l-adic rep of G_Q is cyclo^n times chi for a Dirichlet character chi. Then you do the same: one rep has trace(Frob_p) = p^n chi(p) + p^m psi(p), hence all of them do, hence all of them are cyclo^n times chi + cyclo^m times psi.

[Kevin Buzzard]

Yeah LGTM!

[Stepan Nesterov]

Are there any objections (mathematical or Lean) to changing the definition of a compatible family from "for all embeddings $\phi : E \to \overline{\mathbb{Q}_p}$ there is a representation to $\overline{\mathbb{Q}_p}$" to "for all finite places $v$ of $E$ there is a representation to $E_v$"? Then I could formalize the preceding proof much more naturally instead of running into this irreducible vs. geometrically irreducible situation.

[Stepan Nesterov]

Kevin Buzzard said:

Note that, the way I set things up, it doesn't make sense for a Galois rep to GL_2(Q_p) to be hardly ramified, and the reason for this is that the flatness condition as it's currently formalized needs a choice of a lattice, and formally it could be the case that one lattice gives you something flat but another does not.

An update on this: the proof of "every 3-adic hardly ramified representation is reducible" does in fact rely on this independence of lattice fact. I have currently formalised its statement (and proof, under some definition of proof) like this:

theorem hardlyRamified_of_hardlyRamified_isogenous {ℓ : ℕ} [Fact ℓ.Prime] (hℓOdd : Odd ℓ)
    {R : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsLocalRing R]
    [IsDomain R] [Algebra ℤ_[ℓ] R]
    {V : Type*} [AddCommGroup V] [Module R V]
    [Module.Finite R V] [Module.Free R V] (hdimV : Module.rank R V = 2)
    {W : Type*} [AddCommGroup W] [Module R W]
    [Module.Finite R W] [Module.Free R W] (hdimW : Module.rank R W = 2)
    (ρ : GaloisRep ℚ R V) (σ : GaloisRep ℚ R W)
    (e : (FractionRing R) ⊗[R] V ≃ₗ[FractionRing R] (FractionRing R) ⊗[R] W)
    (he : GaloisRep.conj (GaloisRep.baseChange (FractionRing R) ρ) e =
      (GaloisRep.baseChange (FractionRing R) σ)) :
    IsHardlyRamified hℓOdd hdimV ρ ↔ IsHardlyRamified hℓOdd hdimW σ := knownin1980s

[Kevin Buzzard]

Stepan Nesterov said:

Are there any objections (mathematical or Lean) to changing the definition of a compatible family from "for all embeddings $\phi : E \to \overline{\mathbb{Q}_p}$ there is a representation to $\overline{\mathbb{Q}_p}$" to "for all finite places $v$ of $E$ there is a representation to $E_v$"? Then I could formalize the preceding proof much more naturally instead of running into this irreducible vs. geometrically irreducible situation.

What worries me about this definition is that there's an implied descent ("if the char polys are in a smaller field then the rep descends to the smaller field") which I know isn't true in general (the rep could take values in the units of a quaternion algebra defined over the smaller field rather than in GL_2; this caught Cremona out once when he spent some time looking for an elliptic curve over $\mathbb{Q}(i)$ when it turned out that the representation was the Tate module of some abelian surface with quaternionic multiplication). I think that for totally real fields you might be OK because of some argument involving complex conjugation though. Having said all that, my instinct is that rather than opening this can of worms this might be a good excuse for proving basic undergraduate-level results about irreducibility (which we need anyway).

[Stepan Nesterov]

Kevin Buzzard said:

Stepan Nesterov said:

Are there any objections (mathematical or Lean) to changing the definition of a compatible family from "for all embeddings $\phi : E \to \overline{\mathbb{Q}_p}$ there is a representation to $\overline{\mathbb{Q}_p}$" to "for all finite places $v$ of $E$ there is a representation to $E_v$"? Then I could formalize the preceding proof much more naturally instead of running into this irreducible vs. geometrically irreducible situation.

What worries me about this definition is that there's an implied descent ("if the char polys are in a smaller field then the rep descends to the smaller field") which I know isn't true in general (the rep could take values in the units of a quaternion algebra defined over the smaller field rather than in GL_2; this caught Cremona out once when he spent some time looking for an elliptic curve over $\mathbb{Q}(i)$ when it turned out that the representation was the Tate module of some abelian surface with quaternionic multiplication). I think that for totally real fields you might be OK because of some argument involving complex conjugation though. Having said all that, my instinct is that rather than opening this can of worms this might be a good excuse for proving basic undergraduate-level results about irreducibility (which we need anyway).

Right, but you can always just enlarge $E$ to contain a splitting field of that quaternion algebra, so it doesn't really affect the property of a given representation $\rho$ to spread out into a compatible family.

[Stepan Nesterov]

But I guess it might be nice to talk about a compatible family with minimal $E$ sometimes, even if not for FLT, so I went the "odd 2-dimensional irreducible Galois rep is absolutely irreducible" route in the end