Commutation with shifts of functors in two variables

We introduce a typeclass Functor.CommShift₂Int for a bifunctor G : C₁ ⥤ C₂ ⥤ D (with D a preadditive category) as the two variable analogue of Functor.CommShift. We require that G commutes with the shifts in both variables and that the two ways to identify (G.obj (X₁⟦p⟧)).obj (X₂⟦q⟧) to ((G.obj X₁).obj X₂)⟦p + q⟧ differ by the sign (-1) ^ (p + q).

This is implemented using a structure Functor.CommShift₂ which does not depend on the preadditive structure on D: instead of signs, elements in (CatCenter D)ˣ are used. These elements are part of a CommShift₂Setup structure which extends a TwistShiftData structure (see the file Mathlib.CategoryTheory.Shift.Twist).

TODO (@joelriou)

• Show that G : C₁ ⥤ C₂ ⥤ D satisfies Functor.CommShift₂Int iff the uncurried functor C₁ × C₂ ⥤ D commutes with the shift by ℤ × ℤ, where C₁ × C₂ is equipped with the obvious product shift, and D is equipped with the twisted shift.

structure CategoryTheory.CommShift₂Setup (D : Type u_5) [Category.{v_5, u_5} D] (M : Type u_6) [AddCommMonoid M] [HasShift D M] extends CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M)) (M × M) : Type (max (max u_5 u_6) v_5)

Given a category D equipped with a shift by an additive monoid M, this structure CommShift₂Setup D M allows to define what it means for a bifunctor C₁ ⥤ C₂ ⥤ D to commute with shifts by M with respect to both variables. This structure consists of a TwistShiftData for the shift by M × M on D obtained by pulling back the addition map M × M →+ M, with two axioms z_zero₁ and z_zero₂. We also require an additional data of ε m n : (CatCenter D)ˣ for m and n: even though this is determined by the z field of TwistShiftData, we make it a separate field so as to have control on its definitional properties.

• z (a b : M × M) : (CatCenter (PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M)))ˣ
• z_zero_zero : self.z 0 0 = 1
• assoc (a b c : M × M) : self.z (a + b) c * self.z a b = self.z a (b + c) * self.z b c
• commShift (a b : M × M) : NatTrans.CommShift (↑(self.z a b)) (M × M)
• z_zero₁ (m₁ m₂ : M) : self.z (0, m₁) (0, m₂) = 1
• z_zero₂ (m₁ m₂ : M) : self.z (m₁, 0) (m₂, 0) = 1
• ε (m n : M) : (CatCenter D)ˣ

  The invertible elements in the center of D that are equal to (z (0, n) (m, 0))⁻¹ * z (m, 0) (0, n).

• hε (m n : M) : self.ε m n = (self.z (0, n) (m, 0))⁻¹ * self.z (m, 0) (0, n)

noncomputable def CategoryTheory.CommShift₂Setup.int {D : Type u_5} [Category.{v_5, u_5} D] [Preadditive D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] : CommShift₂Setup D ℤ

The standard setup for the commutation of bifunctors with shifts by ℤ.

Equations

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

@[simp]

theorem CategoryTheory.CommShift₂Setup.int_z {D : Type u_5} [Category.{v_5, u_5} D] [Preadditive D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] (m n : ℤ × ℤ) : int.z m n = (-1) ^ (m.1 * n.2)

@[simp]

theorem CategoryTheory.CommShift₂Setup.int_ε {D : Type u_5} [Category.{v_5, u_5} D] [Preadditive D] [HasShift D ℤ] [∀ (n : ℤ), (shiftFunctor D n).Additive] (p q : ℤ) : int.ε p q = (-1) ^ (p * q)

class CategoryTheory.Functor.CommShift₂ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_3, u_3} C₂] [Category.{v_5, u_5} D] {M : Type u_6} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₂ M] [HasShift D M] (G : Functor C₁ (Functor C₂ D)) (h : CommShift₂Setup D M) : Type (max (max (max u_1 u_3) u_6) v_5)

A bifunctor G : C₁ ⥤ C₂ ⥤ D commutes with the shifts by M if all functors G.obj X₁ and G.flip X₂ are equipped with Functor.CommShift structures, in a way that is natural in X₁ and X₂, and that these isomorphisms commute up to the multiplication with an element in (CatCenter D)ˣ which is determined by a CommShift₂Setup D M structure. (In most cases, one should use the abbreviation CommShift₂Int.)

• commShiftObj (X₁ : C₁) : (G.obj X₁).CommShift M
• commShift_map {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) : NatTrans.CommShift (G.map f) M
• commShiftFlipObj (X₂ : C₂) : (G.flip.obj X₂).CommShift M
• commShift_flip_map {X₂ Y₂ : C₂} (g : X₂ ⟶ Y₂) : NatTrans.CommShift (G.flip.map g) M
• comm (X₁ : C₁) (X₂ : C₂) (m n : M) : CategoryStruct.comp ((commShiftIso (G.obj ((shiftFunctor C₁ m).obj X₁)) n).hom.app X₂) ((shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app X₁)) = CategoryStruct.comp ((commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app X₁) (CategoryStruct.comp ((shiftFunctor D m).map ((commShiftIso (G.obj X₁) n).hom.app X₂)) (CategoryStruct.comp (shiftComm ((G.obj X₁).obj X₂) m n).inv ((↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj X₁).obj X₂))))))

theorem CategoryTheory.Functor.commShift₂_comm {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst✝ : Category.{v_1, u_1} C₁} {inst✝¹ : Category.{v_3, u_3} C₂} {inst✝² : Category.{v_5, u_5} D} {M : Type u_6} {inst✝³ : AddCommMonoid M} {inst✝⁴ : HasShift C₁ M} {inst✝⁵ : HasShift C₂ M} {inst✝⁶ : HasShift D M} (G : Functor C₁ (Functor C₂ D)) (h : CommShift₂Setup D M) [self : G.CommShift₂ h] (X₁ : C₁) (X₂ : C₂) (m n : M) : CategoryStruct.comp ((commShiftIso (G.obj ((shiftFunctor C₁ m).obj X₁)) n).hom.app X₂) ((shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app X₁)) = CategoryStruct.comp ((commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app X₁) (CategoryStruct.comp ((shiftFunctor D m).map ((commShiftIso (G.obj X₁) n).hom.app X₂)) (CategoryStruct.comp (shiftComm ((G.obj X₁).obj X₂) m n).inv ((↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj X₁).obj X₂))))))

This alias for Functor.CommShift₂.comm allows to use the dot notation.

theorem CategoryTheory.Functor.commShift₂_comm_assoc {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} {inst✝ : Category.{v_1, u_1} C₁} {inst✝¹ : Category.{v_3, u_3} C₂} {inst✝² : Category.{v_5, u_5} D} {M : Type u_6} {inst✝³ : AddCommMonoid M} {inst✝⁴ : HasShift C₁ M} {inst✝⁵ : HasShift C₂ M} {inst✝⁶ : HasShift D M} (G : Functor C₁ (Functor C₂ D)) (h : CommShift₂Setup D M) [self : G.CommShift₂ h] (X₁ : C₁) (X₂ : C₂) (m n : M) {Z : D} (h✝ : (shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.flip.obj X₂).obj X₁)) ⟶ Z) : CategoryStruct.comp ((commShiftIso (G.obj ((shiftFunctor C₁ m).obj X₁)) n).hom.app X₂) (CategoryStruct.comp ((shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app X₁)) h✝) = CategoryStruct.comp ((commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app X₁) (CategoryStruct.comp ((shiftFunctor D m).map ((commShiftIso (G.obj X₁) n).hom.app X₂)) (CategoryStruct.comp (shiftComm ((G.obj X₁).obj X₂) m n).inv (CategoryStruct.comp ((↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj X₁).obj X₂)))) h✝)))

This alias for Functor.CommShift₂.comm allows to use the dot notation.

@[reducible, inline]

abbrev CategoryTheory.Functor.CommShift₂Int {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_3, u_3} C₂] [Category.{v_5, u_5} D] [HasShift C₁ ℤ] [HasShift C₂ ℤ] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] (G : Functor C₁ (Functor C₂ D)) : Type (max (max u_1 u_3) v_5)

A bifunctor G : C₁ ⥤ C₂ ⥤ D commutes with the shifts by ℤ if all functors G.obj X₁ and G.flip X₂ are equipped with Functor.CommShift structures, in a way that is natural in X₁ and X₂, and that these isomorphisms for the shift by p on the first variable and the shift by q on the second variable commute up to the sign (-1) ^ (p * q).

Equations

• G.CommShift₂Int = G.CommShift₂ CategoryTheory.CommShift₂Setup.int

instance CategoryTheory.Functor.CommShift₂.precomp₁ {C₁ : Type u_1} {C₁' : Type u_2} {C₂ : Type u_3} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₁'] [Category.{v_3, u_3} C₂] [Category.{v_5, u_5} D] {M : Type u_6} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₁' M] [HasShift C₂ M] [HasShift D M] (F : Functor C₁' C₁) [F.CommShift M] (G : Functor C₁ (Functor C₂ D)) (h : CommShift₂Setup D M) [G.CommShift₂ h] : (F.comp G).CommShift₂ h

Equations

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

instance CategoryTheory.Functor.CommShift₂.precomp₂ {C₁ : Type u_1} {C₂ : Type u_3} {C₂' : Type u_4} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_3, u_3} C₂] [Category.{v_4, u_4} C₂'] [Category.{v_5, u_5} D] {M : Type u_6} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₂' M] [HasShift C₂ M] [HasShift D M] (F : Functor C₂' C₂) [F.CommShift M] (G : Functor C₁ (Functor C₂ D)) (h : CommShift₂Setup D M) [G.CommShift₂ h] : (G.comp ((whiskeringLeft C₂' C₂ D).obj F)).CommShift₂ h

Equations

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

class CategoryTheory.NatTrans.CommShift₂ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_3, u_3} C₂] [Category.{v_5, u_5} D] {M : Type u_6} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₂ M] [HasShift D M] {G₁ G₂ : Functor C₁ (Functor C₂ D)} (τ : G₁ ⟶ G₂) (h : CommShift₂Setup D M) [G₁.CommShift₂ h] [G₂.CommShift₂ h] : Prop

If τ : G₁ ⟶ G₂ is a natural transformation between two bifunctors which commute shifts on both variables, this typeclass asserts a compatibility of τ with these shifts.

• commShift_app (X₁ : C₁) : CommShift (τ.app X₁) M
• commShift_flipApp (X₂ : C₂) : CommShift (flipApp τ X₂) M

instance CategoryTheory.NatTrans.CommShift₂.instIdFunctor {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_3, u_3} C₂] [Category.{v_5, u_5} D] {M : Type u_6} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₂ M] [HasShift D M] {G₁ : Functor C₁ (Functor C₂ D)} (h : CommShift₂Setup D M) [G₁.CommShift₂ h] : CommShift₂ (CategoryStruct.id G₁) h

instance CategoryTheory.NatTrans.CommShift₂.instCompFunctor {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_3, u_3} C₂] [Category.{v_5, u_5} D] {M : Type u_6} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₂ M] [HasShift D M] {G₁ G₂ G₃ : Functor C₁ (Functor C₂ D)} (τ : G₁ ⟶ G₂) (τ' : G₂ ⟶ G₃) (h : CommShift₂Setup D M) [G₁.CommShift₂ h] [G₂.CommShift₂ h] [G₃.CommShift₂ h] [CommShift₂ τ h] [CommShift₂ τ' h] : CommShift₂ (CategoryStruct.comp τ τ') h

@[reducible, inline]

abbrev CategoryTheory.NatTrans.CommShift₂Int {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_3, u_3} C₂] [Category.{v_5, u_5} D] [HasShift C₁ ℤ] [HasShift C₂ ℤ] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] {G₁ G₂ : Functor C₁ (Functor C₂ D)} [G₁.CommShift₂Int] [G₂.CommShift₂Int] (τ : G₁ ⟶ G₂) : Prop

If τ : G₁ ⟶ G₂ is a natural transformation between two bifunctors which commute shifts on both variables, this typeclass asserts a compatibility of τ with these shifts.

Equations

• CategoryTheory.NatTrans.CommShift₂Int τ = CategoryTheory.NatTrans.CommShift₂ τ CategoryTheory.CommShift₂Setup.int