The counit isomorphism of the Dold-Kan equivalence

The purpose of this file is to construct natural isomorphisms N₁Γ₀ : Γ₀ ⋙ N₁ ≅ toKaroubi (ChainComplex C ℕ) and N₂Γ₂ : Γ₂ ⋙ N₂ ≅ 𝟭 (Karoubi (ChainComplex C ℕ)).

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

noncomputable def AlgebraicTopology.DoldKan.Γ₀NondegComplexIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) : (Γ₀.splitting K).nondegComplex ≅ K

The isomorphism (Γ₀.splitting K).nondegComplex ≅ K for all K : ChainComplex C ℕ.

@[simp]

theorem AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (i : ℕ) : (Γ₀NondegComplexIso K).inv.f i = CategoryTheory.CategoryStruct.id ((Γ₀.splitting K).N i)

@[simp]

theorem AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (i : ℕ) : (Γ₀NondegComplexIso K).hom.f i = CategoryTheory.CategoryStruct.id ((Γ₀.splitting K).N i)

noncomputable def AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : Γ₀'.comp SimplicialObject.Split.nondegComplexFunctor ≅ CategoryTheory.Functor.id (ChainComplex C ℕ)

The natural isomorphism (Γ₀.splitting K).nondegComplex ≅ K for K : ChainComplex C ℕ.

noncomputable def AlgebraicTopology.DoldKan.N₁Γ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : Γ₀.comp N₁ ≅ CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)

The natural isomorphism Γ₀ ⋙ N₁ ≅ toKaroubi (ChainComplex C ℕ).

theorem AlgebraicTopology.DoldKan.N₁Γ₀_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) : N₁Γ₀.app K = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.symm ≪≫ (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)

theorem AlgebraicTopology.DoldKan.N₁Γ₀_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) : N₁Γ₀.hom.app K = CategoryTheory.CategoryStruct.comp (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom)

theorem AlgebraicTopology.DoldKan.N₁Γ₀_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) : N₁Γ₀.inv.app K = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv) (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom

@[simp]

theorem AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (n : ℕ) : (N₁Γ₀.hom.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.inv.f.f n

@[simp]

theorem AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) (n : ℕ) : (N₁Γ₀.inv.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n

noncomputable def AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).comp (Γ₂.comp N₂) ≅ Γ₀.comp N₁

Compatibility isomorphism between toKaroubi _ ⋙ Γ₂ ⋙ N₂ and Γ₀ ⋙ N₁ which are functors ChainComplex C ℕ ⥤ Karoubi (ChainComplex C ℕ).

@[simp]

theorem AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) : (N₂Γ₂ToKaroubiIso.hom.app X).f = PInfty

@[simp]

theorem AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : ChainComplex C ℕ) : (N₂Γ₂ToKaroubiIso.inv.app X).f = PInfty

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

The counit isomorphism of the Dold-Kan equivalence for additive categories.

@[simp]

theorem AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (X : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)) (n : ℕ) : (N₂Γ₂.inv.app X).f.f n = CategoryTheory.CategoryStruct.comp (X.p.f n) (((Γ₀.splitting X.X).cofan (Opposite.op (SimplexCategory.mk n))).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n))))

theorem AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).whiskerLeft N₂Γ₂.hom = CategoryTheory.CategoryStruct.comp N₂Γ₂ToKaroubiIso.hom N₁Γ₀.hom

theorem AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) : N₂Γ₂.hom.app ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).obj K) = CategoryTheory.CategoryStruct.comp (N₂Γ₂ToKaroubiIso.hom.app K) (N₁Γ₀.hom.app K)