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 : ℕ)
:
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)
:
The alternating face map complex, on objects
Equations
- AlgebraicTopology.AlternatingFaceMapComplex.obj X = ChainComplex.of (fun (n : ℕ) => X.obj (Opposite.op (SimplexCategory.mk n))) (AlgebraicTopology.AlternatingFaceMapComplex.objD X) ⋯
@[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 : ℕ)
:
(AlgebraicTopology.AlternatingFaceMapComplex.obj X).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 : ℕ)
:
def
AlgebraicTopology.AlternatingFaceMapComplex.map
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{X Y : CategoryTheory.SimplicialObject C}
(f : X ⟶ Y)
:
The alternating face map complex, on morphisms
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
AlgebraicTopology.AlternatingFaceMapComplex.map_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
{X Y : CategoryTheory.SimplicialObject C}
(f : X ⟶ Y)
(n : ℕ)
:
(AlgebraicTopology.AlternatingFaceMapComplex.map f).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]
:
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.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.SimplicialObject C)
(n : ℕ)
:
((AlgebraicTopology.alternatingFaceMapComplex C).obj X).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 : ℕ)
:
((AlgebraicTopology.alternatingFaceMapComplex C).obj X).d (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 Y : CategoryTheory.SimplicialObject C}
(f : X ⟶ Y)
(n : ℕ)
:
((AlgebraicTopology.alternatingFaceMapComplex C).map f).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)
[F.Additive]
:
(AlgebraicTopology.alternatingFaceMapComplex C).comp (F.mapHomologicalComplex (ComplexShape.down ℕ)) = ((CategoryTheory.SimplicialObject.whiskering C D).obj F).comp (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 : ℕ)
:
((AlgebraicTopology.AlternatingFaceMapComplex.obj (CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P)).d
(n + 1) n).f = CategoryTheory.CategoryStruct.comp (P.p.app (Opposite.op (SimplexCategory.mk (n + 1))))
((AlgebraicTopology.AlternatingFaceMapComplex.obj P.X).d (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.SimplicialObject.Augmented.drop.comp (AlgebraicTopology.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.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
(X : CategoryTheory.SimplicialObject.Augmented C)
:
(AlgebraicTopology.AlternatingFaceMapComplex.ε.app X).f 0 = X.hom.app (Opposite.op (SimplexCategory.mk 0))
@[simp]
theorem
AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasZeroObject C]
(X : CategoryTheory.SimplicialObject.Augmented C)
(n : ℕ)
:
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
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
AlgebraicTopology.inclusionOfMooreComplexMap_f
{A : Type u_2}
[CategoryTheory.Category.{u_3, u_2} A]
[CategoryTheory.Abelian A]
(X : CategoryTheory.SimplicialObject A)
(n : ℕ)
:
def
AlgebraicTopology.inclusionOfMooreComplex
(A : Type u_2)
[CategoryTheory.Category.{u_3, u_2} A]
[CategoryTheory.Abelian 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]
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 : ℕ)
:
def
AlgebraicTopology.AlternatingCofaceMapComplex.obj
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(X : CategoryTheory.CosimplicialObject C)
:
The alternating coface map complex, on objects
Equations
- AlgebraicTopology.AlternatingCofaceMapComplex.obj X = CochainComplex.of (fun (n : ℕ) => X.obj (SimplexCategory.mk n)) (AlgebraicTopology.AlternatingCofaceMapComplex.objD X) ⋯
def
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)
:
The alternating face map complex, on morphisms
Equations
- One or more equations did not get rendered due to their size.
def
AlgebraicTopology.alternatingCofaceMapComplex
(C : Type u_1)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
:
The alternating coface map complex, as a functor
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[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✝)
: