Qbar

Stream: maths

[Kevin Buzzard]

Do we want to define an explicit algebraic closure type Qbar of rat? For example the subfield of complex? I think this might be necessary in practice. However there is a subtlety here. The reals are defined up to unique isomorphism by being a complete ordered archimedean field; Qbar is only defined up to isomorphism by being an algebraic closure of the rationals, and indeed its automorphism group is a topological group with an extremely subtle structure, all of which is invariant by inner automorphisms in some sense that mathematicians are good at keeping track of

[Johan Commelin]

I think that we'll want the algebraic closure of Q in C for various things. But otherwise, we should probably get used to the fact that we should only use the universal property of algebraic closures and not really on specific definitions.

[Kevin Buzzard]

So why do we have real?

[Johan Commelin]

Because I'm saying we should also have Qbar {Aside: ratbar :rat:, or algnum?}

[Kevin Buzzard]

Oh I see, I misunderstood. I think you're right, both will be useful.

[Chris Hughes]

So we use Qbar, and then choose some embedding into the complexes that we always use? But don't define it as a subfield?

[Johan Commelin]

I would just define it as a subfield...

[Johan Commelin]

I think that might simplify some of the proofs that will be part of the API

[Kevin Buzzard]

Wait -- do you want Qbar to be the type or the term?

[Johan Commelin]

I'm inclined to make it a type...

[Johan Commelin]

But it might still help when setting up the API to know that it is a subtype