instIsMonHomHom

Mathlib.CategoryTheory.Monoidal.Mon_

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

English

A map f: X → Y between monoid objects is a monoid homomorphism if f.hom is MonHom.

Русский

Гомоморфизм между моноидальными объектами является моноидным гомоморфизмом, если f.hom — MonHom.

LaTeX

$$$\\text{IsMonHom}(f) \\;\\text{for } f: X\\to Y$$$

Lean4

instance {M N : Mon C} (f : M ⟶ N) : IsMonHom f.hom :=
  f.isMonHom_hom

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

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

Разделы

Аффилиация

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