composition of algebra structures?

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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.