Transporting `mul_action` along a `monoid_hom`

Stream: Is there code for X?

[Eric Wieser]

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] }

[Eric Wieser]

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 }

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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