Zulip Chat Archive

Stream: maths

Topic: composition of algebra structures?


view this post on Zulip 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?

view this post on Zulip 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, C\mathbb{C} as a Q\mathbb{Q} algebra is not defined to be the composition of QR\mathbb{Q} \to \mathbb{R} and RC\mathbb{R}\to \mathbb{C}

view this post on Zulip 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.

view this post on Zulip 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