instIsMonHom

Mathlib.CategoryTheory.Monoidal.Mon_

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.map.instIsMonHom

English

Relates unit isomorphism to braiding identity; braiding with unit reduces to identity.

Русский

Связь единичной изоморфности и braiding: braiding с единицей сводится к тождественному.

LaTeX

$$$η ≫ (β_{X,Y}).hom = η$$$

Lean4

instance instIsMonHom : IsMonHom (F.map f)
    where
  one_hom := by simp [← map_comp]
  mul_hom := by simp [← map_comp]

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

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

Разделы

Аффилиация

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