A typeclass for `(r : R) (x y : A) : (r • x)*y = r • (x*y)`

Stream: Is there code for X?

[Eric Wieser]

This lemma exists as docs#smul_mul_assoc, but that requires A to be an algebra.

This property also holds for A = α →₀ R, but there can be no algebra instance on α →₀ R because it has no 1.

[Eric Wieser]

So is there a typeclass that can be extracted from algebra that sits somewhere between algebra and semimodule?

[Anne Baanen]

I guess you can fake it with docs#is_scalar_tower combined with docs#smul_eq_mul?

[Eric Wieser]

Not if R is not commutative I can't

[Eric Wieser]

But I guess I don't really care about that case

[Eric Wieser]

Can you give a sketch of the is_scalar_tower solution? What I have right now is

import data.finsupp.pointwise

namespace finsupp

section
variables {α R A : Type*} [comm_semiring R] [semiring A] [algebra R A]

@[simp] lemma mul_smul_comm (s : R) (x y : α →₀ A) :
  x * (s • y) = s • (x * y) :=
by { ext, simp [←mul_assoc]}

@[simp] lemma smul_mul_assoc (r : R) (x y : α →₀ A) :
  (r • x) * y = r • (x * y) :=
by { ext, simp }
end

end finsupp

What arguments are you suggesting I instantiate is_scalar_tower with in order to avoid needing to define finsupp.mul_smul_comm at all?

[Anne Baanen]

Eric Wieser said:

Can you give a sketch of the is_scalar_tower solution?

You are right, I can't really put anything together that works nicely. I guess the best is indeed to add a new class in between semimodule and algebra.