Compression of mapping cones #
The n-periodic compression Δₙ of the mapping cone of a morphism φ : K ⟶ L of
integer-indexed cochain complexes is the periodic mapping cone of Δₙ φ. In residue degree r,
the summand K^(i+1) ⊞ L^i of Δₙ (cone φ), for i ≡ r modulo n, goes to the summands of
degrees i + 1 and i of (Δₙ K)^(r+1) ⊞ (Δₙ L)^r. No signs are introduced: the cone
differentials on both sides are [[-d, 0], [φ, d]].
The comparison is TauCeti.PeriodicComplex.compressionMappingConeIso. Its inverse is the morphism
out of the periodic cone determined by the compression of inr φ and the compression of the
standard null-homotopy of φ ≫ inr φ. Together with the comparison
TauCeti.PeriodicComplex.compressionShiftIso of compression with the shift, it identifies the
compression of Mathlib's mapping-cone triangle CochainComplex.mappingCone.triangle φ with the
periodic mapping-cone triangle of Δₙ φ
(TauCeti.PeriodicComplex.compressionMappingConeTriangleIso). Consequently the image of the
compressed triangle in the periodic homotopy category is distinguished
(TauCeti.PeriodicComplex.compressionMappingConeTriangle_mem_distTriang).
The results hold for every morphism between complexes whose compressions exist, for instance
bounded complexes: the degree-r term of the periodic cone exhibits the required coproduct for
the mapping cone (TauCeti.PeriodicComplex.hasCompression_mappingCone).
References #
- T. Stai, The triangulated hull of periodic complexes, Mathematical Research Letters 25 (2018), 199–236, Section 3.3.
The mapping cone of a morphism of complexes with n-periodic compressions has an n-periodic
compression: in each residue class, the coproduct is the corresponding term of the periodic
mapping cone of the compressed map.
The compression of φ ≫ inr φ is null-homotopic, by the compression of the standard
null-homotopy of φ ≫ inr φ.
Instances For
Compression of mapping cones. The compression of the mapping cone of φ is isomorphic to
the periodic mapping cone of the compression of φ. In residue degree r, the summand
K^(i+1) ⊞ L^i of the left side, for i ≡ r, is sent to the summands of degrees i + 1 and i
of (Δₙ K)^(r+1) ⊞ (Δₙ L)^r.
Instances For
The inverse comparison is the morphism out of the periodic cone determined by the compression
of inr φ and the compressed null-homotopy of φ ≫ inr φ.
On the summand of degree i, the comparison is given by the two projections of the mapping
cone followed by the inclusions into the compressions.
On the summand of degree i, the comparison is given by the two projections of the mapping
cone followed by the inclusions into the compressions.
On the left summand of the periodic cone, the inverse comparison is the compression of the
left inclusion inl φ of the mapping cone.
On the left summand of the periodic cone, the inverse comparison is the compression of the
left inclusion inl φ of the mapping cone.
On the right summand of the periodic cone, the inverse comparison is the compression of the
right inclusion inr φ of the mapping cone.
On the right summand of the periodic cone, the inverse comparison is the compression of the
right inclusion inr φ of the mapping cone.
The right inclusion of the periodic cone followed by the inverse comparison is the
compression of inr φ.
The right inclusion of the periodic cone followed by the inverse comparison is the
compression of inr φ.
The compression of the inclusion inr φ corresponds to the inclusion of the periodic
cone.
The compression of the inclusion inr φ corresponds to the inclusion of the periodic
cone.
The compression of the third morphism of the mapping-cone triangle of φ, followed by the
comparison of compression with the shift, corresponds to minus the projection of the periodic
cone.
The compression of the third morphism of the mapping-cone triangle of φ, followed by the
comparison of compression with the shift, corresponds to minus the projection of the periodic
cone.
The compression of the mapping-cone triangle K ⟶ L ⟶ mappingCone φ ⟶ K⟦1⟧ of φ: its
morphisms are the compressions of φ, of inr φ and of the third morphism of
mappingCone.triangle φ (the morphism induced by the cocycle -fst φ), the last followed by the
comparison compressionShiftIso of compression with the shift.
Instances For
Compression preserves mapping-cone triangles. The compression of the mapping-cone triangle
of φ is isomorphic to the periodic mapping-cone triangle of the compression of φ, by the
identity on the first two vertices and compressionMappingConeIso on the cone.
Instances For
The image in the periodic homotopy category of the compression of the mapping-cone triangle of a morphism of cochain complexes is distinguished.