Theorems · Theorem · category theory

CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (m n p : ℤ)
  (h : autoParam (m + n = p) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C p).unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctorAdd' C m n p h).inv.app
            (Opposite.unop (((CategoryTheory.shiftFunctor Cᵒᵖ n).comp (CategoryTheory.shiftFunctor Cᵒᵖ m)).obj X))).op
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C n).map
              ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).unitIso.inv.app
                  ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)).unop).op
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)))

Defined in

Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Cited by

2 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift