# mathlib3documentation

algebraic_topology.alternating_face_map_complex

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

## 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]
theorem algebraic_topology.alternating_face_map_complex.obj_d_eq {C : Type u_1} (n : ) :
= finset.univ.sum (λ (i : fin (n + 2)), (-1) ^ i X.δ i)

The alternating face map complex, on morphisms

Equations
@[simp]
theorem algebraic_topology.alternating_face_map_complex.map_f {C : Type u_1} (f : X Y) (n : ) :

The alternating face map complex, as a functor

Equations
@[simp]
theorem algebraic_topology.alternating_face_map_complex_map_f {C : Type u_1} (f : X Y) (n : ) :
= f.app
@[simp]

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

Equations

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

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

Equations
Instances for algebraic_topology.inclusion_of_Moore_complex_map
@[simp]

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

Equations
@[simp]
@[simp]

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

Equations

The alternating coface map complex, on objects

Equations
@[simp]

The alternating face map complex, on morphisms

Equations
@[simp]

The alternating coface map complex, as a functor

Equations
@[simp]