# Documentation

Mathlib.CategoryTheory.Shift.Opposite

# 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) [] (A : Type u_2) [] [] :

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.
Instances For
def CategoryTheory.OppositeShift (C : Type u_1) [] (A : Type u_3) [] [] :
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
Instances For
instance CategoryTheory.instCategoryOppositeShift (C : Type u_1) [] (A : Type u_2) [] [] :
Equations
• = id inferInstance
noncomputable instance CategoryTheory.instHasShiftOppositeShiftInstCategoryOppositeShift (C : Type u_1) [] (A : Type u_2) [] [] :
Equations
Equations
Equations
• = id inferInstance
Equations
theorem CategoryTheory.oppositeShiftFunctorZero_inv_app (C : Type u_1) [] (A : Type u_2) [] [] (X : ) :
.inv.app X = (.hom.app X.unop).op
theorem CategoryTheory.oppositeShiftFunctorZero_hom_app (C : Type u_1) [] (A : Type u_2) [] [] (X : ) :
.hom.app X = (.inv.app X.unop).op
theorem CategoryTheory.oppositeShiftFunctorAdd_inv_app {C : Type u_1} [] {A : Type u_2} [] [] (X : ) (a : A) (b : A) :
.inv.app X = (().hom.app X.unop).op
theorem CategoryTheory.oppositeShiftFunctorAdd_hom_app {C : Type u_1} [] {A : Type u_2} [] [] (X : ) (a : A) (b : A) :
.hom.app X = (().inv.app X.unop).op
theorem CategoryTheory.oppositeShiftFunctorAdd'_inv_app {C : Type u_1} [] {A : Type u_2} [] [] (X : ) (a : A) (b : A) (c : A) (h : a + b = c) :
().inv.app X = (().hom.app X.unop).op
theorem CategoryTheory.oppositeShiftFunctorAdd'_hom_app {C : Type u_1} [] {A : Type u_2} [] [] (X : ) (a : A) (b : A) (c : A) (h : a + b = c) :
().hom.app X = (().inv.app X.unop).op