Zulip Chat Archive

Stream: maths

Topic: galois theory / splitting fields


view this post on Zulip Johan Commelin (Mar 05 2019 at 09:02):

The splitting fields PR was just closed. What is the status of algebraic closures / galois theory / splitting fields, etc? After Lean Together I thought people decided there was a short Zorn-like argument using some sufficiently big type. But this hasn't materialized yet...

view this post on Zulip Chris Hughes (Mar 05 2019 at 09:02):

The zorn argument is much easier with direct limit I think, so I was waiting for that.

view this post on Zulip Johan Commelin (Mar 05 2019 at 09:05):

Didn't Kenny do direct limits a long time ago?

view this post on Zulip Chris Hughes (Mar 05 2019 at 09:07):

Yes, but there was something wrong with that, but I'm not sure what. There's another PR open now, but I'm putting off merging it, because I don't like having free_comm_ring, when we already have mv_polynomial int

view this post on Zulip Kenny Lau (Mar 05 2019 at 09:12):

even when Mario said it’s alright?

view this post on Zulip Johan Commelin (Mar 05 2019 at 09:13):

I really wish these issues can be resolved soon.

view this post on Zulip Chris Hughes (Mar 05 2019 at 09:13):

I'd rather not have it there. There's no functions defined on it that don't make sense on mv polynomial.

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:20):

So is there a PR containing both direct limits and free_comm_ring?

view this post on Zulip Chris Hughes (Mar 05 2019 at 09:21):

Yes.

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:21):

@Kenny Lau could you split it into two PR's so we can get direct limits without entering into the free_comm_ring debate?

view this post on Zulip Chris Hughes (Mar 05 2019 at 09:22):

Free comm ring is used for direct limit

view this post on Zulip Kevin Buzzard (Mar 05 2019 at 09:22):

oh :-)

view this post on Zulip Chris Hughes (Mar 05 2019 at 11:25):

@Kenny Lau Does the branch mv_polynomial_direct_limit work? Why not use that?

view this post on Zulip Johan Commelin (Mar 07 2019 at 08:50):

I don't know anything about these issues. Is the problem once again that mv_polynomial is to slow to be usable?


Last updated: May 11 2021 at 00:31 UTC