MonOpOpToComonObjComon

Mathlib.CategoryTheory.Monoidal.Comon_

URI: https://scilib.ai/kg/mathlib#Comon.MonOpOpToComonObjComon

Lean4

/-- Auxiliary definition for `MonOpOpToComonObj`. -/
abbrev MonOpOpToComonObjComon (A : Mon Cᵒᵖ) : ComonObj (unop A.X)
    where
  counit := η[A.X].unop
  comul := μ[A.X].unop
  counit_comul := by rw [← unop_whiskerRight, ← unop_comp, MonObj.one_mul]; rfl
  comul_counit := by rw [← unop_whiskerLeft, ← unop_comp, MonObj.mul_one]; rfl
  comul_assoc :=
    by
    rw [← unop_whiskerRight, ← unop_whiskerLeft, ← unop_comp_assoc, ← unop_comp, MonObj.mul_assoc_flip]
    rfl

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

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

Разделы

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

Аффилиация

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