bifunctorComp₂₃

Mathlib.CategoryTheory.Functor.Trifunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.bifunctorComp₂₃

Lean4

/-- Given two bifunctors `F : C₁ ⥤ C₂₃ ⥤ C₄` and `G₂₃ : C₂ ⥤ C₃ ⥤ C₄`, this is
the trifunctor `C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` obtained by composition. -/
@[simps]
def bifunctorComp₂₃ (F : C₁ ⥤ C₂₃ ⥤ C₄) (G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃) : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
    where
  obj X₁ := bifunctorComp₂₃Obj F G₂₃ X₁
  map {X₁ Y₁} φ := { app := fun X₂ => { app := fun X₃ => (F.map φ).app ((G₂₃.obj X₂).obj X₃) } }

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

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

Разделы

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

Аффилиация

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