Zulip Chat Archive

Stream: maths

Topic: Qbar


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 13:01):

So why do we have real?

view this post on Zulip Johan Commelin (Sep 14 2020 at 13:06):

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

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 13:25):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 14 2020 at 13:56):

I would just define it as a subfield...

view this post on Zulip Johan Commelin (Sep 14 2020 at 13:57):

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

view this post on Zulip Kevin Buzzard (Sep 14 2020 at 13:59):

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

view this post on Zulip Johan Commelin (Sep 14 2020 at 14:00):

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

view this post on Zulip 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