Theorems · Theorem · category theory

CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app_assoc

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app._auto_1) {Z : C}
  (h : (CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.unopUnop C).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (CategoryTheory.unopUnop C) n).hom.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop h)

Defined in

Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift