The (naive) shift on the opposite category

If C is a category equipped with a shift by a monoid A, the opposite category can be equipped with a shift such that the shift functor by n is (shiftFunctor C n).op. This is the "naive" opposite shift, which we shall set on a category OppositeShift C A, which is a type synonym for Cᵒᵖ.

However, for the application to (pre)triangulated categories, we would like to define the shift on Cᵒᵖ so that shiftFunctor Cᵒᵖ n for n : ℤ identifies to (shiftFunctor C (-n)).op rather than (shiftFunctor C n).op. Then, the construction of the shift on Cᵒᵖ shall combine the shift on OppositeShift C A and another construction of the "pullback" of a shift by a monoid morphism like n ↦ -n.

noncomputable def CategoryTheory.HasShift.mkShiftCoreOp (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] : CategoryTheory.ShiftMkCore Cᵒᵖ A

Construction of the naive shift on the opposite category of a category C: the shiftfunctor by n is (shiftFunctor C n).op.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.OppositeShift (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [CategoryTheory.HasShift C A] : Type u_1

The category OppositeShift C A is the opposite category Cᵒᵖ equipped with the naive shift: shiftFunctor (OppositeShift C A) n is (shiftFunctor C n).op.

Equations

• CategoryTheory.OppositeShift C A = Cᵒᵖ

instance CategoryTheory.instCategoryOppositeShift (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] : CategoryTheory.Category.{u_3, u_1} (CategoryTheory.OppositeShift C A)

Equations

• CategoryTheory.instCategoryOppositeShift C A = id inferInstance

noncomputable instance CategoryTheory.instHasShiftOppositeShift (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] : CategoryTheory.HasShift (CategoryTheory.OppositeShift C A) A

Equations

• CategoryTheory.instHasShiftOppositeShift C A = CategoryTheory.hasShiftMk Cᵒᵖ A (CategoryTheory.HasShift.mkShiftCoreOp C A)

instance CategoryTheory.instHasZeroObjectOppositeShift (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.OppositeShift C A)

instance CategoryTheory.instPreadditiveOppositeShift (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] : CategoryTheory.Preadditive (CategoryTheory.OppositeShift C A)

Equations

• CategoryTheory.instPreadditiveOppositeShift C A = id inferInstance

instance CategoryTheory.instAdditiveOppositeShiftShiftFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.Preadditive C] (n : A) [(CategoryTheory.shiftFunctor C n).Additive] : (CategoryTheory.shiftFunctor (CategoryTheory.OppositeShift C A) n).Additive

theorem CategoryTheory.oppositeShiftFunctorZero_inv_app (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) : (CategoryTheory.shiftFunctorZero (CategoryTheory.OppositeShift C A) A).inv.app X = ((CategoryTheory.shiftFunctorZero C A).hom.app (Opposite.unop X)).op

theorem CategoryTheory.oppositeShiftFunctorZero_hom_app (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) : (CategoryTheory.shiftFunctorZero (CategoryTheory.OppositeShift C A) A).hom.app X = ((CategoryTheory.shiftFunctorZero C A).inv.app (Opposite.unop X)).op

theorem CategoryTheory.oppositeShiftFunctorAdd_inv_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b : A) : (CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).inv.app X = ((CategoryTheory.shiftFunctorAdd C a b).hom.app (Opposite.unop X)).op

theorem CategoryTheory.oppositeShiftFunctorAdd_hom_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b : A) : (CategoryTheory.shiftFunctorAdd (CategoryTheory.OppositeShift C A) a b).hom.app X = ((CategoryTheory.shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op

theorem CategoryTheory.oppositeShiftFunctorAdd'_inv_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b c : A) (h : a + b = c) : (CategoryTheory.shiftFunctorAdd' (CategoryTheory.OppositeShift C A) a b c h).inv.app X = ((CategoryTheory.shiftFunctorAdd' C a b c h).hom.app (Opposite.unop X)).op

theorem CategoryTheory.oppositeShiftFunctorAdd'_hom_app {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {A : Type u_2} [AddMonoid A] [CategoryTheory.HasShift C A] (X : CategoryTheory.OppositeShift C A) (a b c : A) (h : a + b = c) : (CategoryTheory.shiftFunctorAdd' (CategoryTheory.OppositeShift C A) a b c h).hom.app X = ((CategoryTheory.shiftFunctorAdd' C a b c h).inv.app (Opposite.unop X)).op

noncomputable def CategoryTheory.Functor.commShiftOp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_3) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] : F.op.CommShift A

Given a CommShift structure on F, this is the corresponding CommShift structure on F.op (for the naive shifts on the opposite categories).

Equations

• F.commShiftOp A = { iso := fun (a : A) => (CategoryTheory.NatIso.op (F.commShiftIso a)).symm, zero := ⋯, add := ⋯ }

@[simp]

theorem CategoryTheory.Functor.commShiftOp_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_3) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (a : A) : CategoryTheory.Functor.CommShift.iso a = (CategoryTheory.NatIso.op (F.commShiftIso a)).symm

noncomputable def CategoryTheory.Functor.commShiftUnop {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_3) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.op.CommShift A] : F.CommShift A

Given a CommShift structure on F.op (for the naive shifts on the opposite categories), this is the corresponding CommShift structure on F.

Equations

• F.commShiftUnop A = { iso := fun (a : A) => CategoryTheory.NatIso.removeOp (F.op.commShiftIso a).symm, zero := ⋯, add := ⋯ }

@[simp]

theorem CategoryTheory.Functor.commShiftUnop_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_3) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.op.CommShift A] (a : A) : CategoryTheory.Functor.CommShift.iso a = CategoryTheory.NatIso.removeOp (F.op.commShiftIso a).symm