Zulip Chat Archive

Stream: Is there code for X?

Topic: Transporting `mul_action` along a `monoid_hom`


view this post on Zulip Eric Wieser (Mar 26 2021 at 14:38):

Do we have this definition?

/-- If `M` has an `R`-action, then it has an `R'`-action through `f` -/
def monoid_hom.transport_mul_action {R R' : Type*} (M : Type*) [monoid R] [monoid R'] [mul_action R M] (f : R' →* R) :
  mul_action R' M :=
{ smul := ()  f,
  one_smul := λ m, by simp,
  mul_smul := λ r s m, by simp [mul_smul] }

view this post on Zulip Eric Wieser (Mar 26 2021 at 15:03):

Or these two from the same family?

def monoid_hom.transport_distrib_mul_action [monoid R] [monoid R'] [add_monoid M] [distrib_mul_action R M]
  (f : R' →* R) :
  distrib_mul_action R' M :=
{ smul := ()  f,
  smul_zero := λ x, smul_zero (f x),
  smul_add := λ x, smul_add (f x),
  ..f.transport_mul_action M }
def ring_hom.transport_semimodule [semiring R] [semiring R'] [add_comm_monoid M] [semimodule R M]
  (f : R' →+* R) :
  semimodule R' M :=
{ smul := ()  f,
  zero_smul := λ x, by simp [zero_smul],
  add_smul := λ r s x, by simp [add_smul],
  ..f.to_monoid_hom.transport_distrib_mul_action M }

view this post on Zulip Eric Wieser (Mar 26 2021 at 16:16):

#6895, this generalizes docs#restrict_scalars.semimodule, and I think we don't have it yet.

view this post on Zulip Eric Wieser (Mar 29 2021 at 10:25):

Whoops, we had this already as docs#mul_action.comp_hom

view this post on Zulip Johan Commelin (Mar 29 2021 at 10:27):

We really need to get that algebraic hierarchy build up and running

view this post on Zulip Eric Wieser (Mar 29 2021 at 10:27):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Duplicate.20mul_action.20defs/near/232246589 for voting on the better name


Last updated: May 07 2021 at 21:10 UTC