Documentation

Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive

The Dold-Kan equivalence for additive categories.

This file defines Preadditive.DoldKan.equivalence which is the equivalence of categories Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ).

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

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

The functor Karoubi (SimplicialObject C) ⥤ Karoubi (ChainComplex C ℕ) of the Dold-Kan equivalence for additive categories.

Equations
  • CategoryTheory.Preadditive.DoldKan.N = AlgebraicTopology.DoldKan.N₂
Instances For
    source
    def CategoryTheory.Preadditive.DoldKan.Γ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
    CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)) (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))

    The inverse functor Karoubi (ChainComplex C ℕ) ⥤ Karoubi (SimplicialObject C) of the Dold-Kan equivalence for additive categories.

    Equations
    • CategoryTheory.Preadditive.DoldKan.Γ = AlgebraicTopology.DoldKan.Γ₂
    Instances For
      source
      def CategoryTheory.Preadditive.DoldKan.equivalence {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
      CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C) ≌ CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)

      The Dold-Kan equivalence Karoubi (SimplicialObject C) ≌ Karoubi (ChainComplex C ℕ) for additive categories.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Preadditive.DoldKan.equivalence_functor {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.Preadditive.DoldKan.equivalence.functor = CategoryTheory.Preadditive.DoldKan.N
        source
        @[simp]
        theorem CategoryTheory.Preadditive.DoldKan.equivalence_unitIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.Preadditive.DoldKan.equivalence.unitIso = AlgebraicTopology.DoldKan.Γ₂N₂
        source
        @[simp]
        theorem CategoryTheory.Preadditive.DoldKan.equivalence_inverse {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.Preadditive.DoldKan.equivalence.inverse = CategoryTheory.Preadditive.DoldKan.Γ
        source
        @[simp]
        theorem CategoryTheory.Preadditive.DoldKan.equivalence_counitIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteCoproducts C] :
        CategoryTheory.Preadditive.DoldKan.equivalence.counitIso = AlgebraicTopology.DoldKan.N₂Γ₂