id_toFunctor

Mathlib.CategoryTheory.SingleObj

URI: https://scilib.ai/kg/mathlib#MonoidHom.id_toFunctor

English

The monoid identity homomorphism corresponds to the identity functor.

Русский

Гомоморфизм единичного моноидa соответствует тождественному функтору.

LaTeX

$$$\\mathrm{id}_M.toFunctor = \\mathrm{Id}_{\\mathrm{SingleObj} M}$$$

Lean4

@[simp]
theorem id_toFunctor : (id M).toFunctor = 𝟭 _ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru