# Documentation

Mathlib.AlgebraicTopology.DoldKan.FunctorN

# Construction of functors N for the Dold-Kan correspondence #

In this file, we construct functors N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) and N₂ : Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ) for any preadditive category C. (The indices of these functors are the number of occurrences of Karoubi at the source or the target.)

In the case C is additive, the functor N₂ shall be the functor of the equivalence CategoryTheory.Preadditive.DoldKan.equivalence defined in EquivalenceAdditive.lean.

In the case the category C is pseudoabelian, the composition of N₁ with the inverse of the equivalence ChainComplex C ℕ ⥤ Karoubi (ChainComplex C ℕ) will be the functor CategoryTheory.Idempotents.DoldKan.N of the equivalence of categories CategoryTheory.Idempotents.DoldKan.equivalence : SimplicialObject C ≌ ChainComplex C ℕ defined in EquivalencePseudoabelian.lean.

When the category C is abelian, a relation between N₁ and the normalized Moore complex functor shall be obtained in Normalized.lean.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

@[simp]
theorem AlgebraicTopology.DoldKan.N₁_map_f {C : Type u_1} [] :
∀ {X Y : } (f : X Y), (AlgebraicTopology.DoldKan.N₁.map f).f = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty ()
@[simp]
theorem AlgebraicTopology.DoldKan.N₁_obj_p {C : Type u_1} [] :
(AlgebraicTopology.DoldKan.N₁.obj X).p = AlgebraicTopology.DoldKan.PInfty
@[simp]
theorem AlgebraicTopology.DoldKan.N₁_obj_X {C : Type u_1} [] :
(AlgebraicTopology.DoldKan.N₁.obj X).X =

The functor SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) which maps X to the formal direct factor of K[X] defined by PInfty.

Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.N₂_map_f_f {C : Type u_1} [] :
∀ {X Y : } (f : X Y) (i : ), HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.N₂.map f).f i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty i) (f.f.app ())
@[simp]
theorem AlgebraicTopology.DoldKan.N₂_obj_X_d {C : Type u_1} [] (i : ) (j : ) :
HomologicalComplex.d (AlgebraicTopology.DoldKan.N₂.obj P).X i j = if h : i = j + 1 then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : P.X.obj () = P.X.obj (Opposite.op (SimplexCategory.mk (j + 1))))) (Finset.sum Finset.univ fun i => (-1) ^ i ) else 0
@[simp]
theorem AlgebraicTopology.DoldKan.N₂_obj_X_X {C : Type u_1} [] (n : ) :
HomologicalComplex.X (AlgebraicTopology.DoldKan.N₂.obj P).X n = P.X.obj ()
@[simp]
theorem AlgebraicTopology.DoldKan.N₂_obj_p_f {C : Type u_1} [] (i : ) :
HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.N₂.obj P).p i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty i) (P.p.app ())

The extension of N₁ to the Karoubi envelope of SimplicialObject C.

Instances For
theorem AlgebraicTopology.DoldKan.compatibility_N₁_N₂ {C : Type u_1} [] :
CategoryTheory.Functor.comp () AlgebraicTopology.DoldKan.N₂ = AlgebraicTopology.DoldKan.N₁