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.

If F : C ⥤ D is a functor between categories equipped with shifts by A, we define a type synonym OppositeShift.functor A F for F.op. When F has a CommShift structure by A, we define a CommShift structure by A on OppositeShift.functor A F. In this way, we can make this an instance and reserve F.op for the CommShift instance by the modified shift in the case of (pre)triangulated categories.

Similarly, if τ is a natural transformation between functors F,G : C ⥤ D, we define a type synonym for τ.op called OppositeShift.natTrans A τ : OppositeShift.functor A F ⟶ OppositeShift.functor A G. When τ has a CommShift structure by A (i.e. is compatible with CommShift structures on F and G), we define a CommShift structure by A on OppositeShift.natTrans A τ.

Finally, if we have an adjunction F ⊣ G (with G : D ⥤ C), we define a type synonym OppositeShift.adjunction A adj : OppositeShift.functor A G ⊣ OppositeShift.functor A F for adj.op, and we show that, if adj compatible with CommShift structures on F and G, then OppositeShift.adjunction A adj is also compatible with the pulled back CommShift structures.

Given a CommShift structure on a functor F, we define a CommShift structure on F.op (and vice versa). We also prove that, if an adjunction F ⊣ G is compatible with CommShift structures on F and G, then the opposite adjunction G.op ⊣ F.op is compatible with the opposite CommShift structures.

noncomputable def CategoryTheory.HasShift.mkShiftCoreOp (C : Type u_1) [Category.{u_3, u_1} C] (A : Type u_2) [AddMonoid A] [HasShift C A] : 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.

def CategoryTheory.OppositeShift (C : Type u_1) [Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [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.

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

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

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

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

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

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

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

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

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

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

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

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

The functor F.op, seen as a functor from OppositeShift C A to OppositeShift D A. (We will use this to carry a CommShift instance for the naive shifts on the opposite category. Then, in the pretriangulated case, we will be able to put a CommShift instance on F.op for the modified shifts and not deal with instance clashes.

def CategoryTheory.OppositeShift.natTrans {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] {F G : Functor C D} (τ : F ⟶ G) : functor A G ⟶ functor A F

The natural transformation τ, seen as a natural transformation from OppositeShift.functor F A to OppositeShift.functor G A..

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

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

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

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

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

@[simp]

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

instance CategoryTheory.NatTrans.commShift_op {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_4, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] {F G : Functor C D} [F.CommShift A] [G.CommShift A] (τ : F ⟶ G) [CommShift τ A] : CommShift (OppositeShift.natTrans A τ) A

def CategoryTheory.NatTrans.OppositeShift.natIsoId (C : Type u_1) [Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [HasShift C A] : Functor.id (OppositeShift C A) ≅ OppositeShift.functor A (Functor.id C)

The obvious isomorphism between the identity of OppositeShift C A and OppositeShift.functor (𝟙 C).

instance CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId {C : Type u_1} [Category.{u_4, u_1} C] (A : Type u_3) [AddMonoid A] [HasShift C A] : CommShift (OppositeShift.natIsoId C A).hom A

The natural isomorphism NatTrans.OppositeShift.natIsoId C A commutes with shifts.

def CategoryTheory.NatTrans.OppositeShift.natIsoComp {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] (F : Functor C D) {E : Type u_4} [Category.{u_7, u_4} E] [HasShift E A] (G : Functor D E) : OppositeShift.functor A (F.comp G) ≅ (OppositeShift.functor A F).comp (OppositeShift.functor A G)

The obvious isomorphism between OppositeShift.functor (F ⋙ G) and the composition of OppositeShift.functor F and OppositeShift.functor G.

instance CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp {C : Type u_1} {D : Type u_2} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] (F : Functor C D) {E : Type u_4} [Category.{u_7, u_4} E] [HasShift E A] (G : Functor D E) [F.CommShift A] [G.CommShift A] : CommShift (OppositeShift.natIsoComp A F G).hom A

def CategoryTheory.OppositeShift.adjunction {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) : functor A G ⊣ functor A F

The adjunction adj, seen as an adjunction between OppositeShift.functor G and OppositeShift.functor F.

theorem CategoryTheory.OppositeShift.adjunction_counit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) : (adjunction A adj).counit = CategoryStruct.comp (NatTrans.OppositeShift.natIsoComp A F G).inv (CategoryStruct.comp (natTrans A adj.unit) (NatTrans.OppositeShift.natIsoId C A).inv)

theorem CategoryTheory.OppositeShift.adjunction_unit {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) : (adjunction A adj).unit = CategoryStruct.comp (NatTrans.OppositeShift.natIsoId D A).hom (CategoryStruct.comp (natTrans A adj.counit) (NatTrans.OppositeShift.natIsoComp A G F).hom)

instance CategoryTheory.Adjunction.commShift_op {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] (A : Type u_3) [AddMonoid A] [HasShift C A] [HasShift D A] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [F.CommShift A] [G.CommShift A] [adj.CommShift A] : (OppositeShift.adjunction A adj).CommShift A

If an adjunction F ⊣ G is compatible with CommShift structures on F and G, then the opposite adjunction OppositeShift.adjunction adj is compatible with the opposite CommShift structures.