galois theory / splitting fields

Stream: maths

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Chris Hughes]

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]

even when Mario said it’s alright?

[Johan Commelin]

I really wish these issues can be resolved soon.

[Chris Hughes]

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

[Kevin Buzzard]

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

[Chris Hughes]

Yes.

[Kevin Buzzard]

@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]

Free comm ring is used for direct limit

[Kevin Buzzard]

oh :-)

[Chris Hughes]

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

[Johan Commelin]

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