multispanIndexCoend

Mathlib.CategoryTheory.Limits.Shapes.End

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.multispanIndexCoend

Lean4

/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the multispan used to define the coend
of `F`. -/
@[simps]
def multispanIndexCoend : MultispanIndex (multispanShapeCoend J) C
    where
  left f := (F.obj (op f.right)).obj f.left
  right j := (F.obj (op j)).obj j
  fst f := (F.map f.hom.op).app f.left
  snd f := (F.obj (op f.right)).map f.hom

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

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

Разделы

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

Аффилиация

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