# mathlibdocumentation

algebraic_topology.Moore_complex

## Moore complex #

We construct the normalized Moore complex, as a functor simplicial_object C ⥤ chain_complex 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 normalized_Moore_complex and should usually only be accessed via that.

@[simp]
noncomputable def algebraic_topology.normalized_Moore_complex.obj_X {C : Type u_1} (n : ) :

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

Equations
@[simp]
noncomputable def algebraic_topology.normalized_Moore_complex.obj_d {C : Type u_1} (n : ) :

The differentials in the normalized Moore complex.

Equations
noncomputable def algebraic_topology.normalized_Moore_complex.obj {C : Type u_1}  :

The normalized Moore complex functor, on objects.

Equations
@[simp]
@[simp]
theorem algebraic_topology.normalized_Moore_complex.obj_d_2 {C : Type u_1} (i j : ) :
= dite (i = j + 1) (λ (h : i = j + 1), (λ (h : ¬i = j + 1), 0)
noncomputable def algebraic_topology.normalized_Moore_complex.map {C : Type u_1} (f : X Y) :

The normalized Moore complex functor, on morphisms.

Equations
@[simp]
theorem algebraic_topology.normalized_Moore_complex.map_f {C : Type u_1} (f : X Y) (n : ) :
@[simp]
@[simp]
theorem algebraic_topology.normalized_Moore_complex_map (C : Type u_1) (f : X Y) :
noncomputable def algebraic_topology.normalized_Moore_complex (C : Type u_1)  :

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
@[simp]
theorem algebraic_topology.normalized_Moore_complex_obj_d {C : Type u_1} (n : ) :