## Stream: maths

### Topic: composition of algebra structures?

#### Kevin Buzzard (Feb 09 2020 at 01:20):

example {R : Type*} [comm_ring R] {A : Type*} [comm_ring A] {B : Type*} [comm_ring B]
[algebra R A] [algebra A B] : algebra R B := by apply_instance


This doesn't work -- should it?

#### Chris Hughes (Feb 09 2020 at 20:02):

This instance is defined on algebra.comap R A B, which is a Type alias for either R or B, I don't remember which. It's bad practice to use it in statements though, because for example, $\mathbb{C}$ as a $\mathbb{Q}$ algebra is not defined to be the composition of $\mathbb{Q} \to \mathbb{R}$ and $\mathbb{R}\to \mathbb{C}$

#### Chris Hughes (Feb 09 2020 at 20:04):

The best solution we have right now is a bit yucky, but you should just have three instances as assumptions [algebra R A], [algebra A B] and [algebra R B], as well as the assumption that the diagram commutes. Some better interface will be needed at some point for this.

#### Kevin Buzzard (Feb 09 2020 at 23:03):

example
{R : Type*} [comm_ring R] {A : Type*} [comm_ring A]
[algebra R A] {σ : Type} :
by letI : algebra R (mv_polynomial σ A) :=
@algebra.comap.algebra R A (mv_polynomial σ A) _ _ _ _ _;
exact
(some theorem which needs A[sigma] to be an R-algebra)
...


Eew.

Last updated: May 06 2021 at 17:38 UTC