Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip Eric Wieser (Jan 13 2021 at 15:41):

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.

view this post on Zulip Eric Wieser (Jan 13 2021 at 15:42):

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

view this post on Zulip Anne Baanen (Jan 13 2021 at 15:53):

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

view this post on Zulip Eric Wieser (Jan 13 2021 at 16:23):

Not if R is not commutative I can't

view this post on Zulip Eric Wieser (Jan 13 2021 at 16:23):

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

view this post on Zulip Eric Wieser (Jan 13 2021 at 16:27):

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?

view this post on Zulip Anne Baanen (Jan 13 2021 at 18:02):

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.


Last updated: May 07 2021 at 20:11 UTC