# Documentation

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

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

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

Equations
Instances For
@[simp]
@[simp]
theorem AlgebraicTopology.NormalizedMooreComplex.objX_add_one {C : Type u_1} [] (n : ) :
= Finset.univ.inf fun (k : Fin (n + 1)) => CategoryTheory.Limits.kernelSubobject (X k.succ)
def AlgebraicTopology.NormalizedMooreComplex.objD {C : Type u_1} [] (n : ) :
CategoryTheory.Subobject.underlying.obj CategoryTheory.Subobject.underlying.obj

The differentials in the normalized Moore complex.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.NormalizedMooreComplex.obj_X {C : Type u_1} [] (n : ) :
= CategoryTheory.Subobject.underlying.obj
@[simp]
theorem AlgebraicTopology.NormalizedMooreComplex.obj_d {C : Type u_1} [] (i : ) (j : ) :
= if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (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

The normalized Moore complex functor, on objects.

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

The normalized Moore complex functor, on morphisms.

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

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicTopology.normalizedMooreComplex_objD {C : Type u_1} [] (n : ) :
().d (n + 1) n =