bifunctorComp₁₂Obj

Mathlib.CategoryTheory.Functor.Trifunctor

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

Lean4

/-- Auxiliary definition for `bifunctorComp₁₂`. -/
@[simps]
def bifunctorComp₁₂Obj (F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂) (G : C₁₂ ⥤ C₃ ⥤ C₄) (X₁ : C₁) : C₂ ⥤ C₃ ⥤ C₄
    where
  obj
    X₂ :=
    { obj := fun X₃ => (G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃
      map := fun {_ _} φ => (G.obj ((F₁₂.obj X₁).obj X₂)).map φ }
  map {X₂ Y₂} φ := { app := fun X₃ => (G.map ((F₁₂.obj X₁).map φ)).app X₃ }

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

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

Разделы

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

Аффилиация

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