instTensorUnit

Mathlib.CategoryTheory.Monoidal.Comon_

URI: https://scilib.ai/kg/mathlib#ComonObj.instTensorUnit

Lean4

/-- The canonical comonoid structure on the monoidal unit.
This is not a global instance to avoid conflicts with other comonoid structures. -/
@[simps]
def instTensorUnit (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] : ComonObj (𝟙_ C)
    where
  counit := 𝟙 _
  comul := (λ_ _).inv
  counit_comul := by simp
  comul_counit := by monoidal_coherence
  comul_assoc := by monoidal_coherence

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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