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.

source
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.
Instances For
    source
    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
    Instances For
      source
      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
      source
      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
      source
      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)
      Equations
      • ⋯ = ⋯
      source
      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
      source
      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
      Equations
      • ⋯ = ⋯
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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