Hardly ramified representations

Stream: FLT

[Kevin Buzzard]

@Stepan Nesterov in FLT#742 I start the work of writing down the statements of nontrivial theorems about hardly ramified Galois representations.

Here are some mathematical questions. After years of formalization I am becoming far more attuned to the idea of writing down "the correct statement" as opposed to "a statement which suffices". Here are some questions.

Richard proves in his course that if $\rho$ is a hardly ramified represention with coefficient ring a finite field of characteristic 3, then $\rho$ is has a trivial 1-dimensional quotient. Do you think that it's true that if $\rho$ is a hardly ramified representation with coefficient ring a finite $\mathbb{F}_3$-algebra then $\rho$ has a trivial 1-dimensional quotient? Just to be clear, I mean that Galois acts on $V$ free of rank 2 over a finite $\mathbb{F}_3$-algebra $R$ and I'm suggesting that we have $0\to R(1)\to V\to R\to 0$. Maybe we need $R$ reduced? (actually reduced probably implies $R$ is a finite direct sum of fields, so here you're fine).

Richard also proves in his course that if $\rho$ is a hardly ramified 3-adic representation, by which I mean a representation to $GL_2(R)$ with $R$ the integers in a finite extension $K$ of $\mathbb{Q}_3$, then $(\rho\otimes K)^{ss}$ is $K(1)\oplus K$. I am pretty sure that the methods prove that $0\to K(1)\to \rho\otimes K\to K\to 0$. Is it true that $0\to R(1)\to \rho\to R\to 0$? Furthermore, is this claim true for $R$ a finite free $\Z_3$-algebra? Maybe reduced?

In short: what are the actual theorems that one should be proving here?

[Kevin Buzzard]

OK I couldn't really let go of this and thought a bit more about it (after attempting to pass it on). I think that Theorem A of Fontaine's "no ab var / Z" still gives you that G^{3/2} acts trivially in the case where R is a finite F_3-algebra; no reducedness necessary. In his course Richard attempts to prove the cases of Fontaine's theorem which he needs directly, but I am happy to defer to Fontaine (avoiding Fontaine will mean classifying finite flat reps over R a la Fontaine's thesis so it's not really saving any work, and anyway the plan was to always assume Fontaine).

As for the 3-adic case; Richard in his course didn't rule out 0->K->rho->K(1)->0 but I think the methods do (Richard didn't need to rule it out, all he needed was rho^ss=1+cyclo); if the trivial were the sub and the extension really was nonsplit then I think you can find an appropriate lattice and reduce mod 3 and contradict the mod 3 result. So "trivial is a quotient" is true if R is a finite extension K of Q_p (one has to be slightly careful here because "flat" doesn't make sense until you choose an integral model, but flatness is a property of the generic fibre so it's independent of the choice of mode). Next, the same thing is true for R the integers of K, because the quotient K^2->K induces a map R^2->(something isomorphic to R) and the kernel must be R too as the quotient splits as R-modules. For R a general order in K, what do f.g. R-submodules of K look like (K is still a finite extension of Q_3)? I ask because that's what we know about the image of R^2. Are they all isomorphic to R as R-modules? If not then this idea is probably dead in the water. Hmm, if R is not integrally closed then presumably it can't be a PID which presumably means that there can be non-free R-ideals? Does this sound right? So are we doomed to focus on integrally-closed R-modules? Or maybe my definition of "rank 1 quotient" is wrong and it shouldn't demand that the quotient is free rank 1?

[Bryan Wang]

Probably the conductor ideal of a non-maximal order gives an example of a non-invertible ideal? Or maybe I'm remembering wrongly

[Kevin Buzzard]

Aah -- maybe this question is irrelevant though? Because the definition of hardly ramified (here in LaTeX) implies that V locally at 2 has a free rank 1 sub and a free rank 1 quotient, and those pieces are not congruent mod p so I suspect that the local filtration is unique, which maybe means that it must be the global filtration?

I think here's the general question for orders, although the question after that is "for what rings R does the proof which is yet to be written down, work?"

Let R be an order in a finite extension K of Q_p, so R is a finite free Z_p-algebra.

Say G is a group and D is a subgroup (in the application G is global Galois and D is decomp at 2). Say chi1 and chi2 are two maps G -> Z_p^* which, when restriced to D, are distinct mod p .

Say V is a finite free rank 2 R-module with an action of G, such that when restriced to D there's a short exact sequence 0->R(chi1)->V->R(chi2)->0 of D-modules.

Say that V tensor_R K admits a short exact sequence 0->K(chi1)->V_K->K(chi2)->0 of G-modules.

Does V admit a short exact sequence 0->R(chi1)->V->R(chi2)->0?

[Bryan Wang]

I'm not sure how helpful this is, but e.g. Remark 1.1 of these notes on Ribet's lemma seems to suggest the order of extension can be exchanged, so in this full generality, the subgroup D is probably the crucial one.

[Kevin Buzzard]

This is only true when you're globally irreducible. Here we're globally reducible and there's a genuine asymmetry.

[Kevin Buzzard]

In fact in some sense this is the proof of the implication "mod 3 hardly ramified => trivial quotient" => "3-adic hardly ramified => trivial quotient". Try as you might you can't find that second lattice which mod 3 is "the other way up", but which Ribet says always exists if the generic fibre is irreducible.

In fact Richard in his course uses the same ideas as the ones in Serre's proof.

[Stepan Nesterov]

Kevin Buzzard said:

Do you think that it's true that if $\rho$ is a hardly ramified representation with coefficient ring a finite $\mathbb{F}_3$-algebra then $\rho$ has a trivial 1-dimensional quotient.

Definitely yes. I think the morally correct theorem underlying the argument is in Schoof's paper: any 3-divisible group scheme over Z[1/2], where I_2 acts unipotently of echelon 2, is an extension of a diagonalizable by constant.

[Stepan Nesterov]

Kevin Buzzard said:

Richard in his course didn't rule out 0->K->rho->K(1)->0 but I think the methods do (Richard didn't need to rule it out, all he needed was rho^ss=1+cyclo); if the trivial were the sub and the extension really was nonsplit then I think you can find an appropriate lattice and reduce mod 3 and contradict the mod 3 result.

That is actually a necessary part of Schoof's argument!
I think what Richard does with Zorn's lemma is hopelessly wrong, actually: definitely S_3 has a representation which is irreducible in char 0 but reducible mod 3. If you only know you are reducible mod 3, how do you get reducible mod 9, 27, etc?
The way it's stated in Daniel's notes I think the mistake is that he considers the map \Lambda \to (\mathcal{O} / \pi)^2 and like yea you can take the lattice \mathcal{O} + 3\mathcal{O} and the image of the map is 1-dimensional, that doesn't prove that Lambda is rank 1.

[Stepan Nesterov]

I am working on the write-up of the correct argument which will be a Taylor/Schoof amalgamation. The idea is to note that the mod 3 result gives you as a corollary that there are no exts of mu_3 by Z/3 which are hardly ramified, then you take rho mod 3^k, take its Jordan-Holder series, move all the mu_3 factors to the left by this, and conclude that it's an extension of Z/3^k by mu_3^k. All of this requires Raynaud's theorem that finite flat group schemes over Z_3 form an abelian category, but that's 1970s.

[Stepan Nesterov]

Hardly_ramified.pdf
Actually here's my highly unpolished preliminary version of the argument

[Stepan Nesterov]

Bryan Wang said:

I'm not sure how helpful this is, but e.g. Remark 1.1 of these notes on Ribet's lemma seems to suggest the order of extension can be exchanged, so in this full generality, the subgroup D is probably the crucial one.

Oh wait

[Stepan Nesterov]

This Ribet's lemma would give a one-line proof of the implication "mod 3 hardly ramified reducible" => "3-adic hardly ramified reducible"

[Stepan Nesterov]

Because we can observe from the proof of the former that the wrong way extensions do not actually occur

[Stepan Nesterov]

Was Ribet's lemma known in the 1980s? Is it from his converse to Herbrand paper by any chance?

[Bryan Wang]

Kevin Buzzard said:

This is only true when you're globally irreducible. Here we're globally reducible and there's a genuine asymmetry.

Ah yeah right, my bad! I got confused here

[Bryan Wang]

Stepan Nesterov said:

Was Ribet's lemma known in the 1980s? Is it from his converse to Herbrand paper by any chance?

The original paper by Ribet is from the 70s I think

[Stepan Nesterov]

Ok so then can we just assume Ribet’s lemma as an axiom and conclude that a 3-adic hardly ramified rep is reducible?

[Stepan Nesterov]

It probably doesn’t give you the stronger statement that an ext in the wrong order splits and probably doesn’t work over arbitrary finite Z_3-algebra, but we don’t really need to worry about that for FLT

[Stepan Nesterov]

The argument I outlined in the pdf above does do all of these things but it is a fair bit longer

[Kevin Buzzard]

This whole thing made me temporaily worry today about whether for "random" R the correct local or global deformation condition really should be "there's a G-equivariant map R^2 -> R" (where G acts via rho on R^2 and trivially on R) or whether we should be more liberal about what kind of quotients to allow. I remembered from Mazur's work that this definitely should work but I was also confused about what happened if R wasn't integrally closed so I kind of had a contradiction in maths, especially when I convinced myself that if $A\subseteq R$ then the image of $A^2$ in some random $R$-linear map $R^2\to R$ definitely might not be isomorphic to $A$, which if I could beef up into an explicit $G$-rep would contradict one of the axioms Mazur needed for subdeformations. I knew that the mistake had to be my hunch that "I have a free rank 1 quotient" didn't descend but it took me multiplying out a bunch of matrices with coefficients in $\Z_3[3i]$ before I realised that my "counterexample" couldn't be made. In short you totally can have $A\subseteq R$ and an $R$-linear map $R^2\to R$ which doesn't descend to $A^2\to A$ and instead becomes $A^2\to$ (random non-free thing) but this map can't be $\phi$-equivariant if $\phi$ is an endomorphism of $A^2$ which when extended to $R^2$ is acting by eigenvalues on the sub and quotient $R$ which are not congruent mod max ideal.

Ribet's lemma can be assumed but morally Ribet's lemma is dead easy, you just conjugate by $(\pi,0;0,1)$ until you make the bottom left hand entry nonzero. If we assume anything Schoofy then it has to be pre-1990; my plan was to get the result from Fontaine which is 1985 (and would actually be a really interesting project to do in Lean but we're a long way from it yet, I am not sure if we have upper numbering and we have essentially nothing about flat Galois reps other than the definition).

[Kevin Buzzard]

Stepan Nesterov said:

I think what Richard does with Zorn's lemma is hopelessly wrong, actually: definitely S_3 has a representation which is irreducible in char 0 but reducible mod 3. If you only know you are reducible mod 3, how do you get reducible mod 9, 27, etc?

Ha ha this is the guy who told me he knew a complete proof ;-) I didn't read Richard's argument in Daniel's notes because I knew the argument myself. What does "reducible mod 9" even mean? Every rep is "reducible mod 9" in some sense because the 3-torsion is a stable sub.

[Kevin Buzzard]

Stepan Nesterov said:

This Ribet's lemma would give a one-line proof of the implication "mod 3 hardly ramified reducible" => "3-adic hardly ramified reducible"

given that we now seem to have established that the correct generality for the coefficient ring in the mod 3 result is "arbitrary finite free $\mathbb{F}_3$-algebra" I am now interested in what the correct generality for the coefficient ring should be in the 3-adic result. Is "Arbitrary finite free $\Z_3$-algebra" too much to hope for? We have a quotient $R^2\to R$ locally at 2 and the game is to show that this is also a global quotient. I think we're all convinced that it works for $R$ the integers of a finite extension of $\mathbb{Q}_p$ but maybe the right proof works far more generally. Basically I am interested in investigating this concept of a hardly ramified representation (which I should say Richard suggested to me in an email, it's not my idea, but I think it's worth developing an API for).

One reason I am thinking about this is that I've often wondered what the right framework for compatible families of ell-adic Galois reps is. Instead of saying "there's some number field M and M_lambda-adic reps for all lambda" you can work with reps to $M\otimes_{\mathbb{Q}}\mathbb{Q}_p$ (a sum of the M_lambda for lambda dividing p) and then you're beginning to think what the point of introducing M in the first place is, maybe there's just some finite free Z-algebra lurking (basically the Hecke algebra over Z) and you just p-adically complete this, invert p and consider Galois reps into GL_2 of this ring instead as p varies.

[Kevin Buzzard]

Stepan Nesterov said:

Hardly_ramified.pdf
Actually here's my highly unpolished preliminary version of the argument

I think Prop 2 is in Tate's "p-divisible groups" paper from the 60s. Richard only gives a direct argument for Prop 5 assuming basically a classification of ffgs. If Theorem 12 is true then is it true that if R is any (module-)finite $\Z_3$-algebra then any hardly ramified rep $V/R$ lives in a short exact sequence 0->R(1)->V->R->0? I'm hoping that this has a cute devissage proof (using only that cyclo != 1 mod 3) if we know it for finite $\mathbb{F}_3$-algebras.

Hmm, you're telling me that it's not as easy as that because of the S_3 example :-/

[Stepan Nesterov]

Kevin Buzzard said:

What does "reducible mod 9" even mean?

What I meant to say is "the 3-adic representation is conjugate to a 3-adic representation such that the lower left corner is always divisible by 9"

[Stepan Nesterov]

Kevin Buzzard said:

If Theorem 12 is true then is it true that if R is any (module-)finite $\Z_3$-algebra then any hardly ramified rep $V/R$ lives in a short exact sequence 0->R(1)->V->R->0? I'm hoping that this has a cute devissage proof (using only that cyclo != 1 mod 3) if we know it for finite $\mathbb{F}_3$-algebras.

Yea I feel like Schoof's argument should be strong enough to give you that.

[Stepan Nesterov]

It's just a bit painful to think about because I think you can probably techically consider a nontrivial extension of Z/3 by mu_3 as a 1-dimensional F_3[eps]/eps^2 Galois representation or something

[Stepan Nesterov]

I would like to do something like this:
Represent your 3-divisible group as an extension of a constant by diagonalisable. If there is an action of a Z_3-algebra R on this object then because there is no hom from diagonalisable to constant, the diagonalisable has to be an R-submodule.

[Stepan Nesterov]

But then of course if your R is Z_3[eps]/eps^2 who's to say that this sub is not just eps*Z_3[eps]/eps^2?

[Notification Bot]

29 messages were moved here from #FLT > Next steps in the formalization by Kevin Buzzard.

[Kevin Buzzard]

@Stepan Nesterov I moved the discussion to a thread with a more representative title. I have also merged two files https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/GaloisRepresentation/HardlyRamified/ModThree.lean and https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/GaloisRepresentation/HardlyRamified/Threeadic.lean so now you have some concrete statements to try proving.

[Stepan Nesterov]

By the way, this argument maybe works for R finite Z_3 algebra which is an integral domain.
For a hardly ramified rep G_Q \to GL_2(R), define a subomdule of cyclotomic vectors to be {v in R^2 : for any g in G_Q, gv = chi(g)v}. This is nonzero because it is nonzero mod any ideal of finite index by Schoof + completeness. Note that if av is cyclotomic, then v also is. So R/(cyclotomic vectors) is torsion free, and I hope this is enough to imply that (cyclotomic vectors)=R and the quotient is R

[Stepan Nesterov]

In

import FLT.GaloisRepresentation.HardlyRamified.Defs
import FLT.Deformations.RepresentationTheory.EllipticCurve
import FLT.Basic.Reductions

variable (P : FLT.FreyPackage)

open GaloisRepresentation

theorem FLT.FreyPackage.FreyCurve.torsion_isHardlyRamified :
    have : Fact (P.p.Prime) := sorry
    let : Algebra ℤ_[P.p] (ZMod P.p) := sorry
    have : Module.Finite (ZMod P.p) (P.freyCurve.n_torsion P.p) := sorry
    IsHardlyRamified (show Odd P.p from sorry) sorry
      (P.freyCurve.galoisRep P.p (show 0 < P.p from sorry)) :=
  sorry

what are all these sorries in the type doing? I would like FLT.FreyPackage.FreyCurve.torsion_isHardlyRamified P to have type IsHardlyRamified (P.freyCurve.galoisRep P.p) but instead it produces an unspeakable horror of a type
have this := ⋯; have this_1 := sorry; have this_2 := ⋯; IsHardlyRamified ⋯ ⋯ (P.freyCurve.galoisRep P.p ⋯)

[Stepan Nesterov]

I understand that definition of a hardly ramified needs p odd and dimension 2 but why isn't it something like this?

theorem FLT.FreyPackage.FreyCurve.torsion_isHardlyRamified (P : FreyPackage) (h1 : Odd P.p) (h2 : Module.rank ZMod P.p P.freyCurve.n_torsion P.p = 2) : IsHardlyRamified h1 h2 P.freyCurve.galoisRep P.p := by sorry

[Ruben Van de Velde]

Maybe those should all be consequences of P being a Frey package?

[Kevin Buzzard]

Oh I just wanted to get the PR over the line so I left them.

The first sorry should be easy, p is prime and this is a theorem whose name I didn't remember.

The second one involves constructing the ring homomorphism from $\mathbb{Z}_p$ to $\mathbb{Z}/p\Z$ and I couldn't immediately find it so I left it.

The third one is much more profound and is the kind of thing which we probably don't have in mathlib (n-torsion in E(K), elliptic curve over a field, is finite for n>0). Probably a nontrivial project although I think that @David Ang might get to it one day (he's just finished his thesis yesterday :tada: ).

P odd is again a one-liner, it's part of the axioms IIRC but I didn't remember the one-line proof and didn't look it up because I didn't want to get distracted. Next sorry I don't even know what the statement is, is it something like E(Kbar)[p] has dimension 2? Again very hard (but known in the 80s). Final sorry should be trivial.

[Kevin Buzzard]

Stepan Nesterov said:

I understand that definition of a hardly ramified needs p odd and dimension 2 but why isn't it something like this?

theorem FLT.FreyPackage.FreyCurve.torsion_isHardlyRamified (P : FreyPackage) (h1 : Odd P.p) (h2 : Module.rank ZMod P.p P.freyCurve.n_torsion P.p = 2) : IsHardlyRamified h1 h2 P.freyCurve.galoisRep P.p := by sorry

We don't need them as extra hypotheses -- we can prove them from the hypotheses we already have. See https://imperialcollegelondon.github.io/FLT/docs/FLT/Basic/Reductions.html#FLT.FreyPackage -- P.p>=5 is a hypothesis so we can prove Odd P.p, the proof will be called P.hp5, similarly P.pp will be the proof that P.p is prime etc etc.

[Yakov Pechersky]

The second one involves constructing the ring homomorphism from $\mathbb{Z}_p$ to $\mathbb{Z}/p\Z$ and I couldn't immediately find it so I left it.

docs#PadicInt.toZMod

[Kevin Buzzard]

Thanks! Here's a revised version of that file:

import FLT.GaloisRepresentation.HardlyRamified.Defs
import FLT.Deformations.RepresentationTheory.EllipticCurve
import FLT.Basic.Reductions

variable (P : FLT.FreyPackage)

open GaloisRepresentation

lemma FLT.FreyPackage.hp_odd : Odd P.p := Nat.Prime.odd_of_ne_two P.pp <|
  have := P.hp5; by linarith

noncomputable local instance (p : ℕ) [Fact p.Prime] : Algebra ℤ_[p] (ZMod p) :=
  RingHom.toAlgebra PadicInt.toZMod

-- could be proved easily using `WeierstrassCurve.n_torsion_card`
instance : Module.Finite (ZMod P.p) (P.freyCurve.n_torsion P.p) := sorry

theorem FLT.FreyPackage.FreyCurve.torsion_isHardlyRamified :
    have : Fact (P.p.Prime) := ⟨P.pp⟩
    IsHardlyRamified P.hp_odd sorry
      (P.freyCurve.galoisRep P.p (show 0 < P.p from P.hppos)) :=
  sorry

theorem FLT.FreyPackage.FreyCurve.torsion_not_isIrreducible :
    have : Fact (P.p.Prime) := ⟨P.pp⟩
    ¬ GaloisRep.IsIrreducible (P.freyCurve.galoisRep P.p P.hppos) :=
  sorry -- TODO prove this

[Kevin Buzzard]

Actually one of the sorrys is false -- looking at the code I've defined the Galois rep to be the p-torsion of $E(\mathbb{Q})$ not $E(\overline{\mathbb{Q}})$ -- I'll fix this now. I set up all of the machinery to have the Galois group acting on the $\overline{Q}$-points but in the recent PR when I was just trying to get the statement down it looks like I've used the $\mathbb{Q}$-points.

[Stepan Nesterov]

What is the difference between these two:

theorem blah :
  have : Fact (P.p.Prime) := ⟨P.pp⟩
  Something P.p

theorem blah' (hPp : P.p.Prime) : Something P.p

[Stepan Nesterov]

In practice, FLT.FreyPackage.FreyCurve.torsion_isHardlyRamifiedseems to need a proof of Fact (P.p.Prime) as an argument

[Stepan Nesterov]

Kevin Buzzard said:

The first sorry should be easy, p is prime and this is a theorem whose name I didn't remember.

I mean the theorem "any prime >=5 is odd" was known in the 1980s

[Stepan Nesterov]

So it's fine

[Ruben Van de Velde]

The difference is that you don't want to use it as blah' P P.pp but rather just blah P

[Stepan Nesterov]

So when I do this

import FLT.GaloisRepresentation.HardlyRamified.Defs
import FLT.GaloisRepresentation.HardlyRamified.Lift
import FLT.Deformations.RepresentationTheory.EllipticCurve
import FLT.Basic.Reductions

variable (P : FLT.FreyPackage)

open GaloisRepresentation

lemma FLT.FreyPackage.hp_odd : Odd P.p := Nat.Prime.odd_of_ne_two P.pp <|
  have := P.hp5; by linarith

noncomputable local instance (p : ℕ) [Fact p.Prime] : Algebra ℤ_[p] (ZMod p) :=
  RingHom.toAlgebra PadicInt.toZMod
-- could be proved easily using `WeierstrassCurve.n_torsion_card`
instance : Module.Finite (ZMod P.p) (P.freyCurve.n_torsion P.p) := sorry

theorem FLT.FreyPackage.FreyCurve.torsion_isHardlyRamified :
    have : Fact (P.p.Prime) := ⟨P.pp⟩
    IsHardlyRamified (ℓ := P.p) P.hp_odd sorry
      (P.freyCurve.galoisRep P.p (show 0 < P.p from P.hppos)) :=
  sorry

theorem FLT.FreyPackage.FreyCurve.torsion_not_isIrreducible :
    have : Fact (P.p.Prime) := ⟨P.pp⟩
    ¬ GaloisRep.IsIrreducible (P.freyCurve.galoisRep P.p P.hppos) := by
    have hard_ram := FLT.FreyPackage.FreyCurve.torsion_isHardlyRamified P

the type of hard_ram is
have this := ⋯; IsHardlyRamified ⋯ ⋯ (P.freyCurve.galoisRep P.p ⋯)

[Stepan Nesterov]

Which I take to be a function from proofs that P.pp is prime to what I actually want

[Stepan Nesterov]

Also the goal is have this := ⋯; ¬(P.freyCurve.galoisRep P.p ⋯).IsIrreducible

[Ruben Van de Velde]

Does simp clean it up? Or you might use haveI instead, not sure if that'd help

[Kevin Buzzard]

Warning: I'm preparing a PR right now making some other modifications and tidying some of this up (we have a bunch of "IsSimpleModule" in the repo right now because there was no definition of an irreducible Galois rep, but now we have such a definition so things need cleaning up). I'll change the haves to haveIs if this makes things easier.

[Kevin Buzzard]

(I thought I was done but I just might have found a diamond in mathlib so I've been distracted)

[Stepan Nesterov]

Ruben Van de Velde said:

Does simp clean it up?

It does! :)

[Stepan Nesterov]

Simp is magic

[Kevin Buzzard]

oh argh it's not a diamond, it's just that AlgebraicClosure Rat and SeparableClosure Rat are two different types :-/

[Kevin Buzzard]

There is some design decision to be made here. Mathlib has Field.absoluteGaloisGroup and it is defined to be Gal(alg closure of K / K) where "Gal" just means K-algebra isomorphisms. I have been more principled and have been using the separable closure but now I've painted myself into a corner.

[Andrew Yang]

We should just change docs#Field.absoluteGaloisGroup to take separable closure right?

[Kevin Buzzard]

I can quite believe that that definition was made before we had existence of separable closure, but maybe? Of course then that would break all the code I just wrote ;-) (because I just switched to algebraic closure) but probably it's easily fixed again.

[Kevin Buzzard]

Another thing which has come up: is it possible to create a computable instance of DecidableEq (AlgebraicClosure ℚ) or shall I just dump the classical instance on it?

[Kevin Buzzard]

The stupid theory of stupid elliptic curves has gone stupid constructive on me and it's causing me pain.

[Stepan Nesterov]

Kevin Buzzard said:

Another thing which has come up: is it possible to create a computable instance of DecidableEq (AlgebraicClosure ℚ) or shall I just dump the classical instance on it?

Does this mean formalising in Lean an algorithm which checks if two algebraic numbers are equal?

[Stepan Nesterov]

Afaik this is mathematically nontrivial

[Stepan Nesterov]

Probably best done using theory of heights and effective Liouville bounds or something

[Aaron Liu]

Kevin Buzzard said:

Another thing which has come up: is it possible to create a computable instance of DecidableEq (AlgebraicClosure ℚ) or shall I just dump the classical instance on it?

It's a quotient of a really big multivariate polynomial ring by a maximal ideal containing docs#AlgebraicClosure.spanCoeffs (must exist so choose one with choice) so I think the answer is no, you can't make such an instance computably since you choosed a maximal ideal with choice

[Kevin Buzzard]

Hmm. So does this mean that Mathlib should have noncomputable instance : DecidableEq (AlgebraicClosure K) := Classical.typeDecidableEq _ for all fields K (and the same for separable closure), on the basis that we will never have a computable instance for any of these, even if K is ZMod 2?

[Kevin Buzzard]

@Stepan Nesterov FLT#750 is incoming. It does a huge amount of cleanup "underneath" what you're thinking about.

[Kevin Buzzard]

Seems to me that the tension between Stepan's answer and Aaron's answer to the decidable question is resolved with the observation that if we have x : AlgebraicClosure \Q then we will be able to prove that there's an irred monic poly over Q with x as a root but we will essentially never be able to compute what it is (we might be able to prove what it is for certain values of x but there is no algorithm giving us the min poly for an arbitrary element) and hence DecidableEq is too much to hope for.

[Stepan Nesterov]

Do number fields have decidable equality?
Because if you ultimately care about E[n] having decidable equality, couldn’t you just prove E(Qbar)[n] = E(K)[n] for some number field K

[Bryan Wang]

Kevin Buzzard said:

Hmm. So does this mean that Mathlib should have noncomputable instance : DecidableEq (AlgebraicClosure K) := Classical.typeDecidableEq _ for all fields K (and the same for separable closure), on the basis that we will never have a computable instance for any of these, even if K is ZMod 2?

This may be irrelevant, but it seems the entire file where AlgebraicClosure is defined is enclosed by a noncomputable section :sweat_smile:

[Junyan Xu]

We should just change docs#Field.absoluteGaloisGroup to take separable closure right?

That's #19616 and I left a comment there.

[Kevin Buzzard]

Stepan Nesterov said:

Do number fields have decidable equality?
Because if you ultimately care about E[n] having decidable equality, couldn’t you just prove E(Qbar)[n] = E(K)[n] for some number field K

Mathlib in general makes no attempt to be constructive. The rationals have decidable equality, and if anyone were to make number field instances on the constructively-defined QuadraticAlgebra \Q a b then we could have decidable equality on those quadratic fields. But if you make a general number field by e.g. taking the splitting field of a random polynomial then this construction is, I would have thought, hopelessly classical in mathlib, and I cannot imagine any desire to make such number fields constructive; if people want e.g. constructive cubic fields then they will probably just make concrete models by hand like we made docs#QuadraticAlgebra concretely.

[Kevin Buzzard]

I am unclear about the following strategy: if K were a random number field of degree 2 then we could prove the existence of a bijection between K and QuadraticAlgebra d 0 for some appropriate d; the bijection would need the type-theoretic axiom of choice (to choose which square root we use) and I am sufficiently unclear about all this constructivist stuff to know whether if you have a noncomputable bijection between X and Y then you might be expected to pull back decidable equality on Y to decidable equality on X (I would kind of doubt it but who knows).

[Aaron Liu]

Kevin Buzzard said:

and I am sufficiently unclear about all this constructivist stuff to know whether if you have a noncomputable bijection between X and Y then you might be expected to pull back decidable equality on Y to decidable equality on X (I would kind of doubt it but who knows).

You can pull back decidable equality along computable injective functions but if it's noncomputable then not really (for example, the obvious function Prop → Bool is a noncomputable bijection)

[Stepan Nesterov]

Why doesn't import FLT.GaloisRepresentation.HardlyRamified.Lift.lifts have that R is a domain in its conclusion but FLT.GaloisRepresentation.HardlyRamified.Family.mem_isCompatible requires that R is a domain in its hypothesis?

[Stepan Nesterov]

I assume that mathematically it doesn't matter much, because you can pushforward a hardly ramified representation from R to R/p for a minimal prime p and get a hardly ramified representation in a domain, but still

[Kevin Buzzard]

Yeah it's always difficult to know what generality to write things in. In the conclusion of lifts we have that R is local (hence nonzero) and finite free over Z_p, so it will have a minimal prime whose quotient will be integral and finite free over Z_p. Of course pushing this argument through will require proving that the minimal prime exists and also proving that a quotient of a hardly ramified representation is hardly ramified. For the first result you could ask on is there code for X, I am not up to date with how much comm alg we have (I think we have a bunch of going up/going down stuff so it should be OK). For the second, I've only just made hardly ramified representations so this result won't be there, it might be an interesting challenge to prove, or you could assume it. Or you could just change the statement of the theorem, or add a new theorem stating what you want and leave a comment saying how to relate it to the old theorem.

[Stepan Nesterov]

What is the idiomatic Lean way of saying ‘R is a ring of integers in a local field’ or ‘R is a local field’? That’s what all these R’s turn out to be in the actual argument, so if you didn’t have any tricky Lean optimizations in mind, I would just change assumptions to one of the two

[Stepan Nesterov]

Another question: is there a reason why the conclusion of the nonexistence of 3-adic hardly ramified reps is ‘trace of Frob_b is 1+p’ instead of ‘it is an extension of trivial by cyclotomic’? To prove the equivalence, we need Cebotatev density and Brauer-Nesbitt, and the proof really does give you reducibility.

[Stepan Nesterov]

Well, I guess we do need those things anyway because we want to deduce that the original p-adic rep is reducible and we do that by comparing traces :c

[Stepan Nesterov]

Are there formalized statements of Cebotarev density and Brauer-Nesbitt anywhere in the file? I couldn’t find them in mathlib, so I assume Lean doesn’t know these yet

[Kenny Lau]

Stepan Nesterov said:

‘R is a ring of integers in a local field’ or ‘R is a local field’

we just got nonarch local fields into mathlib recently

[Kenny Lau]

and for those you have a ValuativeRel, so you can just write 𝒪[k] after opening ValuativeRel

[Kenny Lau]

there's also the predicate version called Valuation.Integers

[Kevin Buzzard]

Stepan Nesterov said:

What is the idiomatic Lean way of saying ‘R is a ring of integers in a local field’ or ‘R is a local field’? That’s what all these R’s turn out to be in the actual argument

Is that true? In the lifting theorem the argument proves that the deformation ring is 1-dimensional and finite over Z_p, so it pretty much says what I wrote as opposed to what you're claiming that they turn out to be. At least, this is why I wrote it the way I wrote it. Even if we quotient out by a minimal prime we just get something which is an integral domain, finite and free over Z_p; I don't see any reason why this order in the field of fractions would be maximal in general.

The idiomatic way to say "I am a nonarchimedean local field" was only established very recently. AFAIK there is currently no way to idiomatically say "I am the ring of integers in a local field", but I don't see anything wrong with "I'm a Z_p-algebra, finite and free as a module, and an integral domain" for being an order, and then you could add "I am integrally closed" if you want it to be the full ring of integers, although I am a bit unclear about how full rings of integers are involved.

[Kevin Buzzard]

Stepan Nesterov said:

Another question: is there a reason why the conclusion of the nonexistence of 3-adic hardly ramified reps is ‘trace of Frob_b is 1+p’ instead of ‘it is an extension of trivial by cyclotomic’? To prove the equivalence, we need Cebotatev density and Brauer-Nesbitt, and the proof really does give you reducibility.

I just chose something random because I wanted to formalise something. We could absolutely change it to "I am an extension of trivial by cyclotomic". Cebotarev and B-N we can just assume, they were known in the 80s.

[Kevin Buzzard]

Kenny Lau said:

and for those you have a ValuativeRel, so you can just write 𝒪[k] after opening ValuativeRel

But we don't have k, I think the argument gives you a Z_p-algebra which has a nonzero torsion-free quotient which is finite over Z_p. I am a bit confused about why local fields need to be involved here.

[Stepan Nesterov]

Fields get involved because the argument uses some results from representation theory of groups over fields, such as Brauer's theorem on induced characters and Brauer-Nesbitt.
The way I have the argument in my mind is:

• The universal deformation ring is finite
• Therefore, it has a K-point, for K/Q_p finite
• The representation rho corresponding to this K-point is potentially modular, hence, its restriction to G_F speads out to a compatible family
• By Brauer group trick and solvable base change, rho itself spreads (this formalism is over a field)
• The 3-adic rep in the family is reducible, hence Tr(Frob_q)=1+q
• The traces of rho are also 1+q, hence by Brauer-Nesbitt (which is over a field), rho^ss = 1 + cyclo
• Therefore, the reduction of rho (which I will need to formally define, I guess) is reducible

[Stepan Nesterov]

Alternatively, I could maybe say that two representations into GL_2(O_K) are isogenous, if they have sublattices which are isomorphic as representations, and state Brauer-Nesbitt in the form "equal traces => semisimplifications are isogenous". Of course the semisimplification will itself only be defined up to isogeny in this approach.
The reason I want full O_K here is because I'm scared of non-normal rings and I'm afraid I will need to consider representations into non-free modules or something to make a correct statement

[Stepan Nesterov]

Are there obvious Lean reasons for why field approach or O_K approach is better?

[Kevin Buzzard]

I don't talk about hardly ramified representations into fields because the flatness criterion involves an integral model (a rep to GL_2(R) is flat iff the correponding reps to GL_2(R/I) come from a ffgs for all open ideals I), so one then has to decide how to formalise what it means for a rep to GL_2(K) to be hardly ramified (there exists a good lattice/for all good lattices). Again of course these things are all the same, but with formalization you just have to be very precise by what you mean with phrases like "hardly ramified" and "flat". I think I would avoid the concept of isogenous representations and work with fields -- and as you point out we'll have to work with fields when doing the Brauer group trick -- but mathematicians are good at glossing over issues, such as calling reps to GL_2(K) flat whereas in fact this concept depends on an integral model (and is independent of the model, but in Lean one would have to give this concept another name). At the end I was going to go "trace of p-adic lift to GL_2(R), when tensored with K, is 1+q, so trace of p-adic lift to GL_2(R) has trace 1+q, so trace of original mod p rhobar is 1+q so it's reducible" rather than attempting to reduce a p-adic representation mod p (which of course we'll also have to do at some stage).

[Kevin Buzzard]

Your "R is finite therefore has a K-point" is just my "choose a minimal prime", you then work with the field of fractions of R/P which will be finite over Q_p and a field and hence a local field.

[Stepan Nesterov]

Kevin Buzzard said:

trace of original mod p rhobar is 1+q so it's reducible

But you cannot apply Braueer-Nesbitt in positive characteristic. Well, you can, but then you need to define Brauer characters, which would take us too far afield

[Stepan Nesterov]

I think we need to say "trace of the original is 1 + p => original tensor field is reducible => reduction of some lattice is reducible, but well-defined up to semisimplification, so rhobar reducible" at this point

[Stepan Nesterov]

But I assume I can leave "reduction well-defined" as a sorry because it was known in the 1980s

[Stepan Nesterov]

Wait, actually you can, if you state Brauer-Nesbitt as "If rho and sigma are reps over a field of char p, which have the same traces, then for any irreducible tau the amount of occurences of tau in the Jordan-Holder series of sigma is congruent mod p to the amount of occurences of tau in the Jordan-Holder series of rho"

[Kevin Buzzard]

The statement I was thinking of is "if semisimple rho and sigma have the same char polys then they're iso"

[Stepan Nesterov]

Yea ok

[Stepan Nesterov]

Because 1 and cyclo are distinct, everything is fine

[Stepan Nesterov]

Is there a theorem saying that if Galois representations are conjugate, then Frobenius at v has the same characteristic polynomial in them?
I have (GaloisRep.baseChange (AlgebraicClosure ℚ_[P.p]) σ).conj r' = T fact ψ, and I need to relate LinearMap.charpoly (((T fact ψ).toLocal v) (Field.AbsoluteGaloisGroup.adicArithFrob v)) to LinearMap.charpoly (GaloisRep.baseChange (AlgebraicClosure ℚ_[P.p]) σ) (Field.AbsoluteGaloisGroup.adicArithFrob v))

[Stepan Nesterov]

Also is there a theorem saying that charpoly behaves correctly under base change of Galois representations? I need
LinearMap.charpoly ((((GaloisRep.baseChange (AlgebraicClosure ℚ_[3]) τ).conj r'').toLocal v) (Field.AbsoluteGaloisGroup.adicArithFrob v)) = Polynomial.map Algebra.algebraMap (LinearMap.charpoly ((τ.toLocal v) (Field.AbsoluteGaloisGroup.adicArithFrob v)))

[Kevin Buzzard]

GaloisRep is a definition made in FLT, and you can see absolutely everything we know about it by just searching for GaloisRep in the FLT repo. I'm sure we're missing plenty of API! Your first step could be to get GaloisRep out of the question and to reduce it to a question involving only objects defined in mathlib and then ask again (because then the whole mathlib community can help), or alternatively to isolate and prove some intermediate results which will help.

Unfortunately I have to spend all day interviewing (apart from a 1 hour lunch break which I will be spending giving a Zoom talk due to poor planning on my part) so I am out of action for the next 8 hours. I guess one thing which might be helpful is if you make a #mwe which would run in the FLT repository; then I can start working on your question much more easily.

[Kevin Buzzard]

@Stepan Nesterov I've finally found the time to look at your question but it's just full of undefined terms and I can't get it to compile. Here's what I have so far:

import FLT.GaloisRepresentation.HardlyRamified.Defs
import FLT.Basic.FreyPackage
import Mathlib

example (P : FreyPackage) [Fact P.p.Prime] (σ : GaloisRep _ _ _)
    (h : (GaloisRep.baseChange (AlgebraicClosure ℚ_[P.p]) σ).conj r' = T fact ψ) :
    LinearMap.charpoly (((T fact ψ).toLocal v) (Field.AbsoluteGaloisGroup.adicArithFrob v)) =
    LinearMap.charpoly (GaloisRep.baseChange (AlgebraicClosure ℚ_[P.p]) σ) (Field.AbsoluteGaloisGroup.adicArithFrob v) := by
  sorry

The best way to ask "how do I prove X" on this forum is to say "here is compiling Lean code; how do I fill in the sorry?" There are often several different ways to formalise the same mathematical idea so the added precision here is more important than you think.

[Kevin Buzzard]

Looks to me like GaloisRep.conj is defined in terms of LinearEquiv.algConj which is defined in terms of LinearEquiv.conjRingEquiv which is defined by an explicit conjugation, and everything here is defeq, so Lean will be able to see through a lot of it and you should be able to use docs#LinearEquiv.charpoly_conj to answer your conjugate question.

[Kevin Buzzard]

As for base change, if I've understood the question correctly then you're talking about GaloisRep.baseChange which is defined in terms of Module.End.baseChangeHom which is defined in terms of LinearMap.baseChange so you should be able to use docs#LinearMap.charpoly_baseChange . In general the amount of precision in my answer balances the amount of precision in your question.

[Stepan Nesterov]

Ok sorry

[Stepan Nesterov]

Here's my sorries:

import FLT.GaloisRepresentation.HardlyRamified.Defs
import FLT.GaloisRepresentation.HardlyRamified.Lift
import FLT.GaloisRepresentation.HardlyRamified.Family
import FLT.GaloisRepresentation.HardlyRamified.Threeadic
import FLT.Basic.FreyPackage
import Mathlib.Tactic.Cases
import Mathlib.LinearAlgebra.Charpoly.ToMatrix

variable {K : Type*} {L : Type*} [Field K] [Field L]
variable {A : Type*} [CommRing A] [TopologicalSpace A]
variable {B : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
variable [Algebra A B] [ContinuousSMul A B]
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
variable [Module.Finite A M] [Module.Free A M] [Module.Finite A N] [Module.Free A N]

lemma charpoly_base_change (ρ : GaloisRep K A M) (g : Field.absoluteGaloisGroup K) :
  LinearMap.charpoly (GaloisRep.baseChange B ρ g) =
    Polynomial.map Algebra.algebraMap (LinearMap.charpoly (ρ g)) := by
  sorry

lemma charpoly_conj (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) (g : Field.absoluteGaloisGroup K) :
  LinearMap.charpoly ((GaloisRep.conj ρ e) g) = LinearMap.charpoly (ρ g) := by
  sorry

lemma conj_commutes_with_to_local [NumberField K]
   (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (ρ : GaloisRep K A M)
     (e : M ≃ₗ[A] N) : (GaloisRep.conj ρ e).toLocal v = GaloisRep.conj (ρ.toLocal v) e := by
  sorry

lemma to_local_commutes_with_base_change [NumberField K]
   (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (ρ : GaloisRep K A M) :
    (GaloisRep.baseChange B ρ).toLocal v = GaloisRep.baseChange B (ρ.toLocal v) := by
  sorry

[Stepan Nesterov]

Ok actually the last two are just rfl

[Kevin Buzzard]

And the first two are the suggestions I made (modulo adding an import: when developing I usually just do import Mathlib and then #min_imports later on)

import FLT.GaloisRepresentation.HardlyRamified.Defs
import FLT.GaloisRepresentation.HardlyRamified.Lift
import FLT.GaloisRepresentation.HardlyRamified.Family
import FLT.GaloisRepresentation.HardlyRamified.Threeadic
import FLT.Basic.FreyPackage
import Mathlib.Tactic.Cases
import Mathlib.LinearAlgebra.Charpoly.ToMatrix
import Mathlib.LinearAlgebra.Charpoly.BaseChange -- I added this

variable {K : Type*} {L : Type*} [Field K] [Field L]
variable {A : Type*} [CommRing A] [TopologicalSpace A]
variable {B : Type*} [CommRing B] [TopologicalSpace B] [IsTopologicalRing B]
variable [Algebra A B] [ContinuousSMul A B]
variable {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
variable [Module.Finite A M] [Module.Free A M] [Module.Finite A N] [Module.Free A N]

lemma charpoly_base_change (ρ : GaloisRep K A M) (g : Field.absoluteGaloisGroup K) :
  LinearMap.charpoly (GaloisRep.baseChange B ρ g) =
    Polynomial.map Algebra.algebraMap (LinearMap.charpoly (ρ g)) := by
  apply LinearMap.charpoly_baseChange

lemma charpoly_conj (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) (g : Field.absoluteGaloisGroup K) :
    LinearMap.charpoly ((GaloisRep.conj ρ e) g) = LinearMap.charpoly (ρ g) := by
  apply LinearEquiv.charpoly_conj

lemma conj_commutes_with_to_local [NumberField K]
   (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (ρ : GaloisRep K A M)
     (e : M ≃ₗ[A] N) : (GaloisRep.conj ρ e).toLocal v = GaloisRep.conj (ρ.toLocal v) e := by
  rfl

lemma to_local_commutes_with_base_change [NumberField K]
   (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (ρ : GaloisRep K A M) :
    (GaloisRep.baseChange B ρ).toLocal v = GaloisRep.baseChange B (ρ.toLocal v) := by
  rfl

[Kevin Buzzard]

You don't even need to go into tactic mode:

lemma charpoly_base_change (ρ : GaloisRep K A M) (g : Field.absoluteGaloisGroup K) :
    LinearMap.charpoly (GaloisRep.baseChange B ρ g) =
    Polynomial.map Algebra.algebraMap (LinearMap.charpoly (ρ g)) :=
  LinearMap.charpoly_baseChange _ _

lemma charpoly_conj (ρ : GaloisRep K A M) (e : M ≃ₗ[A] N) (g : Field.absoluteGaloisGroup K) :
    LinearMap.charpoly ((GaloisRep.conj ρ e) g) = LinearMap.charpoly (ρ g) :=
  LinearEquiv.charpoly_conj _ _

Lean sees through all the definitional equalities.

[Stepan Nesterov]

Is the rule that defeq works with apply but not rw?

[Ruben Van de Velde]

Roughly, yes

[Kevin Buzzard]

Yeah rw will only match up to syntactic equality which is much stronger

[Stepan Nesterov]

Alright, I have succesfully reduced the task to proving ¬ GaloisRep.IsIrreducible (P.freyCurve.galoisRep P.p P.hppos) from
∀ v ∉ S, 3 ∉ v.asIdeal → 5 ≤ ↑(toNatPrime v) → ↑P.p ∉ v.asIdeal → LinearMap.charpoly (((P.freyCurve.galoisRep P.p ⋯).toLocal v) (Field.AbsoluteGaloisGroup.adicArithFrob v)) = Polynomial.map Algebra.algebraMap ((Polynomial.X - 1) * (Polynomial.X - ↑↑(toNatPrime v)))
Do we need recognizable statements of Cebotarev density and Brauer-Nesbitt + formal deduction of this implication from these statements or does this count as reducing a theorem to results known in the 80s?

[Kevin Buzzard]

Reduction: please PR!

Reducing to 1980s: right now my attitude is "if I could prove it in the 1980s with a short proof using only standard stuff then skip it for now and we'll come back to it later". I think this attitude will force us to focus on the important stuff, and I'll worry about tidying up later.