# Documentation

Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

# 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.)

@[simp]
theorem CategoryTheory.Idempotents.DoldKan.N_obj {C : Type u_1} [] :
CategoryTheory.Idempotents.DoldKan.N.obj X = ().inverse.obj (AlgebraicTopology.DoldKan.N₁.obj X)
@[simp]
theorem CategoryTheory.Idempotents.DoldKan.N_map_f {C : Type u_1} [] :
∀ {X Y : } (f : X Y) (i : ), HomologicalComplex.Hom.f (CategoryTheory.Idempotents.DoldKan.N.map f) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f (CategoryTheory.Functor.objObjPreimageIso () (AlgebraicTopology.DoldKan.N₁.obj X)).hom.f i) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f AlgebraicTopology.DoldKan.PInfty i) (CategoryTheory.CategoryStruct.comp (f.app ()) (HomologicalComplex.Hom.f (CategoryTheory.Functor.objObjPreimageIso () (AlgebraicTopology.DoldKan.N₁.obj Y)).inv.f i)))

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
@[simp]
theorem CategoryTheory.Idempotents.DoldKan.Γ_map_app {C : Type u_1} [] :
∀ {X Y : } (f : X Y) (Δ : ), (CategoryTheory.Idempotents.DoldKan.Γ.map f).app Δ = SimplicialObject.Splitting.desc () Δ fun A =>
@[simp]
theorem CategoryTheory.Idempotents.DoldKan.Γ_obj_map {C : Type u_1} [] (X : ) :
∀ {X Y : } (θ : X Y), (CategoryTheory.Idempotents.DoldKan.Γ.obj X).map θ =
@[simp]
theorem CategoryTheory.Idempotents.DoldKan.Γ_obj_obj {C : Type u_1} [] (X : ) (Δ : ) :
(CategoryTheory.Idempotents.DoldKan.Γ.obj X).obj Δ =

The functor Γ for the equivalence is Γ'.

Instances For
theorem CategoryTheory.Idempotents.DoldKan.hN₁ {C : Type u_1} [] :
theorem CategoryTheory.Idempotents.DoldKan.hΓ₀ {C : Type u_1} [] :
CategoryTheory.Functor.comp ().functor CategoryTheory.Preadditive.DoldKan.equivalence.inverse = CategoryTheory.Functor.comp CategoryTheory.Idempotents.DoldKan.Γ

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_functor {C : Type u_1} [] :
CategoryTheory.Idempotents.DoldKan.equivalence.functor = CategoryTheory.Idempotents.DoldKan.N
theorem CategoryTheory.Idempotents.DoldKan.equivalence_inverse {C : Type u_1} [] :
CategoryTheory.Idempotents.DoldKan.equivalence.inverse = CategoryTheory.Idempotents.DoldKan.Γ
theorem CategoryTheory.Idempotents.DoldKan. {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Compatibility.τ₀ = AlgebraicTopology.DoldKan.Compatibility.τ₁ (CategoryTheory.eqToIso (_ : CategoryTheory.Functor.comp CategoryTheory.Preadditive.DoldKan.equivalence.functor = AlgebraicTopology.DoldKan.N₁)) (CategoryTheory.eqToIso (_ : CategoryTheory.Functor.comp ().functor CategoryTheory.Preadditive.DoldKan.equivalence.inverse = CategoryTheory.Functor.comp CategoryTheory.Idempotents.DoldKan.Γ )) AlgebraicTopology.DoldKan.N₁Γ₀

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

@[simp]
theorem CategoryTheory.Idempotents.DoldKan.η_inv_app_f {C : Type u_1} [] (X : ) (i : ) :
HomologicalComplex.Hom.f (CategoryTheory.Idempotents.DoldKan.η.inv.app X) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f (().unitIso.hom.app X) i) (HomologicalComplex.Hom.f (().inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app X)) i)
@[simp]
theorem CategoryTheory.Idempotents.DoldKan.η_hom_app_f {C : Type u_1} [] (X : ) (i : ) :
HomologicalComplex.Hom.f (CategoryTheory.Idempotents.DoldKan.η.hom.app X) i = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f (().inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app X)) i) (HomologicalComplex.Hom.f (().unitIso.inv.app X) i)
def CategoryTheory.Idempotents.DoldKan.η {C : Type u_1} [] :
CategoryTheory.Functor.comp CategoryTheory.Idempotents.DoldKan.Γ CategoryTheory.Idempotents.DoldKan.N

The counit isomorphism induced by N₁Γ₀

Instances For
theorem CategoryTheory.Idempotents.DoldKan.equivalence_counitIso {C : Type u_1} [] :
CategoryTheory.Idempotents.DoldKan.equivalence.counitIso = CategoryTheory.Idempotents.DoldKan.η
theorem CategoryTheory.Idempotents.DoldKan. {C : Type u_1} [] :
AlgebraicTopology.DoldKan.Compatibility.υ (CategoryTheory.eqToIso (_ : CategoryTheory.Functor.comp CategoryTheory.Preadditive.DoldKan.equivalence.functor = AlgebraicTopology.DoldKan.N₁)) = AlgebraicTopology.DoldKan.Γ₂N₁
def CategoryTheory.Idempotents.DoldKan.ε {C : Type u_1} [] :
CategoryTheory.Functor.comp CategoryTheory.Idempotents.DoldKan.N CategoryTheory.Idempotents.DoldKan.Γ

The unit isomorphism induced by Γ₂N₁`.

Instances For
theorem CategoryTheory.Idempotents.DoldKan.equivalence_unitIso {C : Type u_1} [] :
CategoryTheory.Idempotents.DoldKan.equivalence.unitIso = CategoryTheory.Idempotents.DoldKan.ε