multiple norms on a field

Stream: mathlib4

[Kevin Buzzard]

In the theory of number fields one wants to consider many norms on a field at the same time. For example, the definition of the infinite adeles of a number field $K$ is the product of all the archimedean completions of $K$. To give a concrete example, the infinite adeles of $\mathbb{Q}(\sqrt{2})$ is $\R\oplus\R$, because there are two ring maps $\mathbb{Q}(\sqrt{2})\to\R$ (sending $\sqrt{2}$ to $\pm\sqrt{2}$) and this gives two (very different) absolute values on $\mathbb{Q}(\sqrt{2})$. You can see they're different because numbers like $(1+\sqrt{2})^{100000}\in K$ are huge with respect to one norm and tiny with respect to the other.

When making the infinite adeles of $K$, as @Salvatore Mercuri does in #16483, one first runs through these real-valued archimedean absolute values (up to equivalence, so there are only finitely many), completes $K$ with respect to each one, and then takes the product of the completions. Of course the problem is that typeclass inference (and in particular the completion machinery, which runs on uniform spaces) only expects one metric on $K$ and the different norms give different metrics. There are perhaps three ways to solve this. The first is the usual @ / letI dance, putting temporary structures on $K$ in the middle of proofs; this is not ideal. The second is to use a data-carrying typeclass, which feels to me like a better version of the first solution. We can see this idiom already in mathlib, as the phenomenon shows up in the nonarchimedean setting, with Valuation R Γ₀ denoting the type of all nonarchimedean Γ₀-valued norms on R, and [Valued R Γ₀] a data-carrying typeclass indicating that R has a preferred nonarch norm (from which typeclass inference can deduce a topology/uniformity on R). However the typeclass approach isn't ideal because one doesn't always want to commit to one valuation on R; see here for example for something in mathlib with a lot of @s everywhere.

In #16483 Salvatore proposes a third approach, namely a type synonym.

/-- Type synonym for a semiring which depends on an absolute value. This is a function that takes
an absolute value on a semiring and returns the semiring. We use this to assign and infer instances
on a semiring that depend on absolute values. -/
@[nolint unusedArguments]
def WithAbs {R S : Type*} [Semiring R] [OrderedSemiring S] :
    AbsoluteValue R S → Type _ := fun _ => R

variable {K : Type*} [Field K] (v : AbsoluteValue K ℝ)

instance normedField : NormedField (WithAbs v) :=...

The idea is that WithAbs v is now R with a canonical absolute value, so one can define the infinite adeles of $K$ as the product over WithAbs v as v runs through the archimedean real-valued absolute values on K.

It feels to me like this design question is now blocking multiple PRs on adeles, and I'm motivated to get this going because I need to use adeles in FLT to prove that spaces of quaternionic modular forms are finite-dimensional and I want to beat the complex analysts who are trying to prove the same finiteness theorems about classical modular forms. Do people have any opinions on the pros and cons of the approaches above? In particular, the PR mentioned above only has one letI in it and no @s in sight, so I'm now thinking that the type synonym approach might be superior.

Also pinging @Filippo A. E. Nuccio and @Riccardo Brasca who have already reviewed the PR.

[Yakov Pechersky]

How about using docs#AbstractCompletion?

[Yakov Pechersky]

Or are even the uniformities different for the different abs?

[Kevin Buzzard]

Yes they're completely different. $\sqrt{2}$ is close to $1.4$ with one, and close to $-1.4$ with the other. The rationals stay the same but the $\sqrt{2}$ moves; each metric is highly non-continuous (in fact discontinuous everywhere) with respect to the others.

The analyst thinks of $\mathbb{Q}(\sqrt{2})$ as being a subfield of $\mathbb{R}$; the algebraist thinks of it as an abstract 2-dimensional $\mathbb{Q}$-vector space with no preferred embedding into the reals, and two equally "valid" maps which yield two totally different topologies on $\mathbb{Q}(\sqrt{2})$.

[Yakov Pechersky]

One thing about Valued K G0 is that you might have totally different G0 and G0' but the norms end up being the same. Perhaps in your case you are okay with restricting your AbsoluteValues to all have the same codomain.

[Kevin Buzzard]

No the topologies are totally unrelated, even though they all have the same codomain $\mathbb{R}$.

[Yakov Pechersky]

Yes, understood that point. I am separately saying a detail about Valued

[Kevin Buzzard]

In the nonarchimedean case we resrict to valuations having values in ℤₘ₀ but there are in this case infinitely many! When I say "valuation" I really mean "equivalence class of valuation" where two valuations are equivalent iff they induce the same topology.

[Yakov Pechersky]

Yup. I like the type synonym approach in the WithAbs since you give the v directly, instead of encoding it into the data of the TC.

[Riccardo Brasca]

I don't have a clear preference here, but I think I agree with Kevin. More importantly, I think we should not wait forever to find the perfect solution (that may not exist). We can always refactor later (of course it would be better to choose the right solution from the beginning, but this is not always doable).

[Jireh Loreaux]

I think the type synonyms approach is the "obvious" approach (I don't mean this condescendingly; I mean that it's the approach that ticks all the boxes easily). This is what we do throughout the library (e.g., docs#WithLp, docs#WithCStarModule, etc.)

[Kevin Buzzard]

Yeah I asked precisely because I wanted to hear what was going on in other places in the library! I think that we might have missed a trick with Valued. The other examples Jireh points out are also defs not classes. This is great, I think we can get this PR back up and running.

[Riccardo Brasca]

Note the new split PR #17998

[Salvatore Mercuri]

Also, credit to @Andrew Yang for the WithAbs suggestion in the first place

[Andrew Yang]

It's been so long I already forgotten; I was just about to comment something like this is of course the way to do it :sweat_smile:

[Johan Commelin]

Is it valuable to make K_v be defeq to Real or Complex?

[Salvatore Mercuri]

Johan Commelin said:

Is it valuable to make K_v be defeq to Real or Complex?

We did discuss this a bit on an older PR -- I'll quote Andrew again here https://github.com/leanprover-community/mathlib4/pull/13577#issuecomment-2158292781

I think case splitting in the definition on whether an infinite place is complex or not might make things cumbersome (whether that's using "if then else" or separate defs)