Theorems · Theorem · category theory

CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : C) (m n : ℤ)
  (hmn :
    autoParam (m + n = 0) CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app._auto_1),
  (CategoryTheory.shiftFunctor Cᵒᵖ m).map
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X)) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app
        ((CategoryTheory.shiftFunctor Cᵒᵖ m).obj (Opposite.op X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Cᵒᵖ n).map
          ((CategoryTheory.shiftFunctor C n).map
              ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n hmn).hom.app (Opposite.op X)).unop).op)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor Cᵒᵖ n).map
            ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n hmn).inv.app
              (Opposite.op ((CategoryTheory.shiftFunctor C n).obj X))))
          ((CategoryTheory.shiftFunctorComm Cᵒᵖ n m).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj X)))))

Defined in

Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift