English
If f : S →+* R is a ring hom, then there is a canonical S-module structure on any R-module M given by s • m = f s • m.
Русский
Если f : S →+* R — кольцевое гомоморфизм, существует каноническая S-модульная структура на любом R-модуле M, заданная действием s • m = f(s) • m.
LaTeX
$$$\\text{compHom }(f) : \\text{Module } S M$ with \\; s \\cdot m := f(s) \\cdot m$$$
Lean4
/-- Compose a `Module` with a `RingHom`, with action `f s • m`.
See note [reducible non-instances]. -/
abbrev compHom [Semiring S] (f : S →+* R) : Module S M :=
{ MulActionWithZero.compHom M f.toMonoidWithZeroHom, DistribMulAction.compHom M (f : S →* R) with
-- Porting note: the `show f (r + s) • x = f r • x + f s • x` wasn't needed in mathlib3.
-- Somehow, now that `SMul` is heterogeneous, it can't unfold earlier fields of a definition for
-- use in later fields. See
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication
-- TODO(jmc): there should be a rw-lemma `smul_comp` close to `SMulZeroClass.compFun`
add_smul := fun r s x => show f (r + s) • x = f r • x + f s • x by simp [add_smul] }
