instIsMonHomHomBraiding

Mathlib.CategoryTheory.Monoidal.Mon_

URI: https://scilib.ai/kg/mathlib#MonObj.instIsMonHomHomBraiding

English

Existence of IsMonHom for braiding and monoids: β and η form monoid-hom structures.

Русский

Существование моноидных гомоморфизмов для braiding и единиц.

LaTeX

$$$IsMonHom(β_{X,Y}.hom)$ and $IsMonHom(η)$$$

Lean4

instance {X Y : C} [MonObj X] [MonObj Y] : IsMonHom (β_ X Y).hom :=
  ⟨one_braiding X Y, mul_braiding X Y⟩

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

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

Разделы

Аффилиация

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