CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality

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

This theorem states that for any category `C` that has a shift (`CategoryTheory.HasShift C ℤ`), and for any integer `n`, the mapping of the composed morphisms using the operation of shifting functor `CategoryTheory.shiftFunctor` in the opposite category `Cᵒᵖ` is equal to the composition of the inverse of the natural transformation of the equivalence functor (`CategoryTheory.Pretriangulated.opShiftFunctorEquivalence`) and the morphism `f`. This property holds for all objects `X` and `Y` in the opposite category `Cᵒᵖ` and all morphisms `f` from `X` to `Y`. The statement captures a naturality condition under the shift functor in the context of pretriangulated categories.

More concisely: For any pretriangulated category `C` with shift functor, and for all objects `X` and `Y` and morphism `f` in `Cᵒᵖ`, the shift of their composition `(CategoryTheory.shiftFunctor C (-n)).(CategoryTheory.opLim (CategoryTheory.opShiftFunctorEquivalence C).inv ∘ f)` is equal to the composition of `f` and the shift of the identity `(CategoryTheory.shiftFunctor C (-n)) (idY)`.