mul_counit

Mathlib.CategoryTheory.Monoidal.Bimon_

URI: https://scilib.ai/kg/mathlib#Bimon.mul_counit

English

Multiplication and counit satisfy the counit–multiplication compatibility in a braiding context.

Русский

Умножение и counit удовлетворяют совместимости counit-множителя в контексте braided.

LaTeX

$$$$ μ[M] \\circ ε[M] = (ε[M] \\otimes η[M]) \\circ (λ _)^{\\mathrm{hom}} $$$$

Lean4

@[reassoc]
theorem mul_counit (M : C) [BimonObj M] : μ[M] ≫ ε[M] = (ε[M] ⊗ₘ ε[M]) ≫ (λ_ _).hom := by simp

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

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

Разделы

Аффилиация

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