English
Push forward the action of R on M along a surjective ring hom f: R →+* S, obtaining an S-module structure on M with compatibility hsmul.
Русский
Перемещаем действие R на M вдоль сюръективного кольцового отображения f: R →+* S, получая структуру S-модуля на M и совместимость hsmul.
LaTeX
$$$\\text{moduleLeft} (f: R \\to+* S) (hf: \\text{Surjective } f) (hsmul: \\forall c, x, f c \\cdot x = c \\cdot x) : \\text{Module } S M$$$
Lean4
/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →+* S`.
See also `Function.Surjective.mulActionLeft` and `Function.Surjective.distribMulActionLeft`.
-/
abbrev moduleLeft {R S M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul S M] (f : R →+* S)
(hf : Function.Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) : Module S M :=
{
hf.distribMulActionLeft f.toMonoidHom
hsmul with
zero_smul := fun x => by rw [← f.map_zero, hsmul, zero_smul]
add_smul := hf.forall₂.mpr fun a b x => by simp only [← f.map_add, hsmul, add_smul] }
