Complexes with the componentwise split exact structure are Frobenius

Let C be an additive category and c a complex shape. The componentwise split exact structure (ExactStructure.split C).homologicalComplex c on HomologicalComplex C c has as conflations the short complexes of complexes which split in every degree, not necessarily compatibly with the differentials. This file proves that it is a Frobenius exact structure whose projective and injective objects are exactly the contractible complexes, those K with a homotopy Homotopy (𝟙 K) 0, as soon as every index of c is both the source and the target of a relation. This holds for cochain and chain complexes indexed by ℤ and for the n-periodic complexes indexed by ComplexShape.up (ZMod n).

These results are what the stable-category machinery needs to apply to complexes. The projective stable category ((split C).homologicalComplex c).ProjectiveStableCategory kills the morphisms factoring through a contractible complex, which are the null-homotopic ones, so it is a model of the homotopy category of complexes of shape c. Being Frobenius, it is triangulated by Happel's theorem TauCeti.ExactStructure.IsFrobenius.stableIsTriangulated. In particular this covers the homotopy categories of ℤ-indexed and of n-periodic complexes. The comparison with Mathlib's HomotopyCategory C c is not part of this file.

The hypotheses on the shape are needed: for ℕ-indexed chain complexes, a nonzero object placed in degree 0 is relatively projective but not relatively injective.

Main results

• TauCeti.ExactStructure.homologicalComplex_split_isInjective_iff and TauCeti.ExactStructure.homologicalComplex_split_isProjective_iff: the relatively injective and relatively projective complexes are the contractible ones.
• TauCeti.ExactStructure.homologicalComplex_split_isFrobenius: the componentwise split exact structure on complexes is Frobenius.
• TauCeti.ExactStructure.homologicalComplex_split_up'_isFrobenius and TauCeti.ExactStructure.homologicalComplex_split_down'_isFrobenius: the special cases of the shapes ComplexShape.up' a and ComplexShape.down' a over an additive group. These include ComplexShape.up ℤ, ComplexShape.down ℤ and the periodic shapes ComplexShape.up (ZMod n).

References

• Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1, where the category of complexes with the componentwise split exact structure is shown to be Frobenius with the contractible complexes as its projective-injective objects.
• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 3.
• Torkil Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3, for the periodic case.

theorem TauCeti.ExactStructure.homologicalComplex_split_isInjective_of_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} {K : HomologicalComplex C c} (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) : ((split C).homologicalComplex c).isInjective K

A contractible complex is relatively injective for the componentwise split exact structure, for every complex shape.

theorem TauCeti.ExactStructure.homologicalComplex_split_isProjective_of_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} {K : HomologicalComplex C c} (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) : ((split C).homologicalComplex c).isProjective K

A contractible complex is relatively projective for the componentwise split exact structure, for every complex shape.

theorem TauCeti.ExactStructure.homologicalComplex_split_isInflation_inr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} [DecidableRel c.Rel] {F G : HomologicalComplex C c} (φ : F ⟶ G) : ((split C).homologicalComplex c).IsInflation (HomologicalComplex.homotopyCofiber.inr φ)

The inclusion of a complex into the mapping cone of a morphism is a componentwise split inflation: in degree i it is the inclusion of the summand G.X i of F.X j ⊞ G.X i for c.Rel i j, and an isomorphism when i is the source of no relation.

theorem TauCeti.ExactStructure.homologicalComplex_split_enoughInjectives {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) : ((split C).homologicalComplex c).EnoughInjectives

Every complex is a componentwise split subobject of a contractible one, the mapping cone of its identity.

theorem TauCeti.ExactStructure.homologicalComplex_split_enoughProjectives {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} (hc : ∀ (i : ι), ∃ (j : ι), c.Rel i j) : ((split C).homologicalComplex c).EnoughProjectives

Every complex is a componentwise split quotient of a contractible one.

theorem TauCeti.ExactStructure.homologicalComplex_split_isInjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (K : HomologicalComplex C c) : ((split C).homologicalComplex c).isInjective K ↔ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id K) 0)

The relatively injective complexes are the contractible ones. For the componentwise split exact structure, and when every index of the shape is the target of a relation, a complex is relatively injective exactly when its identity is null-homotopic.

theorem TauCeti.ExactStructure.homologicalComplex_split_isProjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} (hc : ∀ (i : ι), ∃ (j : ι), c.Rel i j) (K : HomologicalComplex C c) : ((split C).homologicalComplex c).isProjective K ↔ Nonempty (Homotopy (CategoryTheory.CategoryStruct.id K) 0)

The relatively projective complexes are the contractible ones. For the componentwise split exact structure, and when every index of the shape is the source of a relation, a complex is relatively projective exactly when its identity is null-homotopic.

theorem TauCeti.ExactStructure.homologicalComplex_split_isFrobenius {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {ι : Type u'} {c : ComplexShape ι} (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (hc' : ∀ (i : ι), ∃ (j : ι), c.Rel i j) : ((split C).homologicalComplex c).IsFrobenius

Complexes form a Frobenius exact category. If every index of the complex shape c is both the source and the target of a relation, the componentwise split exact structure on HomologicalComplex C c is Frobenius, and its projective-injective objects are the contractible complexes (homologicalComplex_split_isProjective_iff).

theorem TauCeti.ExactStructure.homologicalComplex_split_up'_isFrobenius {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {α : Type u_1} [AddGroup α] (a : α) : ((split C).homologicalComplex (ComplexShape.up' a)).IsFrobenius

Complexes of shape ComplexShape.up' a over an additive group, such as cochain complexes indexed by ℤ and periodic complexes indexed by ZMod n, form a Frobenius exact category for the componentwise split exact structure.

theorem TauCeti.ExactStructure.homologicalComplex_split_down'_isFrobenius {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {α : Type u_1} [AddGroup α] (a : α) : ((split C).homologicalComplex (ComplexShape.down' a)).IsFrobenius

Complexes of shape ComplexShape.down' a over an additive group, such as chain complexes indexed by ℤ, form a Frobenius exact category for the componentwise split exact structure.