## Stream: maths

### Topic: Qbar

#### Kevin Buzzard (Sep 14 2020 at 10:52):

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 (Sep 14 2020 at 10:54):

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 (Sep 14 2020 at 13:01):

So why do we have real?

#### Johan Commelin (Sep 14 2020 at 13:06):

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

#### Kevin Buzzard (Sep 14 2020 at 13:25):

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

#### Chris Hughes (Sep 14 2020 at 13:53):

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 (Sep 14 2020 at 13:56):

I would just define it as a subfield...

#### Johan Commelin (Sep 14 2020 at 13:57):

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

#### Kevin Buzzard (Sep 14 2020 at 13:59):

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

#### Johan Commelin (Sep 14 2020 at 14:00):

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

#### Johan Commelin (Sep 14 2020 at 14:00):

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

Last updated: May 11 2021 at 16:22 UTC