Theorems · Theorem · category theory

CategoryTheory.Pretriangulated.shiftFunctor_op_map

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {K L : Cᵒᵖ}
  (φ : K ⟶ L) (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.shiftFunctor_op_map._auto_1),
  (CategoryTheory.shiftFunctor Cᵒᵖ n).map φ =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app K)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m).map φ.unop).op
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app L))

Defined in

Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift