Products of pretriangulated categories

The product C × D of two pretriangulated categories is pretriangulated for the componentwise shift of TauCeti/CategoryTheory/Shift/Prod.lean: a triangle is distinguished exactly when its images under the two projections are distinguished. Each axiom is checked coordinatewise, the rotation axiom through CategoryTheory.Functor.mapTriangleRotateIso.

The projections, the two zero sections, and products of triangulated functors are triangulated functors. These are the functors through which triangulated Grothendieck groups of products are compared with those of the factors.

Main definitions

• The CategoryTheory.Pretriangulated instance on C × D.

Main results

• TauCeti.mem_distTriang_prod_iff: a triangle in C × D is distinguished if and only if both of its projections are.
• CategoryTheory.Functor.IsTriangulated instances for CategoryTheory.Prod.fst C D, CategoryTheory.Prod.snd C D, CategoryTheory.Prod.sectL C 0, CategoryTheory.Prod.sectR 0 D, and F.prod G for triangulated functors F and G.

Implementation notes

As in TauCeti/CategoryTheory/Shift/Prod.lean, the third morphism of a triangle mapped along one of these functors involves a commutation isomorphism whose relevant coordinate is an identity only up to unfolding the shift on C × D. The corresponding square of each triangle isomorphism is therefore closed by an explicit identity in the factor.

@[instance_reducible]

noncomputable instance TauCeti.instPretriangulatedProd (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] : CategoryTheory.Pretriangulated (C × D)

The product of two pretriangulated categories is pretriangulated: a triangle is distinguished exactly when both of its projections are distinguished.

Equations

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

theorem TauCeti.mem_distTriang_prod_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (T : CategoryTheory.Pretriangulated.Triangle (C × D)) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ (CategoryTheory.Prod.fst C D).mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ∧ (CategoryTheory.Prod.snd C D).mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

A triangle in a product of pretriangulated categories is distinguished exactly when both of its projections are distinguished.

instance TauCeti.instIsTriangulatedProdFst (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] : (CategoryTheory.Prod.fst C D).IsTriangulated

The first projection of a product of pretriangulated categories is triangulated.

instance TauCeti.instIsTriangulatedProdSnd (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] : (CategoryTheory.Prod.snd C D).IsTriangulated

The second projection of a product of pretriangulated categories is triangulated.

instance TauCeti.instIsTriangulatedProdSectL (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] : (CategoryTheory.Prod.sectL C 0).IsTriangulated

Inserting a zero object in the second coordinate is a triangulated functor.

instance TauCeti.instIsTriangulatedProdSectR (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] : (CategoryTheory.Prod.sectR 0 D).IsTriangulated

Inserting a zero object in the first coordinate is a triangulated functor.

instance TauCeti.instIsTriangulatedFunctorProd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {C' : Type u_1} [CategoryTheory.Category.{v_1, u_1} C'] [CategoryTheory.Preadditive C'] [CategoryTheory.Limits.HasZeroObject C'] [CategoryTheory.HasShift C' ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C' n).Additive] [CategoryTheory.Pretriangulated C'] {D' : Type u_2} [CategoryTheory.Category.{v_2, u_2} D'] [CategoryTheory.Preadditive D'] [CategoryTheory.Limits.HasZeroObject D'] [CategoryTheory.HasShift D' ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D' n).Additive] [CategoryTheory.Pretriangulated D'] (F : CategoryTheory.Functor C C') (G : CategoryTheory.Functor D D') [F.CommShift ℤ] [G.CommShift ℤ] [F.IsTriangulated] [G.IsTriangulated] : (F.prod G).IsTriangulated

The product of two triangulated functors is triangulated.