Functoriality of infinite completion for number fields

Stream: FLT

[Kevin Buzzard]

I don't think we have this:

import Mathlib.NumberTheory.NumberField.Completion

open NumberField

variable (K L : Type*) [Field K] [Field L] [NumberField K] [NumberField L]
  (f : K →+* L) (w : InfinitePlace L) (v : InfinitePlace K)

example (h : w.comap f = v) : v.Completion →SL[f] w.Completion := sorry

In fact what we really need for functoriality (both algebraic and topological) of adele rings is a →SA[f] (continuous semilinear algebra morphism) but we don't seem to even have semilinear algebra morphisms, let alone continuous ones...

[Andrew Yang]

Do we need it as a bundled hom?

[Kevin Buzzard]

Not necessarily, it's just that this seemed to be a nice way of saying it.

[Kevin Buzzard]

Ultimately I want to prove $K_\infty\otimes_KL=L_\infty$ (algebraically and topologically), and the construction above is one way of doing it (by $K_\infty$ I mean InfiniteAdeleRing K). Another approach would be to show $K_\infty=K\otimes_{\mathbb{Q}}\R$.

[Salvatore Mercuri]

I have a version of this I will PR very soon, been a busy start to the year but should get around to it this week!