Discord server

Stream: new members

[Paul Lezeau]

Hi ! I'm a second year undergraduate from Warwick doing a summer project in Lean. Is it still possible to join the Xena project server ?

[Huỳnh Trần Khanh]

It's a top secret server for elite Lean users. @Kevin Buzzard will PM you an invite link if you are qualified.

[Huỳnh Trần Khanh]

Just patiently wait.

[Damiano Testa]

I am not sure about élite, since I have been admitted a long time ago! In any case, there are certainly élite users in the Discord!

Also, for context, Paul will be working with me on a project around Galois theory.

[Eric Wieser]

To clear up any confusion about the joke in @Huỳnh Trần Khanh's message, it is absolutely not exclusively for elite users, but access to it is generally handled on a case-by-case basis. As an undergraduate doing a summer project, you'd definitely be welcome (although it's not my call to make)!

[Adam Topaz]

I'm sure @Bhavik Mehta will be happy to extend an invite when he signs on to zulip ;)

[Adam Topaz]

Out of curiosity, what maths around Galois theory were you planning to formalize in this project?

[Damiano Testa]

We have not really settled on something specific yet: the project is supposed to start at the end of this month. We had been thinking about relating Galois group over different fields, with a view towards Dedekind's Theorem.

[Damiano Testa]

Though I have not yet looked at what is already available, so our aims might change!

[Adam Topaz]

Sounds great! Looking forward to your mathlib PRs :wink:

[Paul Lezeau]

Thanks ! I'm looking to working on it :smiley:

[Kevin Buzzard]

Invite sent. What is Dedekind's theorem?

[Kevin Buzzard]

Here is something I would very much like to have in Lean: if $L/K$ is a finite extension of global fields and $P$ is a prime of $K$ which splits as $\prod_iQ_i^{e_i}$ in $L$ then $K_P\otimes_KL=\bigoplus_iL_{Q_i}$ for some value of $=$ (probably ≃+*).

[Kevin Buzzard]

A corollary of this is $\sum_ie_if_i=[L:K]$, and even that would be pretty cool to have.

[Paul Lezeau]

Thanks a lot !
We were thinking of having a go at https://kconrad.math.uconn.edu/blurbs/gradnumthy/frobeniuspf.pdf, or Theorem 1 in https://kconrad.math.uconn.edu/blurbs/gradnumthy/dedekindf.pdf.

[Paul Lezeau]

Kevin Buzzard said:

Here is something I would very much like to have in Lean: if $L/K$ is a finite extension of global fields and $P$ is a prime of $K$ which splits as $\prod_iQ_i^{e_i}$ in $L$ then $K_P\otimes_KL=\bigoplus_iL_{Q_i}$ for some value of $=$ (probably ≃+*).

Sounds like it would be quite an interesting result to work on, although I think it's a bit too advanced for me !

[Kevin Buzzard]

So "Theorem 1 (Dedekind)" in dedekindf.pdf ? Is that "Dedekind's Theorem"?

[Paul Lezeau]

I think so !

[Kevin Buzzard]

I think you would be better off proving a relative result.

[Paul Lezeau]

A relative result in what sense ?

[Kevin Buzzard]

If $L/K$ is a finite extension of number fields and if $\alpha\in\mathcal{O}_L$ such that $L=K(\alpha)$ and $p\nmid[\mathcal{O}_L:\mathcal{O}_K[\alpha]]$ then for all $P$ of $\mathcal{O}_K$ whose norm is coprime to $[\mathcal{O}_L:\mathcal{O}_K[\alpha]]$, the factorization of the min poly for $\alpha$ over $K$ modulo $P$ corresponds to the decomposition of $P\mathcal{O}_L$ into primes. And you should not just prove an existence theorem -- the "theorem" is a definition which writes down an explicit map between two finite types and then proves that this map is a bijection.

[Kevin Buzzard]

Working in this generality will be much easier.

[Kevin Buzzard]

If it looks intimidating just pretend $K=\mathbb{Q}$ in your head because it's the same proof which works in the general case.

[Kevin Buzzard]

In fact translating Conrad's proof over $\mathbb{Q}$ into a general argument over $K$ will be a very interesting mathematical project, and then you could formalise the general case in Lean whilst doing the translation on paper, and if you get stuck on any Lean bits then just sorry them. Don't make any definitions -- everything you need is there.

[Paul Lezeau]

Oh right that makes sense. That would definitely be a very interesting project to work on, thanks a lot for the advice !

[Kevin Buzzard]

Port it from the top down. First try to state it. This will be much harder than you think but Damiano will be able to tell you the API. The actual construction itself will be that if $k:=\mathcal{O}_K/P$ then to a monic irreducible polynomial $p(x)\in k[x]$ which is a factor mod $P$ of the min poly $f(x)$ of $\alpha$ you will need to make some explicit construction of a prime ideal. It will be really cool to see how abstract and golfy the actual bijection will end up.

[Kevin Buzzard]

You can lift $f$ to $\mathcal{O}_L/P\mathcal{O_L}$ and this is canonically isomorphic to $\bigoplus_i(\mathcal{O}_L/\pi_i^{e_i})$. If you do careful planning there could be something really cool here.

[Kevin Buzzard]

You should really do it over all global fields and assume that $L/K$ is separable, because again this will be no harder than the number field case. We have the theorem that ideals factor uniquely into prime ideals so all the ingredients are there.

[Paul Lezeau]

I'll definitely have a got at that, thanks again !

[Damiano Testa]

Indeed, thanks Kevin!

I also want to emphasize one of the great strengths of formalizing. If you formalize a proof, thinking of your special case (e.g. $\mathbb{Q}$ in this case), and Lean confirms that all the steps work for a general global field, you achieve two goals:

• you proved a more general result;
• normally you also understand the proof in the more general case much better!

This is a very important consequence of using a proof assistant!