postcompIsoOfIso

Mathlib.CategoryTheory.Shift.SingleFunctors

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

Lean4

/-- The isomorphism `F.postcomp G ≅ F.postcomp G'` induced by an isomorphism `e : G ≅ G'`
which commutes with the shift. -/
@[simps!]
def postcompIsoOfIso {G G' : D ⥤ E} (e : G ≅ G') [G.CommShift A] [G'.CommShift A] [NatTrans.CommShift e.hom A] :
    F.postcomp G ≅ F.postcomp G' :=
  isoMk (fun a => isoWhiskerLeft (F.functor a) e)
    (fun n a a' ha' => by
      ext X
      simp [NatTrans.shift_app e.hom n])

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

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

Разделы

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

Аффилиация

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