Shifts on product categories

If two categories C and D carry shifts by the same additive monoid A, their product carries the componentwise shift (X, Y)⟦a⟧ = (X⟦a⟧, Y⟦a⟧), whose structure isomorphisms are taken coordinatewise. This file constructs that shift and the commutation isomorphisms making the projections, products of shift-compatible functors, and (when A is a group) the two zero-section functors compatible with it. When the factors are preadditive with additive shift functors, the componentwise shift functors are additive. It is the shift underlying the pretriangulated structure on a product of pretriangulated categories.

Main definitions

• TauCeti.instHasShiftProd: the componentwise shift on C × D.
• TauCeti.instAdditiveShiftFunctorProd: the componentwise shift functors are additive.
• CategoryTheory.Functor.CommShift instances for CategoryTheory.Prod.fst C D, CategoryTheory.Prod.snd C D, F.prod G, CategoryTheory.Prod.sectL C 0 and CategoryTheory.Prod.sectR 0 D.

Main results

• TauCeti.shiftFunctor_prod_obj, TauCeti.shiftFunctor_prod_map_fst and TauCeti.shiftFunctor_prod_map_snd: the shift acts coordinatewise on objects and morphisms.
• TauCeti.shiftFunctorZero_prod_hom_app_fst, TauCeti.shiftFunctorAdd_prod_hom_app_fst and their variants: the structure isomorphisms of the shift are computed coordinatewise.

Implementation notes

The shift on C × D is a pair only after unfolding CategoryTheory.hasShiftMk, so simp cannot match lemmas such as CategoryTheory.Iso.prod_hom against a component whose target is a shifted object of C × D. The coherence proofs for the zero sections therefore close their nontrivial coordinate by an explicit identity in the factor, to which the component is definitionally equal.

@[instance_reducible]

noncomputable instance TauCeti.instHasShiftProd (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] : CategoryTheory.HasShift (C × D) A

The componentwise shift on a product category: (X, Y)⟦a⟧ = (X⟦a⟧, Y⟦a⟧).

Equations

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

@[simp]

theorem TauCeti.shiftFunctor_prod_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (X : C × D) (a : A) : (CategoryTheory.shiftFunctor (C × D) a).obj X = ((CategoryTheory.shiftFunctor C a).obj X.1, (CategoryTheory.shiftFunctor D a).obj X.2)

The shift of an object of C × D is the pair of the shifted coordinates.

@[simp]

theorem TauCeti.shiftFunctor_prod_map_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {X Y : C × D} (f : X ⟶ Y) (a : A) : ((CategoryTheory.shiftFunctor (C × D) a).map f).1 = (CategoryTheory.shiftFunctor C a).map f.1

The first coordinate of a shifted morphism of C × D is the shifted first coordinate.

@[simp]

theorem TauCeti.shiftFunctor_prod_map_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {X Y : C × D} (f : X ⟶ Y) (a : A) : ((CategoryTheory.shiftFunctor (C × D) a).map f).2 = (CategoryTheory.shiftFunctor D a).map f.2

The second coordinate of a shifted morphism of C × D is the shifted second coordinate.

@[simp]

theorem TauCeti.shiftFunctorZero_prod_hom_app_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (X : C × D) : ((CategoryTheory.shiftFunctorZero (C × D) A).hom.app X).1 = (CategoryTheory.shiftFunctorZero C A).hom.app X.1

The first coordinate of shiftFunctorZero (C × D) is shiftFunctorZero C.

@[simp]

theorem TauCeti.shiftFunctorZero_prod_hom_app_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (X : C × D) : ((CategoryTheory.shiftFunctorZero (C × D) A).hom.app X).2 = (CategoryTheory.shiftFunctorZero D A).hom.app X.2

The second coordinate of shiftFunctorZero (C × D) is shiftFunctorZero D.

@[simp]

theorem TauCeti.shiftFunctorZero_prod_inv_app_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (X : C × D) : ((CategoryTheory.shiftFunctorZero (C × D) A).inv.app X).1 = (CategoryTheory.shiftFunctorZero C A).inv.app X.1

The first coordinate of shiftFunctorZero (C × D) is shiftFunctorZero C.

@[simp]

theorem TauCeti.shiftFunctorZero_prod_inv_app_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (X : C × D) : ((CategoryTheory.shiftFunctorZero (C × D) A).inv.app X).2 = (CategoryTheory.shiftFunctorZero D A).inv.app X.2

The second coordinate of shiftFunctorZero (C × D) is shiftFunctorZero D.

@[simp]

theorem TauCeti.shiftFunctorAdd_prod_hom_app_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (X : C × D) : ((CategoryTheory.shiftFunctorAdd (C × D) a b).hom.app X).1 = (CategoryTheory.shiftFunctorAdd C a b).hom.app X.1

The first coordinate of shiftFunctorAdd (C × D) is shiftFunctorAdd C.

@[simp]

theorem TauCeti.shiftFunctorAdd_prod_hom_app_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (X : C × D) : ((CategoryTheory.shiftFunctorAdd (C × D) a b).hom.app X).2 = (CategoryTheory.shiftFunctorAdd D a b).hom.app X.2

The second coordinate of shiftFunctorAdd (C × D) is shiftFunctorAdd D.

@[simp]

theorem TauCeti.shiftFunctorAdd_prod_inv_app_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (X : C × D) : ((CategoryTheory.shiftFunctorAdd (C × D) a b).inv.app X).1 = (CategoryTheory.shiftFunctorAdd C a b).inv.app X.1

The first coordinate of shiftFunctorAdd (C × D) is shiftFunctorAdd C.

@[simp]

theorem TauCeti.shiftFunctorAdd_prod_inv_app_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (X : C × D) : ((CategoryTheory.shiftFunctorAdd (C × D) a b).inv.app X).2 = (CategoryTheory.shiftFunctorAdd D a b).inv.app X.2

The second coordinate of shiftFunctorAdd (C × D) is shiftFunctorAdd D.

instance TauCeti.instAdditiveShiftFunctorProd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {A : Type u_1} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), (CategoryTheory.shiftFunctor D a).Additive] (a : A) : (CategoryTheory.shiftFunctor (C × D) a).Additive

The componentwise shift functors on a product of preadditive categories are additive.

@[instance_reducible]

noncomputable instance TauCeti.instCommShiftProdFst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] : (CategoryTheory.Prod.fst C D).CommShift A

The first projection commutes with the componentwise shift, by the identity.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.instCommShiftProdSnd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] : (CategoryTheory.Prod.snd C D).CommShift A

The second projection commutes with the componentwise shift, by the identity.

Equations

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

@[simp]

theorem TauCeti.commShiftIso_fst_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a : A) (X : C × D) : (CategoryTheory.Functor.commShiftIso (CategoryTheory.Prod.fst C D) a).hom.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.shiftFunctor (C × D) a).comp (CategoryTheory.Prod.fst C D)).obj X)

The commutation isomorphism of the first projection with the shift is the identity.

@[simp]

theorem TauCeti.commShiftIso_fst_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a : A) (X : C × D) : (CategoryTheory.Functor.commShiftIso (CategoryTheory.Prod.fst C D) a).inv.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.Prod.fst C D).comp (CategoryTheory.shiftFunctor C a)).obj X)

The inverse commutation isomorphism of the first projection with the shift is the identity.

@[simp]

theorem TauCeti.commShiftIso_snd_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a : A) (X : C × D) : (CategoryTheory.Functor.commShiftIso (CategoryTheory.Prod.snd C D) a).hom.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.shiftFunctor (C × D) a).comp (CategoryTheory.Prod.snd C D)).obj X)

The commutation isomorphism of the second projection with the shift is the identity.

@[simp]

theorem TauCeti.commShiftIso_snd_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a : A) (X : C × D) : (CategoryTheory.Functor.commShiftIso (CategoryTheory.Prod.snd C D) a).inv.app X = CategoryTheory.CategoryStruct.id (((CategoryTheory.Prod.snd C D).comp (CategoryTheory.shiftFunctor D a)).obj X)

The inverse commutation isomorphism of the second projection with the shift is the identity.

@[instance_reducible]

noncomputable instance TauCeti.instCommShiftFunctorProd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {C' : Type u_2} [CategoryTheory.Category.{v_1, u_2} C'] {D' : Type u_3} [CategoryTheory.Category.{v_2, u_3} D'] [CategoryTheory.HasShift C' A] [CategoryTheory.HasShift D' A] (F : CategoryTheory.Functor C C') (G : CategoryTheory.Functor D D') [F.CommShift A] [G.CommShift A] : (F.prod G).CommShift A

A product of functors commuting with shifts commutes with the componentwise shifts.

Equations

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

@[simp]

theorem TauCeti.commShiftIso_prod_hom_app_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {C' : Type u_2} [CategoryTheory.Category.{v_1, u_2} C'] {D' : Type u_3} [CategoryTheory.Category.{v_2, u_3} D'] [CategoryTheory.HasShift C' A] [CategoryTheory.HasShift D' A] (F : CategoryTheory.Functor C C') (G : CategoryTheory.Functor D D') [F.CommShift A] [G.CommShift A] (a : A) (X : C × D) : ((CategoryTheory.Functor.commShiftIso (F.prod G) a).hom.app X).1 = (CategoryTheory.Functor.commShiftIso F a).hom.app X.1

The first coordinate of the commutation isomorphism of F.prod G is that of F.

@[simp]

theorem TauCeti.commShiftIso_prod_inv_app_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {C' : Type u_2} [CategoryTheory.Category.{v_1, u_2} C'] {D' : Type u_3} [CategoryTheory.Category.{v_2, u_3} D'] [CategoryTheory.HasShift C' A] [CategoryTheory.HasShift D' A] (F : CategoryTheory.Functor C C') (G : CategoryTheory.Functor D D') [F.CommShift A] [G.CommShift A] (a : A) (X : C × D) : ((CategoryTheory.Functor.commShiftIso (F.prod G) a).inv.app X).1 = (CategoryTheory.Functor.commShiftIso F a).inv.app X.1

The first coordinate of the inverse commutation isomorphism of F.prod G is that of F.

@[simp]

theorem TauCeti.commShiftIso_prod_hom_app_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {C' : Type u_2} [CategoryTheory.Category.{v_1, u_2} C'] {D' : Type u_3} [CategoryTheory.Category.{v_2, u_3} D'] [CategoryTheory.HasShift C' A] [CategoryTheory.HasShift D' A] (F : CategoryTheory.Functor C C') (G : CategoryTheory.Functor D D') [F.CommShift A] [G.CommShift A] (a : A) (X : C × D) : ((CategoryTheory.Functor.commShiftIso (F.prod G) a).hom.app X).2 = (CategoryTheory.Functor.commShiftIso G a).hom.app X.2

The second coordinate of the commutation isomorphism of F.prod G is that of G.

@[simp]

theorem TauCeti.commShiftIso_prod_inv_app_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] {C' : Type u_2} [CategoryTheory.Category.{v_1, u_2} C'] {D' : Type u_3} [CategoryTheory.Category.{v_2, u_3} D'] [CategoryTheory.HasShift C' A] [CategoryTheory.HasShift D' A] (F : CategoryTheory.Functor C C') (G : CategoryTheory.Functor D D') [F.CommShift A] [G.CommShift A] (a : A) (X : C × D) : ((CategoryTheory.Functor.commShiftIso (F.prod G) a).inv.app X).2 = (CategoryTheory.Functor.commShiftIso G a).inv.app X.2

The second coordinate of the inverse commutation isomorphism of F.prod G is that of G.

@[instance_reducible]

noncomputable instance TauCeti.instCommShiftProdSectL (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasZeroObject D] : (CategoryTheory.Prod.sectL C 0).CommShift A

Inserting a zero object in the second coordinate commutes with the componentwise shift: the commutation isomorphism is the identity in the first coordinate and the unique isomorphism 0 ≅ 0⟦a⟧ in the second.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.instCommShiftProdSectR (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (A : Type u_1) [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] : (CategoryTheory.Prod.sectR 0 D).CommShift A

Inserting a zero object in the first coordinate commutes with the componentwise shift: the commutation isomorphism is the unique isomorphism 0 ≅ 0⟦a⟧ in the first coordinate and the identity in the second.

Equations

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