## 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?

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

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: May 11 2021 at 00:31 UTC