on real numbers

Stream: maths

[Johan Commelin]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Chris Hughes]

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

[Johan Commelin]

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

[Kevin Buzzard]

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)