Zulip Chat Archive

Stream: maths

Topic: simple field theory


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:45):

There is a branch splitting_fields on the community repo.

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:45):

Also: welcome!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:46):

@Kenny Lau Defined the perfect closure of a field.

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:47):

See field_theory/perfect_closure.lean.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:48):

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

view this post on Zulip 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:

view this post on Zulip Joey van Langen (Dec 04 2018 at 14:51):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Dec 04 2018 at 15:08):

I wrote a roadmap once

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 04 2018 at 15:29):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 04 2018 at 20:07):

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

view this post on Zulip 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: May 12 2021 at 07:17 UTC