postcompPostcompIso

Mathlib.CategoryTheory.Shift.SingleFunctors

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SingleFunctors.postcompPostcompIso

Lean4

/-- The canonical isomorphism `(F.postcomp G).postcomp G' ≅ F.postcomp (G ⋙ G')`. -/
@[simps!]
def postcompPostcompIso (G : D ⥤ E) (G' : E ⥤ E') [G.CommShift A] [G'.CommShift A] :
    (F.postcomp G).postcomp G' ≅ F.postcomp (G ⋙ G') :=
  isoMk (fun _ => Functor.associator _ _ _)
    (fun n a a' ha' => by
      ext X
      simp [Functor.commShiftIso_comp_inv_app])

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

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

Разделы

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

Аффилиация

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