unitors_equal

Mathlib.CategoryTheory.Monoidal.CoherenceLemmas

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.unitors_equal

English

In a monoidal category, the left and right unitors coincide on the tensor unit 𝟙_C.

Русский

В моноидальной категории левые и правые униторы совпадают на единичном объекте тензора.

LaTeX

$$$(\\lambda_{\\mathbf{1}_C}).hom = (\\rho_{\\mathbf{1}_C}).hom$$$

Lean4

theorem unitors_equal : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by monoidal_coherence

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

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

Разделы

Аффилиация

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