Split simplicial objects in preadditive categories #
In this file we define a functor
nondegComplex : SimplicialObject.Split C ⥤ ChainComplex C ℕ
C is a preadditive category with finite coproducts, and get an isomorphism
toKaroubiNondegComplexFunctorIsoN₁ : nondegComplex ⋙ toKaroubi _ ≅ forget C ⋙ DoldKan.N₁.
Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)
The projection on a summand of the coproduct decomposition given by a splitting of a simplicial object.
If a simplicial object
X in an additive category is split,
PInfty vanishes on all the summands of
X _[n] which do
not correspond to the identity of
s.d i j : s.N i ⟶ s.N j on nondegenerate simplices of a split
simplicial object are induced by the differentials on the alternating face map complex.
s is a splitting of a simplicial object
X in a preadditive category,
s.nondeg_complex is a chain complex which is given in degree
The chain complex
s.nondegComplex attached to a splitting of a simplicial object
becomes isomorphic to the normalized Moore complex
N₁.obj X defined as a formal direct
factor in the category
Karoubi (ChainComplex C ℕ).
The functor which sends a split simplicial object in a preadditive category to the chain complex which consists of nondegenerate simplices.
The natural isomorphism (in
Karoubi (ChainComplex C ℕ)) between the chain complex
of nondegenerate simplices of a split simplicial object and the normalized Moore complex
defined as a formal direct factor of the alternating face map complex.