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

@[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 : ℕ) : HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).hom i = CategoryTheory.CategoryStruct.id (SimplicialObject.Splitting.N (AlgebraicTopology.DoldKan.Γ₀.splitting K) i)

@[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 : ℕ) : HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).inv i = CategoryTheory.CategoryStruct.id (SimplicialObject.Splitting.N (AlgebraicTopology.DoldKan.Γ₀.splitting K) i)

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 ℕ) : SimplicialObject.Splitting.nondegComplex (AlgebraicTopology.DoldKan.Γ₀.splitting K) ≅ K

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

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

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

@[irreducible]

def AlgebraicTopology.DoldKan.N₁Γ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.Γ₀ AlgebraicTopology.DoldKan.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 ℕ) : AlgebraicTopology.DoldKan.N₁Γ₀.app K = (SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ (AlgebraicTopology.DoldKan.Γ₀.splitting K)).symm ≪≫ (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).mapIso (AlgebraicTopology.DoldKan.Γ₀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 ℕ) : AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K = CategoryTheory.CategoryStruct.comp (SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ (AlgebraicTopology.DoldKan.Γ₀.splitting K)).inv ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map (AlgebraicTopology.DoldKan.Γ₀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 ℕ) : AlgebraicTopology.DoldKan.N₁Γ₀.inv.app K = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).inv) (SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ (AlgebraicTopology.DoldKan.Γ₀.splitting K)).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 : ℕ) : HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K).f n = HomologicalComplex.Hom.f (SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ (AlgebraicTopology.DoldKan.Γ₀.splitting K)).inv.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 : ℕ) : HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app K).f n = HomologicalComplex.Hom.f (SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁ (AlgebraicTopology.DoldKan.Γ₀.splitting K)).hom.f n

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

@[simp]

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

@[simp]

theorem AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.inv = CategoryTheory.eqToHom (_ : CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.Γ₀ AlgebraicTopology.DoldKan.N₁ = CategoryTheory.Functor.comp (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) (CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.Γ₂ AlgebraicTopology.DoldKan.N₂))

@[irreducible]

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

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

@[irreducible]

def AlgebraicTopology.DoldKan.N₂Γ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Functor.comp AlgebraicTopology.DoldKan.Γ₂ AlgebraicTopology.DoldKan.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 : ℕ) : HomologicalComplex.Hom.f (AlgebraicTopology.DoldKan.N₂Γ₂.inv.app X).f n = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f X.p n) (SimplicialObject.Splitting.ιSummand (AlgebraicTopology.DoldKan.Γ₀.splitting X.X) (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.whiskerLeft (CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)) AlgebraicTopology.DoldKan.N₂Γ₂.hom = CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom AlgebraicTopology.DoldKan.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 ℕ) : AlgebraicTopology.DoldKan.N₂Γ₂.hom.app ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).obj K) = CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom.app K) (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K)