Moore complex

We construct the normalized Moore complex, as a functor SimplicialObject C ⥤ ChainComplex C ℕ, for any abelian category C.

The n-th object is intersection of the kernels of X.δ i : X.obj n ⟶ X.obj (n-1), for i = 1, ..., n.

The differentials are induced from X.δ 0, which maps each of these intersections of kernels to the next.

This functor is one direction of the Dold-Kan equivalence, which we're still working towards.

References

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

The definitions in this namespace are all auxiliary definitions for NormalizedMooreComplex and should usually only be accessed via that.

def AlgebraicTopology.NormalizedMooreComplex.objX {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : CategoryTheory.Subobject (X.obj (Opposite.op (SimplexCategory.mk n)))

The normalized Moore complex in degree n, as a subobject of X n.

@[simp]

theorem AlgebraicTopology.NormalizedMooreComplex.objX_zero {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) : objX X 0 = ⊤

@[simp]

theorem AlgebraicTopology.NormalizedMooreComplex.objX_add_one {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : objX X (n + 1) = Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)

def AlgebraicTopology.NormalizedMooreComplex.objD {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : CategoryTheory.Subobject.underlying.obj (objX X (n + 1)) ⟶ CategoryTheory.Subobject.underlying.obj (objX X n)

The differentials in the normalized Moore complex.

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

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

The normalized Moore complex functor, on objects.

@[simp]

theorem AlgebraicTopology.NormalizedMooreComplex.obj_X {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : (obj X).X n = CategoryTheory.Subobject.underlying.obj (objX X n)

@[simp]

theorem AlgebraicTopology.NormalizedMooreComplex.obj_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (i j : ℕ) : (obj X).d i j = if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (match j with | 0 => CategoryTheory.CategoryStruct.comp (Finset.univ.inf fun (k : Fin (0 + 1)) => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)).arrow (CategoryTheory.CategoryStruct.comp (X.δ 0) (CategoryTheory.inv ⊤.arrow)) | n.succ => (Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)).factorThru (CategoryTheory.CategoryStruct.comp (Finset.univ.inf fun (k : Fin (n + 1 + 1)) => CategoryTheory.Limits.kernelSubobject (X.δ k.succ)).arrow (X.δ 0)) ⋯) else 0

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

The normalized Moore complex functor, on morphisms.

@[simp]

theorem AlgebraicTopology.NormalizedMooreComplex.map_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ) : (map f).f n = (objX Y n).factorThru (CategoryTheory.CategoryStruct.comp (objX X n).arrow (f.app (Opposite.op (SimplexCategory.mk n)))) ⋯

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

The (normalized) Moore complex of a simplicial object X in an abelian category C.

The n-th object is intersection of the kernels of X.δ i : X.obj n ⟶ X.obj (n-1), for i = 1, ..., n.

The differentials are induced from X.δ 0, which maps each of these intersections of kernels to the next.

@[simp]

theorem AlgebraicTopology.normalizedMooreComplex_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) : (normalizedMooreComplex C).obj X = NormalizedMooreComplex.obj X

@[simp]

theorem AlgebraicTopology.normalizedMooreComplex_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {X✝ Y✝ : CategoryTheory.SimplicialObject C} (f : X✝ ⟶ Y✝) : (normalizedMooreComplex C).map f = NormalizedMooreComplex.map f

theorem AlgebraicTopology.normalizedMooreComplex_objD {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (n : ℕ) : ((normalizedMooreComplex C).obj X).d (n + 1) n = NormalizedMooreComplex.objD X n