Twisting a shift

Given a category C equipped with a shift by a monoid A, we introduce a structure t : TwistShiftData C A which consists of a collection of invertible elements in the center of the category C (typically, C will be preadditive, and these will be signs), which allow to introduce a type synonym category t.Category with identical shift functors as C but where the isomorphisms shiftFunctorAdd have been modified.

structure CategoryTheory.TwistShiftData (C : Type u) [Category.{v, u} C] (A : Type w) [AddMonoid A] [HasShift C A] : Type (max (max u v) w)

Given a category C equipped with a shift by a monoid A

• z (a b : A) : (CatCenter C)ˣ

  The invertible elements in the center of C which are used to modify the shiftFunctorAdd isomorphisms.

• z_zero_zero : self.z 0 0 = 1
• assoc (a b c : A) : self.z (a + b) c * self.z a b = self.z a (b + c) * self.z b c
• commShift (a b : A) : NatTrans.CommShift (↑(self.z a b)) A

@[simp]

theorem CategoryTheory.TwistShiftData.z_zero_right {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (a : A) : t.z a 0 = 1

@[simp]

theorem CategoryTheory.TwistShiftData.z_zero_left {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (b : A) : t.z 0 b = 1

@[simp]

theorem CategoryTheory.TwistShiftData.shift_z_app {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (a b c : A) (X : C) : (shiftFunctor C c).map ((↑(t.z a b)).app X) = (↑(t.z a b)).app ((shiftFunctor C c).obj X)

def CategoryTheory.TwistShiftData.Category {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] : TwistShiftData C A → Type u

Given t : TwistShiftData C A, this is a type synonym for the category C, which the same shift functors as C but where the shiftFunctorAdd isomorphisms have been modified using t.

instance CategoryTheory.TwistShiftData.instCategoryCategory {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) : Category.{v, u} t.Category

def CategoryTheory.TwistShiftData.shiftMkCore {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) : ShiftMkCore t.Category A

Given t : TwistShiftData C A, the shift on the category TwistShift t has the same shift functors as C, the same isomorphism shiftFunctorZero isomorphism, but the shiftFunctorAdd isomorphisms are modified using t.

instance CategoryTheory.TwistShiftData.hasShift {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) : HasShift t.Category A

noncomputable def CategoryTheory.TwistShiftData.shiftIso {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (m : A) : shiftFunctor t.Category m ≅ shiftFunctor C m

Given t : TwistShiftData C A, the shift functors on t.Category identify to the shift functors on C.

theorem CategoryTheory.TwistShiftData.shiftFunctor_map {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) {X Y : t.Category} (f : X ⟶ Y) (m : A) : (shiftFunctor t.Category m).map f = CategoryStruct.comp ((t.shiftIso m).hom.app X) (CategoryStruct.comp ((shiftFunctor C m).map f) ((t.shiftIso m).inv.app Y))

theorem CategoryTheory.TwistShiftData.shiftFunctorZero_hom_app {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (X : t.Category) : (shiftFunctorZero t.Category A).hom.app X = CategoryStruct.comp ((t.shiftIso 0).hom.app X) ((shiftFunctorZero C A).hom.app X)

theorem CategoryTheory.TwistShiftData.shiftFunctorZero_inv_app {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (X : t.Category) : (shiftFunctorZero t.Category A).inv.app X = CategoryStruct.comp ((shiftFunctorZero C A).inv.app X) ((t.shiftIso 0).inv.app X)

@[simp]

theorem CategoryTheory.TwistShiftData.shiftFunctorAdd'_hom_app {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (i j k : A) (h : i + j = k) (X : t.Category) : (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • CategoryStruct.comp ((t.shiftIso k).hom.app X) (CategoryStruct.comp ((shiftFunctorAdd' C i j k h).hom.app X) (CategoryStruct.comp ((shiftFunctor C j).map ((t.shiftIso i).inv.app X)) ((t.shiftIso j).inv.app ((shiftFunctor t.Category i).obj X))))

@[simp]

theorem CategoryTheory.TwistShiftData.shiftFunctorAdd'_inv_app {C : Type u} [Category.{v, u} C] {A : Type w} [AddMonoid A] [HasShift C A] (t : TwistShiftData C A) (i j k : A) (h : i + j = k) (X : t.Category) : (shiftFunctorAdd' t.Category i j k h).inv.app X = ↑(t.z i j)⁻¹ • CategoryStruct.comp ((t.shiftIso j).hom.app ((shiftFunctor t.Category i).obj X)) (CategoryStruct.comp ((shiftFunctor C j).map ((t.shiftIso i).hom.app X)) (CategoryStruct.comp ((shiftFunctorAdd' C i j k h).inv.app X) ((t.shiftIso k).inv.app X)))