multicospanIndexEnd

Mathlib.CategoryTheory.Limits.Shapes.End

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

Lean4

/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this is the multicospan index which shall be used
to define the end of `F`. -/
@[simps]
def multicospanIndexEnd : MulticospanIndex (multicospanShapeEnd J) C
    where
  left j := (F.obj (op j)).obj j
  right f := (F.obj (op f.left)).obj f.right
  fst f := (F.obj (op f.left)).map f.hom
  snd f := (F.map f.hom.op).app f.right

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

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

Разделы

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

Аффилиация

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