comul_counit

Mathlib.CategoryTheory.Bicategory.Monad.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.Comonad.comul_counit

English

Comonad comultiplication-counit law: Δ ≫ t ◁ ε = ρ_t^{-1}.

Русский

Закон комонaд comul counit: Δ ≫ t ◁ ε = ρ_t^{-1}.

LaTeX

$$$Δ \\;≫\\; t \\triangleleft ε = (ρ_ t)^{-1}$$$

Lean4

@[reassoc (attr := simp)]
theorem comul_counit : Δ ≫ t ◁ ε = (ρ_ t).inv :=
  ComonObj.comul_counit t

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

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

Разделы

Аффилиация

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