# Construction of the inverse functor of the Dold-Kan equivalence #

In this file, we construct the functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C which shall be the inverse functor of the Dold-Kan equivalence in the case of abelian categories, and more generally pseudoabelian categories.

By definition, when K is a chain_complex, Γ₀.obj K is a simplicial object which sends Δ : SimplexCategoryᵒᵖ to a certain coproduct indexed by the set Splitting.IndexSet Δ whose elements consists of epimorphisms e : Δ.unop ⟶ Δ'.unop (with Δ' : SimplexCategoryᵒᵖ); the summand attached to such an e is K.X Δ'.unop.len. By construction, Γ₀.obj K is a split simplicial object whose splitting is Γ₀.splitting K.

We also construct Γ₂ : Karoubi (ChainComplex C ℕ) ⥤ Karoubi (SimplicialObject C) which shall be an equivalence for any additive category C.

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

Isδ₀ i is a simple condition used to check whether a monomorphism i in SimplexCategory identifies to the coface map δ 0.

Equations
• = (Δ.len = Δ'.len + 1 )
Instances For
def AlgebraicTopology.DoldKan.Γ₀.Obj.summand {C : Type u_1} [] (K : ) (Δ : ) :
C

In the definition of (Γ₀.obj K).obj Δ as a direct sum indexed by A : Splitting.IndexSet Δ, the summand summand K Δ A is K.X A.1.len.

Equations
Instances For
def AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂ {C : Type u_1} [] (K : ) (Δ : ) :
C

The functor Γ₀ sends a chain complex K to the simplicial object which sends Δ to the direct sum of the objects summand K Δ A for all A : Splitting.IndexSet Δ

Equations
Instances For
def AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono {C : Type u_1} [] (K : ) {Δ' : SimplexCategory} {Δ : SimplexCategory} (i : Δ' Δ) :
K.X Δ.len K.X Δ'.len

A monomorphism i : Δ' ⟶ Δ induces a morphism K.X Δ.len ⟶ K.X Δ'.len which is the identity if Δ = Δ', the differential on the complex K if i = δ 0, and zero otherwise.

Equations
• = if h : Δ = Δ' then else if h : then K.d Δ.len Δ'.len else 0
Instances For
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀' {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' Δ) (hi : ) :
= K.d Δ.len Δ'.len
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀ {C : Type u_1} [] (K : ) {n : } :
= K.d (n + 1) n
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' Δ) (h₁ : Δ Δ') (h₂ : ) :
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc {C : Type u_1} [] {K : } {K' : } (f : K K') {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ Δ') {Z : C} (h : K'.X Δ.len Z) :
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality {C : Type u_1} [] {K : } {K' : } (f : K K') {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ Δ') :
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} {Δ'' : SimplexCategory} (i' : Δ'' Δ') (i : Δ' Δ) [] {Z : C} (h : K.X Δ''.len Z) :
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} {Δ'' : SimplexCategory} (i' : Δ'' Δ') (i : Δ' Δ) [] :
def AlgebraicTopology.DoldKan.Γ₀.Obj.map {C : Type u_1} [] (K : ) {Δ' : } {Δ : } (θ : Δ Δ') :

The simplicial morphism on the simplicial object Γ₀.obj K induced by a morphism Δ' → Δ in SimplexCategory is defined on each summand associated to an A : Splitting.IndexSet Δ in terms of the epi-mono factorisation of θ ≫ A.e.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc {C : Type u_1} [] (K : ) {Δ : } {Δ' : } {θ : Δ Δ'} {Δ'' : SimplexCategory} {e : Δ''} {i : Δ'' Opposite.unop A.fst} (fac : ) {Z : C} (h : ) :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀ {C : Type u_1} [] (K : ) {Δ : } {Δ' : } {θ : Δ Δ'} {Δ'' : SimplexCategory} {e : Δ''} {i : Δ'' Opposite.unop A.fst} (fac : ) :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') {Z : C} (h : ) :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀' {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') :
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.obj_map {C : Type u_1} [] (K : ) :
∀ {X Y : } (θ : X Y),
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.obj_obj {C : Type u_1} [] (K : ) (Δ : ) :

The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, on objects.

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

By construction, the simplicial Γ₀.obj K is equipped with a splitting.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') {Δ'' : SimplexCategory} {e : Δ''} {i : Δ'' Opposite.unop A.fst} (fac : ) {Z : C} (h : .obj Δ' Z) :
CategoryTheory.CategoryStruct.comp ((.cofan Δ).inj A) () =
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') {Δ'' : SimplexCategory} {e : Δ''} {i : Δ'' Opposite.unop A.fst} (fac : ) :
CategoryTheory.CategoryStruct.comp ((.cofan Δ).inj A) (.map θ) =
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') {Z : C} (h : .obj Δ' Z) :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand' {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') :
CategoryTheory.CategoryStruct.comp ((.cofan Δ).inj A) (.map θ) = CategoryTheory.CategoryStruct.comp ((.cofan Δ').inj (A.pull θ))
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' Δ) :
CategoryTheory.CategoryStruct.comp ((.cofan ()).inj ) (.map i.op) =
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (e : Δ' Δ) {Z : C} (h : .obj () Z) :
CategoryTheory.CategoryStruct.comp ((.cofan ()).inj ) () =
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (e : Δ' Δ) :
CategoryTheory.CategoryStruct.comp ((.cofan ()).inj ) (.map e.op) = (.cofan ()).inj
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.map_app {C : Type u_1} [] {K : } {K' : } (f : K K') (Δ : ) :
.app Δ = Δ fun (A : ) => CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len) ((.cofan Δ).inj A)
def AlgebraicTopology.DoldKan.Γ₀.map {C : Type u_1} [] {K : } {K' : } (f : K K') :

The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, on morphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀'_map_F {C : Type u_1} [] {K : } {K' : } (f : K K') :
(AlgebraicTopology.DoldKan.Γ₀'.map f).F =
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀'_map_f {C : Type u_1} [] {K : } {K' : } (f : K K') (i : ) :
(AlgebraicTopology.DoldKan.Γ₀'.map f).f i = f.f i
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀'_obj {C : Type u_1} [] (K : ) :
AlgebraicTopology.DoldKan.Γ₀'.obj K =

The functor Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject.Split C that induces Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, which shall be the inverse functor of the Dold-Kan equivalence for abelian or pseudo-abelian categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀_obj_map {C : Type u_1} [] (X : ) :
∀ {X_1 Y : } (θ : X_1 Y), (AlgebraicTopology.DoldKan.Γ₀.obj X).map θ =
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀_obj_obj {C : Type u_1} [] (X : ) (Δ : ) :
(AlgebraicTopology.DoldKan.Γ₀.obj X).obj Δ =
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀_map_app {C : Type u_1} [] :
∀ {X Y : } (f : X Y) (Δ : ), (AlgebraicTopology.DoldKan.Γ₀.map f).app Δ = Δ fun (A : ) => CategoryTheory.CategoryStruct.comp (f.f (Opposite.unop A.fst).len) ((.cofan Δ).inj A)

The functor Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C, which is the inverse functor of the Dold-Kan equivalence when C is an abelian category, or more generally a pseudoabelian category.

Equations
• AlgebraicTopology.DoldKan.Γ₀ = AlgebraicTopology.DoldKan.Γ₀'.comp
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂_map_f_app {C : Type u_1} [] :
∀ {X Y : } (f : X Y) (Δ : ), (AlgebraicTopology.DoldKan.Γ₂.map f).f.app Δ = .desc Δ fun (A : ) => CategoryTheory.CategoryStruct.comp (f.f.f (Opposite.unop A.fst).len) ((.cofan Δ).inj A)
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂_obj_X_map {C : Type u_1} [] :
∀ {X Y : } (θ : X Y), (AlgebraicTopology.DoldKan.Γ₂.obj P).X.map θ =
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂_obj_X_obj {C : Type u_1} [] (Δ : ) :
(AlgebraicTopology.DoldKan.Γ₂.obj P).X.obj Δ =
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂_obj_p_app {C : Type u_1} [] (Δ : ) :
(AlgebraicTopology.DoldKan.Γ₂.obj P).p.app Δ = .desc Δ fun (A : ) => CategoryTheory.CategoryStruct.comp (P.p.f (Opposite.unop A.fst).len) ((.cofan Δ).inj A)

The extension of Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C on the idempotent completions. It shall be an equivalence of categories for any additive category C.

Equations
• AlgebraicTopology.DoldKan.Γ₂ = AlgebraicTopology.DoldKan.Γ₀
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc {C : Type u_1} [] (K : ) {n : } {Z : C} :
CategoryTheory.CategoryStruct.comp ((.cofan ).inj ) (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) = CategoryTheory.CategoryStruct.comp ((.cofan ).inj ) h
@[simp]
theorem AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self {C : Type u_1} [] (K : ) {n : } :
CategoryTheory.CategoryStruct.comp ((.cofan ).inj ) (AlgebraicTopology.DoldKan.PInfty.f n) = (.cofan ).inj