English
Pull back a module structure along an injective additive monoid homomorphism f: M₂ →+ M. If hf is Injective f and smul : ∀ (c : R) (x), f (c • x) = c • f x, then M₂ inherits an R-module structure transported along f.
Русский
Переносим структуру модуля вдоль инъективного дополнительно моноидного гомоморфа f: M₂ →+ M. Если hf инъективно, и smul совместимо, тогда M₂ получает структуру модуля над R, переносимую через f.
LaTeX
$$$\\forall R\\ M\\ M₂\\ [\\text{Semiring } R] [\\text{AddCommMonoid } M] [\\text{Module } R M],\\ f : M₂ \\to+ M,\\ hf:\\text{Injective } f,\\ smul : \\forall (c : R) (x : M₂),\\ f (c \\cdot x) = c \\cdot f x \\Rightarrow\\ M₂ \\text{ has an } R\\text{-module structure transported along } f$$$
Lean4
/-- Pullback a `Module` structure along an injective additive monoid homomorphism.
See note [reducible non-instances]. -/
protected abbrev module [AddCommMonoid M₂] [SMul R M₂] (f : M₂ →+ M) (hf : Injective f)
(smul : ∀ (c : R) (x), f (c • x) = c • f x) : Module R M₂ :=
{
hf.distribMulAction f
smul with
add_smul := fun c₁ c₂ x => hf <| by simp only [smul, f.map_add, add_smul]
zero_smul := fun x => hf <| by simp only [smul, zero_smul, f.map_zero] }
