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} [Category.{u_2, u_1} C] [HasShift C ℤ] {X Y : C} (n : ℤ) : ShiftedHom X Y n ≃ 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} [Category.{u_2, u_1} C] [HasShift C ℤ] {X Y : C} {n : ℤ} (f : ShiftedHom (Opposite.op Y) (Opposite.op X) n) : (opEquiv n).symm f = CategoryStruct.comp ((Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ((shiftFunctor C n).map (Quiver.Hom.unop f))

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

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

noncomputable def CategoryTheory.ShiftedHom.opEquiv' {C : Type u_1} [Category.{u_2, u_1} C] [HasShift C ℤ] {X Y : C} (n a a' : ℤ) (h : n + a = a') : ShiftedHom X Y a' ≃ (Opposite.op ((shiftFunctor C a).obj Y) ⟶ (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} [Category.{u_2, u_1} C] [HasShift C ℤ] {X Y : C} {n a : ℤ} (f : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)) (a' : ℤ) (h : n + a = a') : (opEquiv' n a a' h).symm f = CategoryStruct.comp ((opEquiv n).symm f) ((shiftFunctorAdd' C a n a' ⋯).inv.app Y)

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

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

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

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

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

@[simp]

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

@[simp]

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