Zulip Chat Archive

Stream: maths

Topic: galois theory / splitting fields


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...

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.

Johan Commelin (Mar 05 2019 at 09:05):

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

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

Kenny Lau (Mar 05 2019 at 09:12):

even when Mario said it’s alright?

Johan Commelin (Mar 05 2019 at 09:13):

I really wish these issues can be resolved soon.

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.

Kevin Buzzard (Mar 05 2019 at 09:20):

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

Chris Hughes (Mar 05 2019 at 09:21):

Yes.

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?

Chris Hughes (Mar 05 2019 at 09:22):

Free comm ring is used for direct limit

Kevin Buzzard (Mar 05 2019 at 09:22):

oh :-)

Chris Hughes (Mar 05 2019 at 11:25):

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

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: Dec 20 2023 at 11:08 UTC