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

noncomputable def CategoryTheory.Idempotents.DoldKan.N {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : Functor (SimplicialObject C) (ChainComplex C ℕ)

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

Equations

• CategoryTheory.Idempotents.DoldKan.N = AlgebraicTopology.DoldKan.N₁.comp (CategoryTheory.Idempotents.toKaroubiEquivalence (ChainComplex C ℕ)).inverse

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.N_obj {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] (X : SimplicialObject C) : N.obj X = (toKaroubiEquivalence (ChainComplex C ℕ)).inverse.obj (AlgebraicTopology.DoldKan.N₁.obj X)

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.N_map {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] {X✝ Y✝ : SimplicialObject C} (f : X✝ ⟶ Y✝) : N.map f = (toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁.map f)

noncomputable def CategoryTheory.Idempotents.DoldKan.Γ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : Functor (ChainComplex C ℕ) (SimplicialObject C)

The functor Γ for the equivalence is Γ'.

Equations

• CategoryTheory.Idempotents.DoldKan.Γ = AlgebraicTopology.DoldKan.Γ₀

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.Γ_obj_map {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) {X✝ Y✝ : SimplexCategoryᵒᵖ} (θ : X✝ ⟶ Y✝) : (Γ.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.Γ_map_app {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] {X✝ Y✝ : ChainComplex C ℕ} (f : X✝ ⟶ Y✝) (Δ : SimplexCategoryᵒᵖ) : (Γ.map f).app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting X✝).desc Δ fun (A : SimplicialObject.Splitting.IndexSet Δ) => CategoryStruct.comp (f.f (Opposite.unop A.fst).len) (((AlgebraicTopology.DoldKan.Γ₀.splitting Y✝).cofan Δ).inj A)

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.Γ_obj_obj {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ) : (Γ.obj X).obj Δ = AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ X Δ

noncomputable def CategoryTheory.Idempotents.DoldKan.isoN₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : (toKaroubiEquivalence (SimplicialObject C)).functor.comp Preadditive.DoldKan.equivalence.functor ≅ AlgebraicTopology.DoldKan.N₁

A reformulation of the isomorphism toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁

Equations

• CategoryTheory.Idempotents.DoldKan.isoN₁ = AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] (X : SimplicialObject C) : (isoN₁.hom.app X).f = AlgebraicTopology.DoldKan.PInfty

noncomputable def CategoryTheory.Idempotents.DoldKan.isoΓ₀ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : (toKaroubiEquivalence (ChainComplex C ℕ)).functor.comp Preadditive.DoldKan.equivalence.inverse ≅ Γ.comp (toKaroubiEquivalence (SimplicialObject C)).functor

A reformulation of the canonical isomorphism toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ≅ Γ ⋙ toKaroubi (SimplicialObject C).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) : (AlgebraicTopology.DoldKan.N₂.map (isoΓ₀.hom.app X)).f = AlgebraicTopology.DoldKan.PInfty

noncomputable def CategoryTheory.Idempotents.DoldKan.equivalence {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : SimplicialObject C ≌ ChainComplex C ℕ

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.

Equations

• CategoryTheory.Idempotents.DoldKan.equivalence = AlgebraicTopology.DoldKan.Compatibility.equivalence CategoryTheory.Idempotents.DoldKan.isoN₁ CategoryTheory.Idempotents.DoldKan.isoΓ₀

theorem CategoryTheory.Idempotents.DoldKan.equivalence_functor {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : equivalence.functor = N

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

theorem CategoryTheory.Idempotents.DoldKan.hη {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : AlgebraicTopology.DoldKan.Compatibility.τ₀ = AlgebraicTopology.DoldKan.Compatibility.τ₁ isoN₁ isoΓ₀ AlgebraicTopology.DoldKan.N₁Γ₀

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

noncomputable def CategoryTheory.Idempotents.DoldKan.η {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : Γ.comp N ≅ Functor.id (ChainComplex C ℕ)

The counit isomorphism induced by N₁Γ₀

Equations

• CategoryTheory.Idempotents.DoldKan.η = AlgebraicTopology.DoldKan.Compatibility.equivalenceCounitIso AlgebraicTopology.DoldKan.N₁Γ₀

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.η_inv_app_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) (i : ℕ) : (η.inv.app X).f i = CategoryStruct.comp (((toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.hom.app X).f i) (((toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app X)).f i)

@[simp]

theorem CategoryTheory.Idempotents.DoldKan.η_hom_app_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) (i : ℕ) : (η.hom.app X).f i = CategoryStruct.comp (((toKaroubiEquivalence (ChainComplex C ℕ)).inverse.map (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app X)).f i) (((toKaroubiEquivalence (ChainComplex C ℕ)).unitIso.inv.app X).f i)

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

theorem CategoryTheory.Idempotents.DoldKan.hε {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : AlgebraicTopology.DoldKan.Compatibility.υ isoN₁ = AlgebraicTopology.DoldKan.Γ₂N₁

noncomputable def CategoryTheory.Idempotents.DoldKan.ε {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] [IsIdempotentComplete C] [Limits.HasFiniteCoproducts C] : Functor.id (SimplicialObject C) ≅ N.comp Γ

The unit isomorphism induced by Γ₂N₁.

Equations

• CategoryTheory.Idempotents.DoldKan.ε = AlgebraicTopology.DoldKan.Compatibility.equivalenceUnitIso CategoryTheory.Idempotents.DoldKan.isoΓ₀ AlgebraicTopology.DoldKan.Γ₂N₁

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