instIsMonHomHomLeftUnitor

Mathlib.CategoryTheory.Monoidal.Mon_

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

English

The left unitor morphism is a monoid homomorphism.

Русский

Левый унитор является моноидным гомоморфизмом.

LaTeX

$$$\\text{leftUnitor}(X): I⊗X\\to X \\quad\\Rightarrow\\quad \\text{MonHom}$$$

Lean4

instance : IsMonHom (λ_ X).hom :=
  ⟨one_leftUnitor, mul_leftUnitor⟩

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

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

Разделы

Аффилиация

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