Documentation

Mathlib.Algebra.Homology.SingleHomology

The homology of single complexes #

The main definition in this file is HomologicalComplex.homologyFunctorSingleIso which is a natural isomorphism single C c j ⋙ homologyFunctor C c j ≅ 𝟭 C.

The canonical isomorphism ((single C c j).obj A).cycles j ≅ A

Equations
Instances For

    The canonical isomorphism ((single C c j).obj A).opcycles j ≅ A

    Equations
    Instances For

      The canonical isomorphism ((single C c j).obj A).homology j ≅ A

      Equations
      Instances For

        The computation of the homology of single complexes, as a natural isomorphism single C c j ⋙ homologyFunctor C c j ≅ 𝟭 C.

        Equations
        Instances For