Zulip Chat Archive
Stream: Is there code for X?
Topic: Is there code for Galois theory?
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?
Patrick Massot (Jun 23 2020 at 15:41):
Mostly manpower
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
Keyao Peng (Jun 23 2020 at 15:45):
Yeah, I am new to Lean, but I'd like to have a try.
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.
Patrick Massot (Jun 23 2020 at 15:50):
You should ask @Chris Hughes too
Johan Commelin (Jun 23 2020 at 15:53):
@Jack J Garzella Is also interested in doing this, I think.
Adam Topaz (Jun 23 2020 at 15:55):
Does mathlib have code for etale algebras?
Adam Topaz (Jun 23 2020 at 15:55):
I suppose not.
Patrick Massot (Jun 23 2020 at 15:55):
No
Johan Commelin (Jun 23 2020 at 16:01):
You can git grep "tale"
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?
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
Patrick Massot (Jun 23 2020 at 16:17):
But Markus knows.
Patrick Massot (Jun 23 2020 at 16:17):
@Markus Himmel?
Markus Himmel (Jun 23 2020 at 16:29):
Unfortunately, I don't think my work helps here in its current form
Patrick Massot (Jun 23 2020 at 16:29):
Is it getting closer to mathlib by the way?
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.
Patrick Massot (Jun 23 2020 at 16:33):
I think you should also write a paper if you haven't done so already.
Markus Himmel (Jun 23 2020 at 16:35):
Honestly, I don't think there is anything in my work that would warrant a paper.
Patrick Massot (Jun 23 2020 at 16:36):
The automation part looks really new to me (but I'm not an expert).
Johan Commelin (Jun 23 2020 at 16:36):
How many computers have verified 5 line proofs of the four lemma?
Johan Commelin (Jun 23 2020 at 16:37):
I'm ignorant, of course, but I'm not aware of other provers have such automation
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.
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!
Kevin Buzzard (Jun 23 2020 at 16:43):
Teach others how trivial it is! People can learn from your work.
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.
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.
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.
Kevin Buzzard (Jun 23 2020 at 19:38):
Is normal and separable and splitting field in mathlib?
Kenny Lau (Jun 23 2020 at 19:39):
I am working on separable. Normal is in galois repo.
Alex J. Best (Jun 23 2020 at 19:41):
What is galois repo?
Kevin Buzzard (Jun 23 2020 at 19:42):
The private IC repo
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!
Adam Topaz (Jun 23 2020 at 19:52):
Does mathlib have the theorem that any field embeds in some algebraically closed field?
Patrick Massot (Jun 23 2020 at 19:53):
No.
Patrick Massot (Jun 23 2020 at 19:53):
It has been discussed a lot, but never converged.
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.
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.
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...
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.
Alex J. Best (Jun 23 2020 at 19:56):
Whats the status of https://github.com/leanprover-community/mathlib/pull/1297 ?
Patrick Massot (Jun 23 2020 at 20:05):
Given the age of this PR, it may be faster to restart from scratch.
Kevin Buzzard (Jun 23 2020 at 20:16):
over 1000 lines
Patrick Massot (Jun 23 2020 at 20:17):
How many refactors in the mean time?
Kevin Buzzard (Jun 23 2020 at 20:17):
over 10000 lines
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?
Kenny Lau (Jun 23 2020 at 20:23):
I believe that's the point
Reid Barton (Jun 23 2020 at 20:29):
I think the PR is on hold because Chris wants to do it a different way.
Keyao Peng (Jun 23 2020 at 20:31):
Can I define a category of all algebraic extension of a field k?
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.
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.
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?
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.
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.
Patrick Massot (Jun 23 2020 at 20:51):
You should probably avoid category theory in the beginning.
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.
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
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)
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: Dec 20 2023 at 11:08 UTC