The split stable category of complexes is the homotopy category #
For a complex shape in which every index has a successor, the projective stable category of the componentwise split exact structure is equivalent to Mathlib's homotopy category. The comparison sends a complex to itself and a stable morphism to its homotopy class. It is additive and, over a linear category, linear.
The key identification is that a chain map factors through a relative projective exactly when it is null-homotopic. A null-homotopy lifts the map through a componentwise split projective presentation of its target. Conversely, a contraction of an intermediate projective gives a null-homotopy of the composite. Thus the stable ideal is precisely the kernel of the homotopy quotient, with no choice of representatives in the comparison functor.
This applies to ComplexShape.up ℕ, integer-indexed complexes and to ComplexShape.up (ZMod n)
for every positive period n, including one-periodic differential objects. The equivalence supplies
the comparison
needed to relate the stable triangulation to the homotopy category; compatibility of their
shifts and triangles is a separate assertion.
References #
- Bernhard Keller, Chain complexes and stable categories, Manuscripta Mathematica 67 (1990), 379–417, Section 1.
- Torkil Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.
The construction uses Mathlib's Homotopy.nullHomotopicMap, HomotopyCategory.quotient and the
morphism-ideal quotient universal property.
A null-homotopic chain map factors through a relative projective for the componentwise split exact structure, when every index has a successor, by lifting its null-homotopy through a componentwise split projective presentation of its target.
Factoring through a relative projective is the same as being null-homotopic for the componentwise split exact structure, when every index has a successor.
The projective stable ideal of the componentwise split exact structure is exactly the kernel of the quotient to the homotopy category.
The canonical comparison from the componentwise split stable category to the homotopy category, sending a stable class of chain maps to its homotopy class.
Equations
Instances For
The comparison restricts to the ordinary homotopy quotient on complexes.
On objects the comparison sends the stable class of a complex to its homotopy class.
On morphisms the comparison sends the stable class to the homotopy class of the same map.
The stable-to-homotopy comparison preserves addition of morphisms.
The stable-to-homotopy comparison preserves scalars when the base category is linear.
The comparison is an equivalence: both quotients kill exactly the null-homotopic maps.
The projective stable category of componentwise split complexes is equivalent to their homotopy category. This is an additive equivalence, and linear over any scalar semiring for which the base category is linear.
Equations
Instances For
The functor of the stable/homotopy equivalence is the canonical comparison.
The equivalence's forward functor is additive; Mathlib then also makes its inverse additive.
Both directions of the equivalence preserve scalars over a linear base category.
The inverse equivalence sends the homotopy class of a complex back to its stable class, naturally in complexes. The components of this identification are the inverse unit of the equivalence.