English
Push forward a module structure along a surjective additive monoid homomorphism f: M →+ M₂. If hf is Surjective f and smul : ∀ (c : R) (x), f (c • x) = c • f x, then M₂ inherits an R-module structure via f.
Русский
Переносим структуру модуля вдоль сюръективного аддитивного мономорфизма f: M →+ M₂. Пусть smul совместимо и f сюръективен; тогда M₂ получает структуру модуля над R через f.
LaTeX
$$$\\forall R\\ M\\ M_2\\ [\\text{Semiring } R] [\\text{AddCommMonoid } M] [\\text{Module } R M] (f : M \\to+ M_2) (hf : \\text{Surjective } f) (smul : \\forall (c : R) (x), f (c \\cdot x) = c \\cdot f x) \\Rightarrow M_2 \\text{ is an } R\\text{-module via } f$$$
Lean4
/-- Pushforward a `Module` structure along a surjective additive monoid homomorphism.
See note [reducible non-instances]. -/
protected abbrev module [AddCommMonoid M₂] [SMul R M₂] (f : M →+ M₂) (hf : Surjective f)
(smul : ∀ (c : R) (x), f (c • x) = c • f x) : Module R M₂ :=
{ toDistribMulAction := hf.distribMulAction f smul
add_smul := fun c₁ c₂ x => by
rcases hf x with ⟨x, rfl⟩
simp only [add_smul, ← smul, ← f.map_add]
zero_smul := fun x => by
rcases hf x with ⟨x, rfl⟩
rw [← f.map_zero, ← smul, zero_smul] }
