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

• https://stacks.math.columbia.edu/tag/0194
• https://ncatlab.org/nlab/show/Moore+complex

## Construction of the alternating face map complex #

def AlgebraicTopology.AlternatingFaceMapComplex.objD {C : Type u_1} [] (n : ) :
X.obj { unop := SimplexCategory.mk (n + 1) } X.obj { unop := }

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

Equations
• = i : Fin (n + 2), (-1) ^ i X i
Instances For

## Construction of the alternating face map complex functor #

The alternating face map complex, on objects

Equations
Instances For
@[simp]
theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_X {C : Type u_1} [] (n : ) :
= X.obj { unop := }
@[simp]
theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq {C : Type u_1} [] (n : ) :
(n + 1) n = i : Fin (n + 2), (-1) ^ i X i

The alternating face map complex, on morphisms

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.AlternatingFaceMapComplex.map_f {C : Type u_1} [] (f : X Y) (n : ) :
= f.app { unop := }

The alternating face map complex, as a functor

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.alternatingFaceMapComplex_obj_X {C : Type u_1} [] (n : ) :
().X n = X.obj { unop := }
@[simp]
theorem AlgebraicTopology.alternatingFaceMapComplex_obj_d {C : Type u_1} [] (n : ) :
().d (n + 1) n =
@[simp]
theorem AlgebraicTopology.alternatingFaceMapComplex_map_f {C : Type u_1} [] (f : X Y) (n : ) :
().f n = f.app { unop := }
theorem AlgebraicTopology.map_alternatingFaceMapComplex {C : Type u_1} [] {D : Type u_2} [] (F : ) [F.Additive] :
(F.mapHomologicalComplex ) = ( F).comp
def AlgebraicTopology.AlternatingFaceMapComplex.ε {C : Type u_1} [] :
CategoryTheory.SimplicialObject.Augmented.drop.comp CategoryTheory.SimplicialObject.Augmented.point.comp

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero {C : Type u_1} [] :
(AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f 0 = X.hom.app { unop := }
@[simp]
theorem AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ {C : Type u_1} [] (n : ) :
(AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f (n + 1) = 0

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]

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

Equations
• = { app := AlgebraicTopology.inclusionOfMooreComplexMap, naturality := }
Instances For

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

Equations
• = i : Fin (n + 2), (-1) ^ i X i
Instances For

The alternating coface map complex, on objects

Equations
Instances For

The alternating face map complex, on morphisms

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.alternatingCofaceMapComplex_map (C : Type u_1) [] :
∀ {X Y : } (f : X Y),
@[simp]

The alternating coface map complex, as a functor

Equations
• One or more equations did not get rendered due to their size.
Instances For