Documentation

Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

The alternating face map complex of a simplicial object in a preadditive category #

We construct the alternating face map complex, as a functor alternatingFaceMapComplex : SimplicialObject C ⥤ ChainComplex C ℕ for any preadditive category C. For any simplicial object X in C, this is the homological complex ... → X_2 → X_1 → X_0 where the differentials are alternating sums of faces.

The dual version alternatingCofaceMapComplex : CosimplicialObject C ⥤ CochainComplex C ℕ is also constructed.

We also construct the natural transformation inclusionOfMooreComplex : normalizedMooreComplex A ⟶ alternatingFaceMapComplex A when A is an abelian category.

References #

Construction of the alternating face map complex #

The differential on the alternating face map complex is the alternate sum of the face maps

Instances For

    Construction of the alternating face map complex functor #

    The natural transformation which gives the augmentation of the alternating face map complex attached to an augmented simplicial object.

    Instances For

      Construction of the natural inclusion of the normalized Moore complex #

      The inclusion map of the Moore complex in the alternating face map complex, as a natural transformation

      Instances For

        The differential on the alternating coface map complex is the alternate sum of the coface maps

        Instances For