shiftIso

Mathlib.CategoryTheory.Shift.InducedShiftSequence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.ShiftSequence.induced.shiftIso

Lean4

/-- The `shiftIso` field of the induced shift sequence. -/
noncomputable def shiftIso (n a a' : M) (ha' : n + a = a') : shiftFunctor D n ⋙ F' a ≅ F' a' := by
  exact
    ((whiskeringLeft C D A).obj L).preimageIso
      ((Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (L.commShiftIso n).symm _ ≪≫
          Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (e' a) ≪≫ G.shiftIso n a a' ha' ≪≫ (e' a').symm)

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

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

Разделы

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

Аффилиация

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