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.)
def
CategoryTheory.Preadditive.DoldKan.N
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive 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
def
CategoryTheory.Preadditive.DoldKan.Γ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts 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
@[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
@[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.Γ
@[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₂
@[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₂Γ₂
def
CategoryTheory.Preadditive.DoldKan.equivalence
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteCoproducts 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.