The Dold-Kan correspondence for pseudoabelian categories #

In this file, for any idempotent complete additive category C, the Dold-Kan equivalence Idempotents.DoldKan.Equivalence C : SimplicialObject C ≌ ChainComplex C ℕ is obtained. It is deduced from the equivalence Preadditive.DoldKan.Equivalence between the respective idempotent completions of these categories using the fact that when C is idempotent complete, then both SimplicialObject C and ChainComplex C ℕ are idempotent complete.

The construction of Idempotents.DoldKan.Equivalence uses the tools introduced in the file Compatibility.lean. Doing so, the functor Idempotents.DoldKan.N of the equivalence is the composition of N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) (defined in FunctorN.lean) and the inverse of the equivalence ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ). The functor Idempotents.DoldKan.Γ of the equivalence is by definition the functor Γ₀ introduced in FunctorGamma.lean.

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

The functor N for the equivalence is obtained by composing N' : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) and the inverse of the equivalence ChainComplex C ℕ ≌ Karoubi (ChainComplex C ℕ).

Instances For

    The Dold-Kan equivalence for pseudoabelian categories given by the functors N and Γ. It is obtained by applying the results in Compatibility.lean to the equivalence Preadditive.DoldKan.Equivalence.

    Instances For
      theorem CategoryTheory.Idempotents.DoldKan.equivalence_inverse {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
      CategoryTheory.Idempotents.DoldKan.equivalence.inverse = CategoryTheory.Idempotents.DoldKan.Γ

      The natural isomorphism NΓ' satisfies the compatibility that is needed for the construction of our counit isomorphism η`

      The counit isomorphism induced by N₁Γ₀

      Instances For
        theorem CategoryTheory.Idempotents.DoldKan.equivalence_counitIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.Idempotents.DoldKan.equivalence.counitIso = CategoryTheory.Idempotents.DoldKan.η
        theorem CategoryTheory.Idempotents.DoldKan.equivalence_unitIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.Idempotents.DoldKan.equivalence.unitIso = CategoryTheory.Idempotents.DoldKan.ε