iso

Mathlib.CategoryTheory.Shift.Localization

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.commShiftOfLocalization.iso

Lean4

/-- Auxiliary definition for `Functor.commShiftOfLocalization`. -/
noncomputable def iso (a : A) : shiftFunctor D a ⋙ F' ≅ F' ⋙ shiftFunctor E a :=
  Localization.liftNatIso L W (L ⋙ shiftFunctor D a ⋙ F') (L ⋙ F' ⋙ shiftFunctor E a) _ _
    ((Functor.associator _ _ _).symm ≪≫
      isoWhiskerRight (L.commShiftIso a).symm F' ≪≫
        Functor.associator _ _ _ ≪≫
          isoWhiskerLeft _ (Lifting.iso L W F F') ≪≫
            F.commShiftIso a ≪≫ isoWhiskerRight (Lifting.iso L W F F').symm _ ≪≫ Functor.associator _ _ _)

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

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

Разделы

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

Аффилиация

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