algebra over an algebra is an algebra

Stream: Is there code for X?

[Kevin Buzzard]

Surely we have this in some form:

import Mathlib

example (A B C : Type) [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra B C] :
  Algebra A C := sorry

but exact? and #synth aren't finding it for me. This is data -- I want the one for which IsScalarTower A B C is true :-)

[Adam Topaz]

Is it called docs#Algebra.trans or something?

[Adam Topaz]

No, I guess not. You can always compose the structure maps and use docs#RingHom.toAlgebra

[Andrew Yang]

I would do ((algebraMap B C).comp (algebraMap A C)).toAlgebra and IsScalarTower.of_algebraMap_eq' rfl

[Andrew Yang]

The module version is docs#Module.compHom btw. Maybe we can have one for algebras.

[Kevin Buzzard]

Adam Topaz said:

No, I guess not. You can always compose the structure maps and use docs#RingHom.toAlgebra

I always worry about diamonds when doing this kind of thing.

[Andrew Yang]

Maybe #mwe ? This is fine in a local proof, and should be fine as long as you control where the algebra instances can come from.

[Kevin Buzzard]

In my example I'm not worried :-) If $R$ is the integers of a number field (or a Dedekind domain which isn't a field) with field of fractions $K$ then $R\subseteq K\subseteq \mathbb{A}_K^f\subseteq \prod_{v<\infty}K_v$ (third ring is docs#DedekindDomain.FiniteAdeleRing and 4th is docs#DedekindDomain.ProdAdicCompletions) and I keep needing everything to be an algebra over every smaller thing.

[Filippo A. E. Nuccio]

Andrew Yang said:

I would do ((algebraMap B C).comp (algebraMap A C)).toAlgebra and IsScalarTower.of_algebraMap_eq' rfl

I also believe that this is the right approach, and the IsScalarTower takes care of diamonds. In our project with @María Inés de Frutos Fernández we had this all over the places to pass from something global ($\mathbb{Z}$, $\mathbb{Q}$, ring of integers, number fields) to an extension of a local field.

[Kevin Buzzard]

Thanks! Obviously it can't be an instance in general because you can't predict B in advance but I'm in the same situation (four rings coming from number theory which I need to glue together, all types) and I'll try this approach.

[Eric Wieser]

To avoid diamonds, you may need to construct the smul field by hand

[Kevin Buzzard]

This is exactly what I'm asking about -- I don't know the pitfalls here. How should I define the smul field then? Are you saying the toAlgebra approach suggested above might lead to diamonds?

[Adam Topaz]

I don't see how smul would be defined without the structure maps except for something that looks silly like (a \bu 1) \bu b or something like that.

[Adam Topaz]

In the special case of adeles, of course you could be much more direct.

[Adam Topaz]

Do we have docs#Algebra.copy ?