Pi.algebra

Stream: Is there code for X?

[Andrew Yang]

Do we not have this? Is this just missing or does it cause diamonds?

import Mathlib.Algebra.Algebra.Defs
import Mathlib.Algebra.Group.Action.Pi
import Mathlib.Algebra.Ring.Pi

variable {ι : Type*} {R A : ι → Type*}
variable [∀ i, CommSemiring (R i)] [∀ i, Semiring (A i)] [∀ i, Algebra (R i) (A i)]

instance : Algebra (Π i, R i) (Π i, A i) where
  __ := Pi.ringHom fun i ↦ (algebraMap (R i) (A i)).comp (Pi.evalRingHom R i)
  commutes' r a := funext fun i ↦ Algebra.commutes _ _
  smul_def' r a := funext fun i ↦ by simp [Algebra.smul_def]

[Eric Wieser]

It causes diamonds, take A i = (Π i, R i)

[Eric Wieser]

Of course we already have docs#Pi.smul' which causes the same diamond...

[Andrew Yang]

Since Π i, R i is not an R i algebra and only a Π i, R i algebra, I think your example does not cause diamonds. But I think diamonds will probably appear if furthermore R = fun i ↦ R₀.

So the question is probably: does it cause more diamonds than docs#Pi.smul' ?
If not, I guess it is probably fine to have it?

[Eric Wieser]

Andrew Yang said:

Since Π i, R i is not an R i algebra and only a Π i, R i algebra

If R i = S everywhere, then it is both

[Eric Wieser]

Andrew Yang said:

If not, I guess it is probably fine to have it?

Certainly we should have it as a @[reducible] def, I'm a little less sold that we should continue the slippery slope of adding more data-inducing instances with known diamonds