compHom — Mathlib

English

Given MulSemiringAction M on R and a monoid hom f: N →* M, one gets an action of N on R by n • r := f(n) • r, i.e., transporting the M-action along f.

Русский

Если имеется действие MulSemiringAction M на R и гомоморфизм f: N →* M, то получается действие N на R, задаваемое n • r := f(n) • r (переносящее действие M через f).

LaTeX

$$$\\forall n:\\, N,\\; \\forall r:\\, R:\\; n \\cdot r = f(n) \\cdot r$$$

Lean4

/-- Compose a `MulSemiringAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances]. -/
abbrev compHom (f : N →* M) [MulSemiringAction M R] : MulSemiringAction N R :=
  { DistribMulAction.compHom R f, MulDistribMulAction.compHom R f with }

Похожие утверждения