Documentation

Mathlib.AlgebraicTopology.DoldKan.GammaCompN

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

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

Instances For
    @[irreducible]

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

    Instances For
      @[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]

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

      Instances For
        @[irreducible]

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

        Instances For
          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)