Zulip Chat Archive

Stream: maths

Topic: on real numbers

view this post on Zulip Johan Commelin (Oct 08 2019 at 06:22):

(1) Let KK be a number field: i.e. a finite field extension of Q\mathbb{Q}. One of the key insights in algebraic number theory is that you can study KK, by looking at all its different completions. For K=QK = \mathbb{Q}, this leads to the real numbers and the pp-adic numbers where pp ranges over the primes. For other KK, the completions can be the reals, the complexes, or any finite extension of the pp-adics.

(2) Suppose we develop Galois theory. We will be delighted to be able to speak about invariant subfields, etc. Easy example, the subfield of the complex numbers that is invariant under complex conjugation.

In both of these examples, we end up with fields that are obviously naturally canonically equal to real. Except that Lean will not agree, and we will not be able to apply any of the lemmas from the library.

Wouldn't it be prudent to refactor the library to use any of the well-known characteristic predicates for the reals? I can imagine this might be a nice project for a beginner.

view this post on Zulip Patrick Massot (Oct 08 2019 at 07:33):

Do we have that many lemmas about real numbers that don't go through instances of general classes?

view this post on Zulip Patrick Massot (Oct 08 2019 at 07:34):

We will still need a reference implementation of real numbers anyway.

view this post on Zulip Chris Hughes (Oct 08 2019 at 08:19):

Maybe we should do Galois theory using characteristic predicates for subfield instead. Same goes for characteristic predicates of completions.

view this post on Zulip Johan Commelin (Oct 08 2019 at 08:26):

Mwah, I guess Galois theory will be a Galois correspondence between subfield K L and subgroup G

view this post on Zulip Kevin Buzzard (Oct 08 2019 at 09:22):

The completion of a number field at an infinite complex place is a field which is non-canonically isomorphic to the complex numbers. It is an algebraic closure $\overline{\mathbb{R}}$ of the real numbers, with two square roots $\alpha$ and $\beta$ of $-1$. Identifying it with the complexes requires choosing one of these roots and decreeing that its imaginary part is positive. This seems to me to be the "next layer" of the problem, where we have theorems about the complexes, and we'd like to apply them to a field which is non-uniquely isomorphic to the complexes (as opposed to the reals, where all isomorphisms are unique)

Last updated: May 19 2021 at 02:10 UTC