Construction of functors N for the Dold-Kan correspondence #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
TODO (@joelriou) continue adding the various files referenced below
In this file, we construct functors N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)
and N₂ : karoubi (simplicial_object C) ⥤ karoubi (chain_complex 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
category_theory.preadditive.dold_kan.equivalence defined in equivalence_additive.lean.
In the case the category C is pseudoabelian, the composition of N₁ with the inverse of the
equivalence chain_complex C ℕ ⥤ karoubi (chain_complex C ℕ) will be the functor
category_theory.idempotents.dold_kan.N of the equivalence of categories
category_theory.idempotents.dold_kan.equivalence : simplicial_object C ≌ chain_complex C ℕ
defined in equivalence_pseudoabelian.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.)
The functor simplicial_object C ⥤ karoubi (chain_complex C ℕ) which maps
X to the formal direct factor of K[X] defined by P_infty.
Equations
- algebraic_topology.dold_kan.N₁ = {obj := λ (X : category_theory.simplicial_object C), {X := algebraic_topology.alternating_face_map_complex.obj X, p := algebraic_topology.dold_kan.P_infty X, idem := _}, map := λ (X Y : category_theory.simplicial_object C) (f : X ⟶ Y), {f := algebraic_topology.dold_kan.P_infty ≫ algebraic_topology.alternating_face_map_complex.map f, comm := _}, map_id' := _, map_comp' := _}
Instances for algebraic_topology.dold_kan.N₁
The extension of N₁ to the Karoubi envelope of simplicial_object C.