InfiniteAdeleRing is a real algebra

Stream: Is there code for X?

[William Coram]

As part of the FLT project I need the following sorry filled:

import Mathlib

variable (K : Type*) [Field K] [NumberField K]
variable (D : Type*) [DivisionRing D] [Algebra K D]

local instance : Algebra ℝ (D ⊗[K] (NumberField.InfiniteAdeleRing K)) := by

sorry

I had hoped to use something like Algebra.TensorProduct.leftAlgebra to reduce this to showing the InfiniteAdeleRing K is a $\R$-algebra. But this causes two problems:

Firstly, I cannot find a similar statement to Algebra.TensorProduct.leftAlgebra for right algebras, namely Algebra.TensorProduct.rightAlgebra exists but has $S = B$ - is this due to the set up of Tensor products, or is some API missing?

Secondly, is there an existing result for saying the infinite adele ring is an $\R$-algebra? I have not been able to find it and Kevin thinks it would be surprising if this doesn't already exist.

Any help would be appreciated.

[Ruben Van de Velde]

2) Loogle says there are only 15 declarations about docs#NumberField.InfiniteAdeleRing, and docs#NumberField.InfiniteAdeleRing.instAlgebra is the only one that's even slightly related as far as I can tell

[Kevin Buzzard]

Huh, that's definitely no good, that's the $K$-algebra structure. Another way of thinking about the question mathematically: the $\mathbb{R}$-algebra structure on the tensor product is coming from an $\mathbb{R}$-algebra structure on NumberField.InfiniteAdeleRing K and another definition of this type would be $K\otimes_{\mathbb{Q}}\mathbb{R}$, so the $\mathbb{R}$-algebra structure is precisely the "opposite" of the (existing) $K$-algebra structure.

For Algebra.TensorProduct.rightAlgebra FLT can proudly offer you the mathlib-unapproved open scoped TensorProduct.RightActions whereupon it should happen magically.

[William Coram]

Kevin Buzzard said:

For Algebra.TensorProduct.rightAlgebra FLT can proudly offer you the mathlib-unapproved open scoped TensorProduct.RightActions whereupon it should happen magically.

I am not convinced the TensorProduct.RightActions file has exactly what we want.
e.g.
scoped instance : Algebra S (B ⊗[R] S) where ...
which is exactly the statement of Algebra.TensorProduct.rightAlgebra.
Similarly, I cannot use
def Algebra.TensorProduct.comm : A ⊗[R] B ≃ₐ[A] B ⊗[R] A where ...
as the algebra equivalence is over A - which is not $\R$ in the case we need.

Perhaps, I am missing something ?

[William Coram]

As part of FLT we have concocted the following instance of InfiniteAdeleRing being an $\R$-algebra.

import Mathlib

open NumberField InfiniteAdeleRing

variable (K : Type*) [Field K] [NumberField K]

noncomputable instance : Algebra ℝ (InfiniteAdeleRing K) :=
  (ringEquiv_mixedSpace K|>.symm.toRingHom.comp (algebraMap ℝ _)).toAlgebra

Does this seem acceptable? Or is there a chance this could cause problems?