mathlib3 documentation

algebra.homology.quasi_iso

Quasi-isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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