Documentation

Mathlib.Algebra.Homology.QuasiIso

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?

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

Instances

    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.

    Instances For

      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.

      Instances For