mathlib documentation

algebraic_topology.alternating_face_map_complex

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

We construct the alternating face map complex, as a functor alternating_face_map_complex : simplicial_object C ⥤ chain_complex 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 alternating_coface_map_complex : cosimplicial_object C ⥤ cochain_complex C ℕ is also constructed.

We also construct the natural transformation inclusion_of_Moore_complex : normalized_Moore_complex A ⟶ alternating_face_map_complex A when A is an abelian category.

References #

Construction of the alternating face map complex #

@[simp]

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

Equations

Construction of the alternating face map complex functor #

Construction of the natural inclusion of the normalized Moore complex #

@[simp]

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

Equations