mapHom_id — Mathlib

English

The mapHom construction sends the identity monoid hom to the identity functor on the corresponding single-object category.

Русский

Конструкция mapHom отправляет тождественный гомоморфизм моноидов в тождественный функтор соответствующей категории с одним объектом.

LaTeX

$$$mapHom\\,M\\,M\\,(\\mathrm{id}_M)= \\mathbb{1}_{\\mathrm{SingleObj} M}$$$

Lean4

theorem mapHom_id : mapHom M M (MonoidHom.id M) = 𝟭 _ :=
  rfl

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