Future work

Stream: FLT-regular

[Riccardo Brasca]

Dear all, I think it's a good idea to write down a list of things we should do, maybe in order of priority. In my opinion our main goal now should be to help @Kevin Buzzard's work on full flt. A lot of the stuff we proved will help Kevin's project, so this should be moved to mathlib as soon as possible (and we all know this is not a fast process...). Here is a short list

• Update the blueprint. This is important to make clear what we proved and what we didn't (in particular I would not bother a lot with proofs, we can just say "see the Lean proof" or give a reference, but we want the "Lean" button).
• Opening PRs for the miscellaneous prerequisites (those in AuxLemmas.lean). This can be parallelized and hopefully it will relatively fast.
• Polish the code (checking that everything is in full generality and so on)
• Thinking about the most serious stuff. Maybe ramification is the most basic thing we have?

[Chris Birkbeck]

Yes this is a good idea. I tried adding more \leanoks to the blueprint proof to turn them green, but it didn't seem to work, so I need to see what the problem is. Also some of the links to the code aren't working, which again I'm not sure why is the case.

[Riccardo Brasca]

I've added \leanok to Hilbert90 and Hilbert92 and everything worked fine.

[Chris Birkbeck]

Oh weird they are green now. For some reason when I looked last time they still had a white background. Ok that's good then.

[Riccardo Brasca]

Does the blueprint follow the actual Lean proof?

[Andrew Yang]

Yes in spirit, but we did not prove everything in the blueprint, and the blueprint missed quite a few details.

[Chris Birkbeck]

Ah what bits did we not use from the blueprint? I'm guessing some of the ramification results?

[Chris Birkbeck]

Chris Birkbeck said:

Oh weird they are green now. For some reason when I looked last time they still had a white background. Ok that's good then.

I just realised the problem, I was looking at the test blueprint site not the official one :sweat_smile:

[Yaël Dillies]

If nobody is specifically thinking of PRing homogenisation, I would like to do it. I need it for like three separate things now.

[Riccardo Brasca]

No problem!

[Kevin Buzzard]

I need FLT3 -- this is going to be a blue node on the forthcoming FLT blueprint :-)

[Alex J. Best]

@Yaël Dillies yes please pr it, and sorry to everyone I told I'd manage to do so myself xD

[Riccardo Brasca]

Kevin Buzzard said:

I need FLT3 -- this is going to be a blue node on the forthcoming FLT blueprint :-)

We need to think about it. There are three possibilities:

• PRing @Ruben Van de Velde proof: it is totally elementary, it stays in Z.
• Our proof of case II works for p = 3 (but of course it will take a while to put everything in mathlib). Case I is very easy for p=3 (reasoning modulo 9).
• The last possibility is to work in $\mathbb{Q}(\zeta_3)$, but doing case II by hand.

In my opinion the last option is the best one, it is mathematically OK (we don't want to port to mathlib all the small details of flt-regular if the final goal is flt, we only want the relevant prerequisites) and not that long.

Of course we need that $\mathbb{Q}(\zeta_3)$ is a PID in option 2 and 3, but I am confident @Xavier Roblot will give soon the right tool for that (and at worst it's surely doable by hand in a couple of hours).

[Riccardo Brasca]

Anyway we can take care of that, our techniques are more than enough.

[Ruben Van de Velde]

Happy to help with any of those

[Xavier Roblot]

Riccardo Brasca said:

Of course we need that $\mathbb{Q}(\zeta_3)$ is a PID in option 2 and 3, but I am confident Xavier Roblot will give soon the right tool for that (and at worst it's surely doable by hand in a couple of hours).

Well, Hermite-Minkowski is ready (#8478) and to prove the classical bound on norm of integral ideals in ideal classes you need to do essentially the same proof with the ring of integers replaced by an integral ideal so it should be relatively easy to get. I'll start working on it soon.

[Riccardo Brasca]

Having a look.

[Yaël Dillies]

Btw could I have access to the repository so that I can clean up homogenisation while making sure everything else still builds?

[Riccardo Brasca]

Sure!

[Riccardo Brasca]

YaelDillies • Already has access to this repository

[Yaël Dillies]

Whoops :see_no_evil:

[Riccardo Brasca]

Feel free to push to master. As soon it compiles and it looks reasonable no problem.

[Michael Stoll]

BTW, one of my students in the formalization "seminar" is working on properties of the Eisenstein integers (in particular that they form a euclidean domain), but this will not be ready (and in mathlib-ready form) soon. This will use a more direct (pederstrian?) approach, following Ireland-Rosen.

[Riccardo Brasca]

Nice! Even if we obtain PID almost for free by Minkowski bound, having euclidean domain is better.

[Riccardo Brasca]

We probably want that K is euclidean if IsCyclotomicExtension {3} Q K

[Michael Stoll]

To avoid DTT hell, he is building the ring from a structre like Zsqrtd, but it should be easy to link this up with other definitions.

[Kevin Buzzard]

One could be optimistic that a route would be: prove that the concrete structure R is Euclidean, prove IsCyclotomicExtension 3 \Q (FractionField R) and then get a bunch of stuff for free.

[Michael Stoll]

Possibly. But first the Euclidean property!

[Kevin Buzzard]

Yeah, it's a nice project for a student. I've had several students prove $\Z[i]$ (the concrete structure) is Euclidean over the years.

[Ruben Van de Velde]

Would you be able to make sure the student's work doesn't disappear with them? Even if it's not mathlib-ready, it might be easier to start from something rather than nothing

[Michael Stoll]

I can take his work and try to turn it into something suitable for Mathlib eventually. (I did something similar with Pell's equation a while back.)

[Riccardo Brasca]

What is the concrete definition? We can in parallel show that it is a cyclotomic extension

[Kevin Buzzard]

My understanding is that it's a structure with an integer "real part" field and an integer "omega part" field.

[Riccardo Brasca]

I understand the idea, we already have docs#Zsqrtd, I just wanted a Lean definition to work with. Is it literally Zsqrtd -3?

[Kevin Buzzard]

no because $\Z[\sqrt{-3}]$ isn't $\Z[\zeta_3]$.

[Riccardo Brasca]

Ah yes, Zsqrtd has no /2

[Kevin Buzzard]

The ZSqrtd thing was all set up by Mario because he had to say something about Pell in some very special cases to do Matiyesevich's theorem. There is an argument for doing integers in quadratic fields concretely in this way

[Alex J. Best]

In the class group diophantine project we used a generalized version of zsqrtD see https://github.com/lean-forward/class-group-and-mordell-equation/blob/main/src/number_theory/quad_ring/basic.lean . Though most of our results were for numbers 3 mod 4 for simplicity anyway

[Xavier Roblot]

Xavier Roblot said:

Riccardo Brasca said:

Of course we need that $\mathbb{Q}(\zeta_3)$ is a PID in option 2 and 3, but I am confident Xavier Roblot will give soon the right tool for that (and at worst it's surely doable by hand in a couple of hours).

Well, Hermite-Minkowski is ready (#8478) and to prove the classical bound on norm of integral ideals in ideal classes you need to do essentially the same proof with the ring of integers replaced by an integral ideal so it should be relatively easy to get. I'll start working on it soon.

I was able to prove the following

theorem exists_ideal_in_class_of_norm_le (C : ClassGroup (𝓞 K)):
    ∃ I : (Ideal (𝓞 K))⁰, ClassGroup.mk0 I = C ∧
      Ideal.absNorm (I : Ideal (𝓞 K)) ≤ (4 / π) ^ NrComplexPlaces K *
        ((finrank ℚ K).factorial / (finrank ℚ K) ^ (finrank ℚ K) * Real.sqrt |discr K|) := by

I guess that should be enough to prove that $\mathbb{Q}(\zeta_3)$ is principal. The PR (#9084) is still WIP as there are quite a number of auxiliary lemmas that need to find their place (and probably should be generalised, golfed, etc.)

[Riccardo Brasca]

Nice! @Andrew Yang have you proved anything about the embedding of a cyclotomic field (I mean that they're all complex)?

[Andrew Yang]

No but it should be easy using pow_eq_one_iff_of_nonneg in R.

[Riccardo Brasca]

Yes, it is surely not hard, I just wanted to not duplicate your work