# Documentation

Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

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

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.

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 Δ

Instances For

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.

Instances For
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀' {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' Δ) (hi : ) :
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 : ) :
@[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 : 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.

Instances For
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc {C : Type u_1} [] (K : ) {Δ : } {Δ' : } {θ : Δ Δ'} {Δ'' : SimplexCategory} {e : Δ'.unop Δ''} {i : Δ'' A.fst.unop} (fac : ) {Z : C} (h : ) :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀ {C : Type u_1} [] (K : ) {Δ : } {Δ' : } {θ : Δ Δ'} {Δ'' : SimplexCategory} {e : Δ'.unop Δ''} {i : Δ'' A.fst.unop} (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.

Instances For

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

Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') {Δ'' : SimplexCategory} {e : Δ'.unop Δ''} {i : Δ'' A.fst.unop} (fac : ) {Z : C} (h : ().obj Δ' Z) :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand {C : Type u_1} [] (K : ) {Δ : } {Δ' : } (θ : Δ Δ') {Δ'' : SimplexCategory} {e : Δ'.unop Δ''} {i : Δ'' A.fst.unop} (fac : ) :
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 : ) {Δ : } {Δ' : } (θ : Δ Δ') :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (i : Δ' Δ) {Z : C} (h : ().obj () Z) :
theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id_assoc {C : Type u_1} [] (K : ) {Δ : SimplexCategory} {Δ' : SimplexCategory} (e : Δ' Δ) {Z : C} (h : ().obj () Z) :
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀.map_app {C : Type u_1} [] {K : } {K' : } (f : K K') (Δ : ) :
().app Δ =
def AlgebraicTopology.DoldKan.Γ₀.map {C : Type u_1} [] {K : } {K' : } (f : K K') :

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

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 : ) :
SimplicialObject.Split.Hom.f (AlgebraicTopology.DoldKan.Γ₀'.map 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.

Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀_map_app {C : Type u_1} [] :
∀ {X Y : } (f : X Y) (Δ : ), (AlgebraicTopology.DoldKan.Γ₀.map f).app Δ = SimplicialObject.Splitting.desc () Δ fun A =>
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀_obj_obj {C : Type u_1} [] (X : ) (Δ : ) :
(AlgebraicTopology.DoldKan.Γ₀.obj X).obj Δ =
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₀_obj_map {C : Type u_1} [] (X : ) :
∀ {X Y : } (θ : X Y), (AlgebraicTopology.DoldKan.Γ₀.obj X).map θ =

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.

Instances For
@[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_p_app {C : Type u_1} [] (Δ : ) :
(AlgebraicTopology.DoldKan.Γ₂.obj P).p.app Δ = SimplicialObject.Splitting.desc () Δ fun A => CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f P.p (SimplexCategory.len A.fst.unop)) ()
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂_obj_X_obj {C : Type u_1} [] (Δ : ) :
(AlgebraicTopology.DoldKan.Γ₂.obj P).X.obj Δ =
@[simp]
theorem AlgebraicTopology.DoldKan.Γ₂_map_f_app {C : Type u_1} [] :
∀ {X Y : } (f : X Y) (Δ : ), (AlgebraicTopology.DoldKan.Γ₂.map f).f.app Δ = SimplicialObject.Splitting.desc () Δ fun A => CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f.f (SimplexCategory.len A.fst.unop)) ()

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

Instances For