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

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

Equations

• AlgebraicTopology.AlternatingFaceMapComplex.objD X n = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i

The chain complex relation d ≫ d

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

Construction of the alternating face map complex functor

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

The alternating face map complex, on objects

Equations

• AlgebraicTopology.AlternatingFaceMapComplex.obj X = ChainComplex.of (fun (n : ℕ) => X.obj (Opposite.op { len := n })) (AlgebraicTopology.AlternatingFaceMapComplex.objD X) ⋯

@[simp]

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

@[simp]

theorem AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : (obj X).d (n + 1) n = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i

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

The alternating face map complex, on morphisms

Equations

• AlgebraicTopology.AlternatingFaceMapComplex.map f = ChainComplex.ofHom (fun (n : ℕ) => f.app (Opposite.op { len := n })) ⋯

@[simp]

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

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

The alternating face map complex, as a functor

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

instance AlgebraicTopology.instAdditiveSimplicialObjectChainComplexNatAlternatingFaceMapComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] : (alternatingFaceMapComplex C).Additive

instance AlgebraicTopology.instPreservesMonomorphismsSimplicialObjectChainComplexNatAlternatingFaceMapComplexOfHasPullbacks {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasPullbacks C] : (alternatingFaceMapComplex C).PreservesMonomorphisms

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

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

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.

@[simp]

theorem AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : CategoryTheory.SimplicialObject.Augmented C) : (ε.app X).f 0 = X.hom.app (Opposite.op { len := 0 })

@[simp]

theorem AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : CategoryTheory.SimplicialObject.Augmented C) (n : ℕ) : (ε.app X).f (n + 1) = 0

Construction of the natural inclusion of the normalized Moore complex

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

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

Equations

• AlgebraicTopology.inclusionOfMooreComplexMap X = ChainComplex.ofHom (fun (n : ℕ) => (AlgebraicTopology.NormalizedMooreComplex.objX X n).arrow) ⋯

@[simp]

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

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

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

Equations

• AlgebraicTopology.inclusionOfMooreComplex A = { app := AlgebraicTopology.inclusionOfMooreComplexMap, naturality := ⋯ }

@[simp]

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

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

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

Equations

• AlgebraicTopology.AlternatingCofaceMapComplex.objD X n = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i

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

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

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

The alternating coface map complex, on objects

Equations

• AlgebraicTopology.AlternatingCofaceMapComplex.obj X = CochainComplex.of (fun (n : ℕ) => X.obj { len := n }) (AlgebraicTopology.AlternatingCofaceMapComplex.objD X) ⋯

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

The alternating face map complex, on morphisms

Equations

• AlgebraicTopology.AlternatingCofaceMapComplex.map f = CochainComplex.ofHom (fun (n : ℕ) => f.app { len := n }) ⋯

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

The alternating coface map complex, as a functor

Equations

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

@[simp]

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

@[simp]

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