Compression of bounded complexes to periodic complexes #
The n-periodic compression Δₙ folds an integer-indexed cochain complex K into a
ZMod n-indexed one:
(Δₙ K)^r = ⨁_{i ≡ r mod n} K^i, with differential induced by the differentials of K.
No signs are introduced. The coproduct over a residue class is Mathlib's
CategoryTheory.GradedObject.mapObj along the reduction ℤ → ZMod n, so the construction
TauCeti.PeriodicComplex.compression applies to every complex with these coproducts
(TauCeti.PeriodicComplex.HasCompression). A bounded complex has them in any category with zero
morphisms and finite coproducts, since only finitely many of its terms are nonzero.
The summand inclusions TauCeti.PeriodicComplex.ιCompression and the summand projections
TauCeti.PeriodicComplex.πCompression intertwine the differentials of K and of its compression.
The compression of a complex of projective objects has projective terms.
Compression is functorial, additive, and carries homotopies to homotopies. Consequently the
compression functor on bounded complexes, TauCeti.PeriodicComplex.compressionFunctor, descends
to TauCeti.PeriodicComplex.homotopyCompressionFunctor from the bounded homotopy category to the
n-periodic homotopy category. For n = 0, when ZMod 0 is integer indexing, every residue
class is a single degree.
The construction follows Mathlib's total complex of a bicomplex
(Mathlib.Algebra.Homology.TotalComplex), which also assembles a complex from coproducts
GradedObject.mapObj with differentials defined summand by summand.
References #
- T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.3.
A cochain complex has an n-periodic compression when, for every residue class modulo n,
its terms in the degrees of that class have a coproduct.
Instances For
The n-periodic compression of an integer-indexed cochain complex: its term of residue r
is the coproduct of the terms of K in the degrees congruent to r modulo n, and its
differential is induced by the differentials of K.
Instances For
The inclusion of the term of degree i into the term of its residue in the compression.
Instances For
A family of morphisms out of the terms in one residue class induces a morphism out of the corresponding term of the compression.
Instances For
The morphism induced by compressionDesc restricts to the prescribed morphism on each
summand.
The morphism induced by compressionDesc restricts to the prescribed morphism on each
summand.
Morphisms out of a term of the compression agree when they agree on every summand.
The compression of a complex of projective objects has projective terms: each term is a coproduct of projective objects.
On the summand of degree i, the differential of the compression is the differential of
K into degree i + 1.
On the summand of degree i, the differential of the compression is the differential of
K into degree i + 1.
Identifying two equal integer degrees before including them into the compression does not change the inclusion.
Identifying two equal integer degrees before including them into the compression does not change the inclusion.
Composing the inclusion of a summand with the identification of two equal residue degrees of the compression gives the inclusion into the other degree.
Composing the inclusion of a summand with the identification of two equal residue degrees of the compression gives the inclusion into the other degree.
The projection of the term of residue r of the compression onto the term of degree j
of K; it is zero when j does not lie in the residue class r.
Instances For
The inclusion of the term of degree j of K into the term of residue r of the
compression; it is zero when j does not lie in the residue class r.
Instances For
On a degree in the residue class r, ιCompressionOrZero is the summand inclusion.
On a degree outside the residue class r, ιCompressionOrZero is zero.
The projection onto the summand of degree j restricts to the identity on that summand and to
zero on the other summands.
The projection onto the summand of degree j restricts to the identity on that summand and to
zero on the other summands.
On a degree outside the residue class r, πCompression is zero.
The term of degree j of K is a retract of the term of its residue in the compression.
The term of degree j of K is a retract of the term of its residue in the compression.
The projections onto the summands of degrees i and j = i + 1 intertwine the differentials
of the compression and of K.
The projections onto the summands of degrees i and j = i + 1 intertwine the differentials
of the compression and of K.
The inclusions of the summands of degrees i and j = i + 1 intertwine the differentials
of K and of the compression.
The inclusions of the summands of degrees i and j = i + 1 intertwine the differentials
of K and of the compression.
The morphism of compressions induced by a morphism of cochain complexes.
Instances For
A morphism of compressions acts on the summand of degree i by the component of the
original morphism.
A morphism of compressions acts on the summand of degree i by the component of the
original morphism.
An isomorphism of complexes induces an isomorphism of their compressions.
Instances For
The forward map of the compressed isomorphism is the compression of the forward map.
The inverse map of the compressed isomorphism is the compression of the inverse map.
If every nonzero term of K in the residue class r has degree in T, the identity of the
term of residue r of the compression is the sum over T of the composites of the projections
and inclusions.
A homotopy between morphisms of cochain complexes induces a homotopy between the morphisms of their compressions.
Instances For
On the summand of degree i, the compressed homotopy is the homotopy into degree i - 1.
On the summand of degree i, the compressed homotopy is the homotopy into degree i - 1.
Compressions of morphisms that agree in the homotopy category agree in the periodic homotopy category.
A bounded cochain complex has an n-periodic compression: each residue class meets its
support in finitely many degrees.
The n-periodic compression of bounded cochain complexes.
Instances For
The compression functor sends a bounded complex to the compression of its underlying complex.
The compression functor acts on a morphism by compressing the underlying chain map, after transporting along the object equations.
The compression of a morphism in the homotopy category, computed through any representing
chain map; see quotientCompressionMap_eq.
Instances For
The compression of the class of a chain map is the class of its compression.
The isomorphism of compressions induced by an isomorphism in the homotopy category.
Instances For
The forward map of quotientCompressionIso compresses the forward map of the isomorphism.
The inverse of quotientCompressionIso compresses the inverse of the isomorphism.
The n-periodic compression of bounded cochain complexes, descended to their homotopy
category. It sends the class of a bounded complex to the class of its compression.
Instances For
The descended compression sends an object to the class of the compression of its underlying complex.
The descended compression acts on a morphism through any representing chain map, after transporting along the object equations.
The descended compression restricts along the quotient functor to the compression of bounded cochain complexes.
Instances For
The component of quotientCompHomotopyCompressionFunctorIso at a bounded complex is the
compression of the identification of the class of its underlying complex, after transporting
along the object equations.
The inverse component of quotientCompHomotopyCompressionFunctorIso at a bounded complex is
the compression of the inverse identification, after transporting along the object
equations.