iso

Mathlib.CategoryTheory.Shift.Quotient

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Quotient.LiftCommShift.iso

Lean4

/-- Auxiliary definition for `Quotient.liftCommShift`. -/
noncomputable def iso (a : A) : shiftFunctor (Quotient r) a ⋙ lift r F hF ≅ lift r F hF ⋙ shiftFunctor D a :=
  natIsoLift r
    ((Functor.associator _ _ _).symm ≪≫
      Functor.isoWhiskerRight ((functor r).commShiftIso a).symm _ ≪≫
        Functor.associator _ _ _ ≪≫
          Functor.isoWhiskerLeft _ (lift.isLift r F hF) ≪≫
            F.commShiftIso a ≪≫ Functor.isoWhiskerRight (lift.isLift r F hF).symm _ ≪≫ Functor.associator _ _ _)

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

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

Разделы

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

Аффилиация

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