# mathlibdocumentation

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.

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.

## 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 #

The alternating face map complex, on objects

Equations
@[simp]

The alternating face map complex, on morphisms

Equations
@[simp]
@[simp]
theorem algebraic_topology.alternating_face_map_complex_map (C : Type u_1) (f : X Y) :

The alternating face map complex, as a functor

Equations
theorem algebraic_topology.map_alternating_face_map_complex {C : Type u_1} {D : Type u_3} (F : C D) [F.additive] :

## Construction of the natural inclusion of the normalized Moore complex #

noncomputable def algebraic_topology.inclusion_of_Moore_complex_map {A : Type u_3}  :

The inclusion map of the Moore complex in the alternating face map complex

Equations
@[simp]

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

Equations
@[simp]