mathlib documentation

algebra.homology.quasi_iso

Quasi-isomorphisms #

A chain map is a quasi-isomorphism if it induces isomorphisms on homology.

Future work #

Define the derived category as the localization at quasi-isomorphisms?

If a chain map f : X ⟶ Y[0] is a quasi-isomorphism, then the cokernel of the differential d : X₁ → X₀ is isomorphic to Y.

Equations

If a cochain map f : Y[0] ⟶ X is a quasi-isomorphism, then the kernel of the differential d : X₀ → X₁ is isomorphic to Y.

Equations