Theorems · Theorem · category theory

CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_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_hom_app_eq._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C p).unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C n).map
            ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).unitIso.hom.app
                ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)).unop).op
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop
                ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).functor.obj
                  ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)))).op
          ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op))

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