Theorems · Definition · category theory

CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {n : ℤ} →
        {X Y : Cᵒᵖ} →
          (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) ≃
            (X ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj Y)

Given objects X and Y in Cᵒᵖ, this is the bijection (op (X.unop⟦n⟧) ⟶ Y) ≃ (X ⟶ Y⟦n⟧) for any n : ℤ.

Defined in

Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.HasShift