Zulip Chat Archive

Stream: maths

Topic: simple field theory

Joey van Langen (Dec 04 2018 at 14:42):

I would like to work on some simple results about fields to contribute to the math library. Results that seem achievable are: field extensions and their degree, splitting fields, the existence and uniqueness of finite fields, maybe some galois theory. Is anyone working in this direction? If so, what has already been done?

Johan Commelin (Dec 04 2018 at 14:45):

There is a branch splitting_fields on the community repo.

Johan Commelin (Dec 04 2018 at 14:45):

Also: welcome!

Johan Commelin (Dec 04 2018 at 14:45):

I think that branch has a definition of the splitting field, but not yet the proofs of the interesting properties.

Johan Commelin (Dec 04 2018 at 14:46):

@Kenny Lau Defined the perfect closure of a field.

Johan Commelin (Dec 04 2018 at 14:47):

See field_theory/perfect_closure.lean.

Johan Commelin (Dec 04 2018 at 14:48):

In general, Kenny and @Chris Hughes have been doing some stuff. So it would be good to check with them before you start big projects.

Johan Commelin (Dec 04 2018 at 14:48):

I think Kenny has most of the definition of algebraic closure.

Johan Commelin (Dec 04 2018 at 14:49):

Uniqueness of finite fields isn't there, as far as I know. Galois theory is completely missing. But I'dd love to see it there, so please work on it :smiley:

Joey van Langen (Dec 04 2018 at 14:51):

Thanks for all the information. Looking at the sources you mentioned now

Johan Commelin (Dec 04 2018 at 14:53):

If you decide to work on splitting fields, it shouldn't be hard to give you access to the community repo, so that you can push your contributions

Chris Hughes (Dec 04 2018 at 15:04):

In general, Kenny and @Chris Hughes have been doing some stuff. So it would be good to check with them before you start big projects.

I haven't done anything that hasn't been merged.

Johan Commelin (Dec 04 2018 at 15:07):

Right, but it would also be a pity if people redid stuff that you did that isn't merged.

Kenny Lau (Dec 04 2018 at 15:08):

I wrote a roadmap once

Kenny Lau (Dec 04 2018 at 15:09):

https://github.com/kckennylau/Lean/blob/master/algebraic-closure-roadmap.md
https://github.com/kckennylau/Lean/blob/master/Galois-theory-roadmap.md
https://github.com/semorrison/lean-category-theory/blob/master/schemes_roadmap.md

Kevin Buzzard (Dec 04 2018 at 15:29):

@Kenny Lau why not make your roadmaps into mathlib issues? They'd be easier to find.

Scott Morrison (Dec 04 2018 at 19:03):

My student @Aditya Agarwal has expressed some interest in doing some Galois theory over the summer. He's at a conference at the moment, so I'm not sure if he's started on anything yet.

Kevin Buzzard (Dec 04 2018 at 20:07):

@Scott Morrison you presumably mean Aussie summer i.e. right now?

Chris Hughes (Dec 12 2018 at 18:35):

I've started work on splitting fields https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Splitting.20fields

Last updated: Dec 20 2023 at 11:08 UTC