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 isomorphism (Γ₀.splitting K).nondegComplex ≅ K for all K : ChainComplex C ℕ.

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

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

    Equations
    Instances For
      @[irreducible]

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[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 : ) :
        (AlgebraicTopology.DoldKan.N₁Γ₀.hom.app K).f.f n = (AlgebraicTopology.DoldKan.Γ₀.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 : ) :
        (AlgebraicTopology.DoldKan.N₁Γ₀.inv.app K).f.f n = (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f 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.Idempotents.toKaroubi (ChainComplex C )).comp (AlgebraicTopology.DoldKan.Γ₂.comp AlgebraicTopology.DoldKan.N₂) AlgebraicTopology.DoldKan.Γ₀.comp AlgebraicTopology.DoldKan.N₁

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[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 ) :
          (AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.hom.app X).f = AlgebraicTopology.DoldKan.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 ) :
          (AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso.inv.app X).f = AlgebraicTopology.DoldKan.PInfty
          @[irreducible]

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

          Equations
          • One or more equations did not get rendered due to their size.
          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)