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 : C}
{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))
Instances For
theorem
CategoryTheory.ShiftedHom.opEquiv_symm_apply
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.HasShift C ℤ]
{X : C}
{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 : C}
{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 : C}
{Y : C}
{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 : C}
{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)
Instances For
theorem
CategoryTheory.ShiftedHom.opEquiv'_symm_apply
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.HasShift C ℤ]
{X : C}
{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 : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{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 : C}
{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 : C}
{Y : C}
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
{n : ℤ}
(x : CategoryTheory.ShiftedHom (Opposite.op Y) (Opposite.op X) n)
(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 : C}
{Y : C}
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
{n : ℤ}
{a : ℤ}
(x : Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op 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