comp_toFunctor — Mathlib

English

The functor corresponding to the composition of monoid homomorphisms equals the composition of the corresponding functors.

Русский

Функтор, соответствующий композиции гомоморфизмов, равен композиции соответствующих функторов.

LaTeX

$$$ (g\\circ f).toFunctor = f.toFunctor \\circ g.toFunctor $$$

Lean4

@[simp]
theorem comp_toFunctor (f : M →* N) {P : Type w} [Monoid P] (g : N →* P) :
    (g.comp f).toFunctor = f.toFunctor ⋙ g.toFunctor :=
  rfl

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