Zulip Chat Archive

Stream: Is there code for X?

Topic: Is there code for Galois theory?


view this post on Zulip Keyao Peng (Jun 23 2020 at 15:36):

I didn't find the theorems of Galois theory in mathlib. Are there some difficulties to achieve these?

view this post on Zulip Patrick Massot (Jun 23 2020 at 15:41):

Mostly manpower

view this post on Zulip Jalex Stark (Jun 23 2020 at 15:43):

feel free to give it a shot, and post many questions here about the parts you find difficult

view this post on Zulip Keyao Peng (Jun 23 2020 at 15:45):

Yeah, I am new to Lean, but I'd like to have a try.

view this post on Zulip Alex J. Best (Jun 23 2020 at 15:50):

Adding Galois theory would be really great (and quite possible I think) @Kenny Lau added docs#linear_independent_monoid_hom . From this, we can follow more of the reference https://kconrad.math.uconn.edu/blurbs/galoistheory/linearchar.pdf Kenny used to get the normal basis theorem it seems.

view this post on Zulip Patrick Massot (Jun 23 2020 at 15:50):

You should ask @Chris Hughes too

view this post on Zulip Johan Commelin (Jun 23 2020 at 15:53):

@Jack J Garzella Is also interested in doing this, I think.

view this post on Zulip Adam Topaz (Jun 23 2020 at 15:55):

Does mathlib have code for etale algebras?

view this post on Zulip Adam Topaz (Jun 23 2020 at 15:55):

I suppose not.

view this post on Zulip Patrick Massot (Jun 23 2020 at 15:55):

No

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:01):

You can git grep "tale"

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 16:06):

There is an Imperial galois theory repo which was ticking along nicely but got held up at algebraic closures. @Chris Hughes you've told me so many times now what the obstruction is. Something to do with category theory?

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:08):

I think it's more the fact that we don't know how to deal with commutative diagrams

view this post on Zulip Patrick Massot (Jun 23 2020 at 16:17):

But Markus knows.

view this post on Zulip Patrick Massot (Jun 23 2020 at 16:17):

@Markus Himmel?

view this post on Zulip Markus Himmel (Jun 23 2020 at 16:29):

Unfortunately, I don't think my work helps here in its current form

view this post on Zulip Patrick Massot (Jun 23 2020 at 16:29):

Is it getting closer to mathlib by the way?

view this post on Zulip Markus Himmel (Jun 23 2020 at 16:32):

Abelian categories have already landed, the rest is on its way but I'm busy with real-life things at the moment. I'm hoping to get back to PRing in 1-2 weeks.

view this post on Zulip Patrick Massot (Jun 23 2020 at 16:33):

I think you should also write a paper if you haven't done so already.

view this post on Zulip Markus Himmel (Jun 23 2020 at 16:35):

Honestly, I don't think there is anything in my work that would warrant a paper.

view this post on Zulip Patrick Massot (Jun 23 2020 at 16:36):

The automation part looks really new to me (but I'm not an expert).

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:36):

How many computers have verified 5 line proofs of the four lemma?

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:37):

I'm ignorant, of course, but I'm not aware of other provers have such automation

view this post on Zulip Markus Himmel (Jun 23 2020 at 16:40):

Maybe it's new, but it's really trivial. My tactic is essentially a dumber version of the cc tactic adapted to small commutative diagrams.

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 16:43):

@Markus Himmel my PhD thesis was really trivial once I completely understood it because I'd written it. This is a common trap to fall into. Just because you think it's trivial doesn't take away from the fact that you did it first. Publish!

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 16:43):

Teach others how trivial it is! People can learn from your work.

view this post on Zulip Markus Himmel (Jun 23 2020 at 16:58):

Thank you for the advice. I'll look into what might be publishable when I finally start working on the tactic again, but there's lots of non-meta code to clean up and PR first.

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 17:02):

Do that too! It's so easy to lose interest in a project when you've "made it over the line". But actually there are more lines, and the longer you leave it, the harder it is to cross them, so the canonical thing to do is to prioritise the PRs and the write-up now.

view this post on Zulip Jack J Garzella (Jun 23 2020 at 19:35):

@Keyao Peng Yes, I've been working on Galois theory stuff, I am working on proving that all degree 2 extensions are normal. I think there are some relevant theorems of a similar flavor that wouldn't require algebraic closures, maybe we could brainstorm something for you to do if you want to get your feet wet.

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 19:38):

Is normal and separable and splitting field in mathlib?

view this post on Zulip Kenny Lau (Jun 23 2020 at 19:39):

I am working on separable. Normal is in galois repo.

view this post on Zulip Alex J. Best (Jun 23 2020 at 19:41):

What is galois repo?

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 19:42):

The private IC repo

view this post on Zulip Alex J. Best (Jun 23 2020 at 19:43):

I see, would be cool to know whats in there, I've also been sad we don't have any Galois theory recently. Would be a shame to duplicate effort!

view this post on Zulip Adam Topaz (Jun 23 2020 at 19:52):

Does mathlib have the theorem that any field embeds in some algebraically closed field?

view this post on Zulip Patrick Massot (Jun 23 2020 at 19:53):

No.

view this post on Zulip Patrick Massot (Jun 23 2020 at 19:53):

It has been discussed a lot, but never converged.

view this post on Zulip Reid Barton (Jun 23 2020 at 19:54):

It also doesn't seem necessary to do Galois theory--the algebraic closure is not really unique anyways.

view this post on Zulip Reid Barton (Jun 23 2020 at 19:55):

So you will always want to fix an algebraic closure, and then you no longer need an existence theorem.

view this post on Zulip Adam Topaz (Jun 23 2020 at 19:55):

I agree. But if you define the Galois category of finite etale covers of a field, you still need to choose a fibre functor to construct the Galois groups...

view this post on Zulip Reid Barton (Jun 23 2020 at 19:56):

Sure, at some distant point it's necessary, but anything that counts as undergraduate Galois theory can be done in the meantime.

view this post on Zulip Alex J. Best (Jun 23 2020 at 19:56):

Whats the status of https://github.com/leanprover-community/mathlib/pull/1297 ?

view this post on Zulip Patrick Massot (Jun 23 2020 at 20:05):

Given the age of this PR, it may be faster to restart from scratch.

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 20:16):

over 1000 lines

view this post on Zulip Patrick Massot (Jun 23 2020 at 20:17):

How many refactors in the mean time?

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 20:17):

over 10000 lines

view this post on Zulip Keyao Peng (Jun 23 2020 at 20:22):

I'm not familiar with the situation of mathlib, can't we use algebraic closure or something like this?

view this post on Zulip Kenny Lau (Jun 23 2020 at 20:23):

I believe that's the point

view this post on Zulip Reid Barton (Jun 23 2020 at 20:29):

I think the PR is on hold because Chris wants to do it a different way.

view this post on Zulip Keyao Peng (Jun 23 2020 at 20:31):

Can I define a category of all algebraic extension of a field k?

view this post on Zulip Chris Hughes (Jun 23 2020 at 20:34):

I'm not really working on doing it any differently. It's almost done, it just needs a bundled hom refactor.

view this post on Zulip Chris Hughes (Jun 23 2020 at 20:35):

@Keyao Peng yes. This could either be a large category, or could also be defined to be the small category of sub extensions of the algebraic closure.

view this post on Zulip Keyao Peng (Jun 23 2020 at 20:37):

Chris Hughes said:

Keyao Peng yes. This could either be a large category, or could also be defined to be the small category of sub extensions of the algebraic closure.

but how to do it in Lean?

view this post on Zulip Keyao Peng (Jun 23 2020 at 20:46):

Do you know some similar projects? I want to know how to define something like that in Lean.

view this post on Zulip Keyao Peng (Jun 23 2020 at 20:51):

Jack J Garzella said:

Keyao Peng Yes, I've been working on Galois theory stuff, I am working on proving that all degree 2 extensions are normal. I think there are some relevant theorems of a similar flavor that wouldn't require algebraic closures, maybe we could brainstorm something for you to do if you want to get your feet wet.

I'd like to. Maybe it will help me to understand how to do math in Lean.

view this post on Zulip Patrick Massot (Jun 23 2020 at 20:51):

You should probably avoid category theory in the beginning.

view this post on Zulip Bryan Gin-ge Chen (Jun 23 2020 at 20:59):

We do have a mini-tutorial for category theory in mathlib: https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/category_theory/intro.lean but it might be out of date.

view this post on Zulip Kevin Buzzard (Jun 23 2020 at 22:24):

Hopefully it's not out of date. Category theory is not the place to start in lean really. There should be no problem doing these things but when working with stuff for which the API isn't ready for mathematicians there are complications

view this post on Zulip Jack J Garzella (Jun 24 2020 at 01:50):

@Keyao Peng Here's something that might not be too bad--you could try to formalize the result that a polynomial is irreducible if it is irreducible mod p. This is essential for many basic applications of Galois theory (e.g. an algebra qual) and I don't think it exists in mathlib (at least in this form)

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 08:47):

The reason the Galois theory repo was (and hence still is, at the time of writing) private was that I had initially hoped that a few Imperial undergraduates could knock off the entire course in the same way that they'd been demolishing 1st year course material, and it could be some little Imperial project. I made the private repo 2 years ago. I'll just check with the other people involved if they're happy to open it up, and then I'll make it public.


Last updated: May 16 2021 at 05:21 UTC