Theorems · Theorem · category theory

CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y),
  CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X)
      ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f)

Defined in

Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift