Shifted morphisms in the opposite category

If C is a category equipped with a shift by ℤ, X and Y are objects of C, and n : ℤ, we define a bijection ShiftedHom.opEquiv : ShiftedHom X Y n ≃ ShiftedHom (Opposite.op Y) (Opposite.op X) n. We also introduce ShiftedHom.opEquiv' which produces a bijection ShiftedHom X Y a' ≃ (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧) when n + a = a'. The compatibilities that are obtained shall be used in order to study the homological functor preadditiveYoneda.obj B : Cᵒᵖ ⥤ Type _ when B is an object in a pretriangulated category C.

noncomputable def CategoryTheory.ShiftedHom.opEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} (n : ℤ) : CategoryTheory.ShiftedHom X Y n ≃ CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) n

The bijection ShiftedHom X Y n ≃ ShiftedHom (Opposite.op Y) (Opposite.op X) n when n : ℤ, and X and Y are objects of a category equipped with a shift by ℤ.

Equations

• CategoryTheory.ShiftedHom.opEquiv n = Quiver.Hom.opEquiv.trans ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).symm.toAdjunction.homEquiv (Opposite.op Y) (Opposite.op X))

theorem CategoryTheory.ShiftedHom.opEquiv_symm_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} {n : ℤ} (f : CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) n) : (CategoryTheory.ShiftedHom.opEquiv n).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ((CategoryTheory.shiftFunctor C n).map (Quiver.Hom.unop f))

theorem CategoryTheory.ShiftedHom.opEquiv_symm_apply_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} {a : ℤ} (f : CategoryTheory.ShiftedHom (Opposite.op X) (Opposite.op Y) a) {b : ℤ} {Z : C} (z : CategoryTheory.ShiftedHom X Z b) {c : ℤ} (h : b + a = c) : ((CategoryTheory.ShiftedHom.opEquiv a).symm f).comp z h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ShiftedHom.opEquiv a).symm (CategoryTheory.CategoryStruct.comp (Quiver.Hom.op z) f)) ((CategoryTheory.shiftFunctorAdd' C b a c h).inv.app Z)

theorem CategoryTheory.ShiftedHom.opEquiv_symm_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y Z : C} {a b : ℤ} (f : CategoryTheory.ShiftedHom (Opposite.op Z) (Opposite.op Y) a) (g : CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) b) {c : ℤ} (h : b + a = c) : (CategoryTheory.ShiftedHom.opEquiv c).symm (f.comp g h) = ((CategoryTheory.ShiftedHom.opEquiv b).symm g).comp ((CategoryTheory.ShiftedHom.opEquiv a).symm f) ⋯

noncomputable def CategoryTheory.ShiftedHom.opEquiv' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} (n a a' : ℤ) (h : n + a = a') : CategoryTheory.ShiftedHom X Y a' ≃ (Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X))

The bijection ShiftedHom X Y a' ≃ (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧) when integers n, a and a' satisfy n + a = a', and X and Y are objects of a category equipped with a shift by ℤ.

Equations

• CategoryTheory.ShiftedHom.opEquiv' n a a' h = ((CategoryTheory.shiftFunctorAdd' C a n a' ⋯).symm.app Y).homToEquiv.symm.trans (CategoryTheory.ShiftedHom.opEquiv n)

theorem CategoryTheory.ShiftedHom.opEquiv'_symm_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} {n a : ℤ} (f : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) (a' : ℤ) (h : n + a = a') : (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ShiftedHom.opEquiv n).symm f) ((CategoryTheory.shiftFunctorAdd' C a n a' ⋯).inv.app Y)

theorem CategoryTheory.ShiftedHom.opEquiv'_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} {a' : ℤ} (f : CategoryTheory.ShiftedHom X Y a') (n a : ℤ) (h : n + a = a') : (CategoryTheory.ShiftedHom.opEquiv' n a a' h) f = (CategoryTheory.ShiftedHom.opEquiv n) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorAdd' C a n a' ⋯).hom.app Y))

theorem CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y Z : C} {n m : ℤ} (f : CategoryTheory.ShiftedHom X Y n) (g : CategoryTheory.ShiftedHom Y Z m) (q : ℤ) (hq : n + m = q) : (CategoryTheory.ShiftedHom.opEquiv' n m q hq).symm (CategoryTheory.CategoryStruct.comp (Quiver.Hom.op g) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op Y)) ((CategoryTheory.shiftFunctor Cᵒᵖ n).map (Quiver.Hom.op f)))) = f.comp g ⋯

theorem CategoryTheory.ShiftedHom.opEquiv'_symm_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : Y ⟶ X) {n a : ℤ} (x : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Z) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) (a' : ℤ) (h : n + a = a') : (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm (CategoryTheory.CategoryStruct.comp x ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f.op)) = CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm x)

theorem CategoryTheory.ShiftedHom.opEquiv'_zero_add_symm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} (a : ℤ) (f : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ 0).obj (Opposite.op X)) : (CategoryTheory.ShiftedHom.opEquiv' 0 a a ⋯).symm f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).hom.app (Opposite.op X)).unop f.unop

theorem CategoryTheory.ShiftedHom.opEquiv'_add_symm {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} (n m a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'') (x : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)) : (CategoryTheory.ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm x = (CategoryTheory.ShiftedHom.opEquiv' m a' a'' ha'').symm (Quiver.Hom.op ((CategoryTheory.ShiftedHom.opEquiv' n a a' ha').symm (CategoryTheory.CategoryStruct.comp x ((CategoryTheory.shiftFunctorAdd Cᵒᵖ m n).hom.app (Opposite.op X)))))

@[simp]

theorem CategoryTheory.ShiftedHom.opEquiv_symm_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] {n : ℤ} (x y : CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) n) : (CategoryTheory.ShiftedHom.opEquiv n).symm (x + y) = (CategoryTheory.ShiftedHom.opEquiv n).symm x + (CategoryTheory.ShiftedHom.opEquiv n).symm y

@[simp]

theorem CategoryTheory.ShiftedHom.opEquiv'_symm_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {X Y : C} [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] {n a : ℤ} (x y : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) (a' : ℤ) (h : n + a = a') : (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm (x + y) = (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm x + (CategoryTheory.ShiftedHom.opEquiv' n a a' h).symm y