The homotopy category #
HomotopyCategory V c
gives the category of chain complexes of shape c
in V
,
with chain maps identified when they are homotopic.
The congruence on HomologicalComplex V c
given by the existence of a homotopy.
Instances For
HomotopyCategory V c
is the category of chain complexes of shape c
in V
,
with chain maps identified when they are homotopic.
Instances For
The quotient functor from complexes to the homotopy category.
Instances For
If two chain maps become equal in the homotopy category, then they are homotopic.
Instances For
An arbitrarily chosen representation of the image of a chain map in the homotopy category is homotopic to the original chain map.
Equations
Instances For
Homotopy equivalent complexes become isomorphic in the homotopy category.
Equations
- HomotopyCategory.isoOfHomotopyEquiv f = { hom := (HomotopyCategory.quotient V c).map f.hom, inv := (HomotopyCategory.quotient V c).map f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
If two complexes become isomorphic in the homotopy category, then they were homotopy equivalent.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The i
-th homology, as a functor from the homotopy category.
Equations
Instances For
The homology functor on the homotopy category is induced by the homology functor on homological complexes.
Equations
Instances For
An additive functor induces a functor between homotopy categories.
Equations
Instances For
The obvious isomorphism between
HomotopyCategory.quotient V c ⋙ F.mapHomotopyCategory c
and
F.mapHomologicalComplex c ⋙ HomotopyCategory.quotient W c
when F : V ⥤ W
is
an additive functor.
Equations
Instances For
A natural transformation induces a natural transformation between the induced functors on the homotopy category.
Equations
- One or more equations did not get rendered due to their size.