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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : X.obj (Opposite.op (SimplexCategory.mk (n + 1))) ⟶ X.obj (Opposite.op (SimplexCategory.mk n))

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

theorem AlgebraicTopology.AlternatingFaceMapComplex.d_squared {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingFaceMapComplex.objD X (n + 1)) (AlgebraicTopology.AlternatingFaceMapComplex.objD X n) = 0

The chain complex relation d ≫ d

Construction of the alternating face map complex functor

def AlgebraicTopology.AlternatingFaceMapComplex.obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) : ChainComplex C ℕ

The alternating face map complex, on objects

@[simp]

theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : HomologicalComplex.X (AlgebraicTopology.AlternatingFaceMapComplex.obj X) n = X.obj (Opposite.op (SimplexCategory.mk n))

@[simp]

theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : HomologicalComplex.d (AlgebraicTopology.AlternatingFaceMapComplex.obj X) (n + 1) n = Finset.sum Finset.univ fun i => (-1) ^ ↑i • CategoryTheory.SimplicialObject.δ X i

def AlgebraicTopology.AlternatingFaceMapComplex.map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj Y

The alternating face map complex, on morphisms

@[simp]

theorem AlgebraicTopology.AlternatingFaceMapComplex.map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ) : HomologicalComplex.Hom.f (AlgebraicTopology.AlternatingFaceMapComplex.map f) n = f.app (Opposite.op (SimplexCategory.mk n))

def AlgebraicTopology.alternatingFaceMapComplex (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex C ℕ)

The alternating face map complex, as a functor

@[simp]

theorem AlgebraicTopology.alternatingFaceMapComplex_obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : HomologicalComplex.X ((AlgebraicTopology.alternatingFaceMapComplex C).obj X) n = X.obj (Opposite.op (SimplexCategory.mk n))

@[simp]

theorem AlgebraicTopology.alternatingFaceMapComplex_obj_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : HomologicalComplex.d ((AlgebraicTopology.alternatingFaceMapComplex C).obj X) (n + 1) n = AlgebraicTopology.AlternatingFaceMapComplex.objD X n

@[simp]

theorem AlgebraicTopology.alternatingFaceMapComplex_map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} {Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ) : HomologicalComplex.Hom.f ((AlgebraicTopology.alternatingFaceMapComplex C).map f) n = f.app (Opposite.op (SimplexCategory.mk n))

theorem AlgebraicTopology.map_alternatingFaceMapComplex {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor.comp (AlgebraicTopology.alternatingFaceMapComplex C) (CategoryTheory.Functor.mapHomologicalComplex F (ComplexShape.down ℕ)) = CategoryTheory.Functor.comp ((CategoryTheory.SimplicialObject.whiskering C D).obj F) (AlgebraicTopology.alternatingFaceMapComplex D)

theorem AlgebraicTopology.karoubi_alternatingFaceMapComplex_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (n : ℕ) : (HomologicalComplex.d (AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P)) (n + 1) n).f = CategoryTheory.CategoryStruct.comp (P.p.app (Opposite.op (SimplexCategory.mk (n + 1)))) (HomologicalComplex.d (AlgebraicTopology.AlternatingFaceMapComplex.obj P.X) (n + 1) n)

def AlgebraicTopology.AlternatingFaceMapComplex.ε {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented.drop (AlgebraicTopology.alternatingFaceMapComplex C) ⟶ CategoryTheory.Functor.comp CategoryTheory.SimplicialObject.Augmented.point (ChainComplex.single₀ C)

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

Construction of the natural inclusion of the normalized Moore complex

def AlgebraicTopology.inclusionOfMooreComplexMap {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) : (AlgebraicTopology.normalizedMooreComplex A).obj X ⟶ (AlgebraicTopology.alternatingFaceMapComplex A).obj X

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

@[simp]

theorem AlgebraicTopology.inclusionOfMooreComplexMap_f {A : Type u_2} [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) (n : ℕ) : HomologicalComplex.Hom.f (AlgebraicTopology.inclusionOfMooreComplexMap X) n = CategoryTheory.Subobject.arrow (AlgebraicTopology.NormalizedMooreComplex.objX X n)

@[simp]

theorem AlgebraicTopology.inclusionOfMooreComplex_app (A : Type u_2) [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] (X : CategoryTheory.SimplicialObject A) : (AlgebraicTopology.inclusionOfMooreComplex A).app X = AlgebraicTopology.inclusionOfMooreComplexMap X

def AlgebraicTopology.inclusionOfMooreComplex (A : Type u_2) [CategoryTheory.Category.{u_3, u_2} A] [CategoryTheory.Abelian A] : AlgebraicTopology.normalizedMooreComplex A ⟶ AlgebraicTopology.alternatingFaceMapComplex A

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

def AlgebraicTopology.AlternatingCofaceMapComplex.objD {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) (n : ℕ) : X.obj (SimplexCategory.mk n) ⟶ X.obj (SimplexCategory.mk (n + 1))

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

theorem AlgebraicTopology.AlternatingCofaceMapComplex.d_eq_unop_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) (n : ℕ) : AlgebraicTopology.AlternatingCofaceMapComplex.objD X n = (AlgebraicTopology.AlternatingFaceMapComplex.objD ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.obj (Opposite.op X)) n).unop

theorem AlgebraicTopology.AlternatingCofaceMapComplex.d_squared {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingCofaceMapComplex.objD X n) (AlgebraicTopology.AlternatingCofaceMapComplex.objD X (n + 1)) = 0

def AlgebraicTopology.AlternatingCofaceMapComplex.obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) : CochainComplex C ℕ

The alternating coface map complex, on objects

def AlgebraicTopology.AlternatingCofaceMapComplex.map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {X : CategoryTheory.CosimplicialObject C} {Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y) : AlgebraicTopology.AlternatingCofaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingCofaceMapComplex.obj Y

The alternating face map complex, on morphisms

@[simp]

theorem AlgebraicTopology.alternatingCofaceMapComplex_map (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] : ∀ {X Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y), (AlgebraicTopology.alternatingCofaceMapComplex C).map f = AlgebraicTopology.AlternatingCofaceMapComplex.map f

@[simp]

theorem AlgebraicTopology.alternatingCofaceMapComplex_obj (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.CosimplicialObject C) : (AlgebraicTopology.alternatingCofaceMapComplex C).obj X = AlgebraicTopology.AlternatingCofaceMapComplex.obj X

def AlgebraicTopology.alternatingCofaceMapComplex (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor (CategoryTheory.CosimplicialObject C) (CochainComplex C ℕ)

The alternating coface map complex, as a functor