coyoneda

Mathlib.Algebra.Category.MonCat.Yoneda

URI: https://scilib.ai/kg/mathlib#CommMonCat.coyoneda

Lean4

/-- The `CommMonCat`-valued coyoneda embedding. -/
@[to_additive (attr := simps) /-- The `AddCommMonCat`-valued coyoneda embedding. -/
    ]
def coyoneda : CommMonCatᵒᵖ ⥤ CommMonCat ⥤ CommMonCat
    where
  obj M := { obj N := of (M.unop →* N), map f := ofHom (.compHom f.hom) }
  map f := { app N := ofHom (.compHom' f.unop.hom) }

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

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

Разделы

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

Аффилиация

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