function.injective.mul_action on two functions

Stream: general

[Eric Wieser]

Does this generalization make sense?

/-- Pullback a multiplicative action along an injective map respecting `•`, while pulling the base monoid along g. -/
protected def function.injective.mul_action₂ [monoid α] [mul_action α β] [monoid γ] [has_scalar γ δ] (f : δ → β) (g : γ →* α)
  (hf : injective f) (smul : ∀ (c : γ) x, f (c • x) = g c • f x) :
  mul_action γ δ :=
{ smul := (•),
  one_smul := λ x, hf $ by rw [smul, g.map_one, one_smul _ (f x)],
  mul_smul := λ c₁ c₂ x, hf $ by simp only [smul, g.map_mul, mul_smul] }

Or does this factor into docs#function.injective.mul_action and some other definition that doesn't exist yet?

[Eric Wieser]

The application: I want to transport semimodule (⨁ i, A i) (⨁ i, A i) (aka docs#semiring.to_semimodule applied to docs#direct_sum.semiring) to semimodule (A 0) (A i)

[Eric Wieser]

Ah nevermind, it does factor - so this is now a "do we have the thing it factors to" queston: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Transporting.20.60mul_action.60.20along.20a.20.60monoid_hom.60/near/231975342