instIsIsoHom

Mathlib.CategoryTheory.Monoidal.Mon_

URI: https://scilib.ai/kg/mathlib#Mon.instIsIsoHom

English

The (second) Mon initial object exists as the trivial monoid object.

Русский

Существование начального Mon объекта — тривиальный моноид.

LaTeX

$$$\\text{Mon\\,C has initial object }\\cong \\text{trivial Mon } C$$$

Lean4

instance {M N : Mon C} {f : M ⟶ N} [IsIso f] : IsIso f.hom :=
  inferInstanceAs <| IsIso <| (forget C).map f

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

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

Разделы

Аффилиация

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