Mapping cones of split monomorphisms, and maps of mapping cones #
Let 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 be a short complex of homological complexes which is split in the
category of complexes: the retraction r : X₂ ⟶ X₁ of f and the section s : X₃ ⟶ X₂ of g
are chain maps. Then the mapping cone homotopyCofiber f of f is homotopy equivalent to the
cokernel X₃. The map from the cone is homotopyCofiber.desc f g, which exists because
f ≫ g = 0, and its homotopy inverse is s followed by the inclusion homotopyCofiber.inr f of
X₂ into the cone. One composite is s ≫ g = 𝟙, and the other is homotopic to the identity
through the homotopy which sends the X₂-summand of the cone to its X₁-summand by -r.
We assume, as Mathlib's homotopyCofiber.inrCompHomotopy does, that every index of the complex
shape is the target of some relation. This holds for ComplexShape.up ℤ, ComplexShape.down ℤ
and the one-object shape ComplexShape.refl Unit.
The motivating example is multiplication by X - a on the polynomial extension A[X] ⊗[A] K of
a complex K of A-modules, split by division by X - a and by the constant polynomials (see
TauCeti.Algebra.Homology.PolynomialExtension). This is how the stabilization invariance of grid
homology compares a grid complex with the mapping cone of V₁ - V₂.
Conversely, a one-object complex (over the shape ComplexShape.refl Unit) whose object splits as
a direct sum K ⊕ L, with L a subcomplex, is the mapping cone of the component K ⟶ L of its
differential. This is how the unblocked complex of a stabilized grid diagram is presented as a
mapping cone.
The mapping cone of an identity is contractible (homotopyCofiber.homotopyToZeroOfId), the
analogue for homotopyCofiber of Mathlib's CochainComplex.mappingCone.homotopyToZeroOfId.
Finally, a morphism of arrows α from φ : F ⟶ G to φ' : F' ⟶ G' induces a map of mapping
cones homotopyCofiber.mapArrowHom φ φ' _ α. If both components of α are
quasi-isomorphisms, so is the induced map of cones. For grid stabilization, this transfers a
quasi-isomorphism on the off-center states to the comparison map for the whole stabilized
complex.
Main definitions #
CategoryTheory.ShortComplex.Splitting.homotopyCofiberHomotopyEquiv: the homotopy equivalence between the mapping cone ofS.fandS.X₃for a split short complex of complexesS.HomologicalComplex.homotopyCofiber.isoOfSplitting: a one-object complex with a block lower-triangular differential is isomorphic to the mapping cone of its off-diagonal block.HomologicalComplex.homotopyCofiber.homotopyToZeroOfId: a contraction of the mapping cone of an identity.
Main results #
CategoryTheory.ShortComplex.Splitting.quasiIso_homotopyCofiberDesc: the map from the mapping cone ofS.ftoS.X₃induced byS.gis a quasi-isomorphism.HomologicalComplex.homotopyCofiber.inr_mapArrowHom,HomologicalComplex.homotopyCofiber.inrX_mapArrowHom_f,HomologicalComplex.homotopyCofiber.inlX_mapArrowHom_f: the components of a map of cones.HomologicalComplex.homotopyCofiber.quasiIso_mapArrowHom: a map of mapping cones induced by quasi-isomorphisms is a quasi-isomorphism.HomologicalComplex.homotopyCofiber.quasiIso_mapArrowHom_id: any morphism induces a quasi-isomorphism between the mapping cones of identities.
References #
- C. A. Weibel, An introduction to homological algebra, Section 1.5.
- P. Ozsváth, A. Stipsicz, Z. Szabó, Grid Homology for Knots and Links, Section 5.2.
For a short complex of complexes S split by chain maps, the mapping cone of S.f is
homotopy equivalent to S.X₃. The map from the cone is induced by S.g, and its homotopy inverse
is the section σ.s followed by the inclusion of S.X₂ into the cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map from the mapping cone in homotopyCofiberHomotopyEquiv is induced by S.g.
The homotopy inverse in homotopyCofiberHomotopyEquiv is the section σ.s followed by the
inclusion of S.X₂ into the mapping cone.
For a short complex of complexes S split by chain maps, the map from the mapping cone of
S.f to S.X₃ induced by S.g is a quasi-isomorphism.
Mapping cones of one-object complexes #
A triangular one-object complex is a mapping cone. Let M be a one-object complex whose
object is split as M.X () = K.X () ⊕ L.X () by σ, with inr and σ.s the inclusions of the
summands, in such a way that L.X () is a subcomplex (hr) and the differential of M restricted
to K.X () is φ - d_K in block form (hs). Then M is the mapping cone of φ.
The sign in hs is that of Mathlib's homotopyCofiber, whose differential is -d_K on the
K-summand; over a ring of characteristic two it disappears.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On the cone, isoOfSplitting is σ.s on the K-summand and inr on the L-summand.
The inverse of isoOfSplitting sends M into the cone through fst and the retraction
σ.r.
The mapping cone of an identity is contractible #
The mapping cone of an identity is contractible. In the cone of 𝟙 K, whose term in
degree i is K.X j ⊞ K.X i for c.Rel i j, the contracting homotopy sends the second summand
identically onto the first summand of the term in the previous degree. This needs every index
of the complex shape to be the target of some relation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Maps of mapping cones #
The map of cones induced by a morphism of arrows α restricts to α.right on the inclusion
of the target.
The map of cones induced by a morphism of arrows α restricts to α.right on the inclusion
of the target.
On the summand G of the mapping cone, the map of cones induced by a morphism of arrows α
is α.right.
On the summand G of the mapping cone, the map of cones induced by a morphism of arrows α
is α.right.
On the summand F of the mapping cone, the map of cones induced by a morphism of arrows α
is α.left.
On the summand F of the mapping cone, the map of cones induced by a morphism of arrows α
is α.left.
The map of cones of identities induced by any morphism is a quasi-isomorphism, since both cones are contractible. The morphism itself need not be a quasi-isomorphism.
Maps of mapping cones preserve quasi-isomorphisms. If a morphism of arrows α from
φ : F ⟶ G to φ' : F' ⟶ G' consists of quasi-isomorphisms, the induced map of mapping cones
homotopyCofiber φ ⟶ homotopyCofiber φ' is a quasi-isomorphism.