# mathlib3documentation

algebraic_topology.dold_kan.functor_gamma

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we construct the functor Γ₀ : chain_complex C ℕ ⥤ simplicial_object 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 Δ : simplex_categoryᵒᵖ to a certain coproduct indexed by the set splitting.index_set Δ whose elements consists of epimorphisms e : Δ.unop ⟶ Δ'.unop (with Δ' : simplex_categoryᵒᵖ); 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 (chain_complex C ℕ) ⥤ karoubi (simplicial_object 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.)

@[nolint]
def algebraic_topology.dold_kan.is_δ₀ {Δ Δ' : simplex_category} (i : Δ' Δ)  :
Prop

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

Equations

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

Equations
noncomputable def algebraic_topology.dold_kan.Γ₀.obj.obj₂ {C : Type u_1} (K : ) (Δ : simplex_categoryᵒᵖ)  :
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.index_set Δ

Equations
noncomputable def algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono {C : Type u_1} (K : ) {Δ' Δ : simplex_category} (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
• = dite = Δ') (λ (h : Δ = Δ'), (λ (h : ¬Δ = Δ'), (λ (h : , K.d Δ.len Δ'.len) (λ (h : , 0))
theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_eq_zero {C : Type u_1} (K : ) {Δ' Δ : simplex_category} (i : Δ' Δ) (h₁ : Δ Δ')  :
@[simp]
theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_naturality {C : Type u_1} {K K' : } (f : K K') {Δ' Δ : simplex_category} (i : Δ' Δ)  :
@[simp]
theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_naturality_assoc {C : Type u_1} {K K' : } (f : K K') {Δ' Δ : simplex_category} (i : Δ' Δ) {X' : C} (f' : K'.X Δ'.len X') :
=
@[simp]
theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_comp_assoc {C : Type u_1} (K : ) {Δ'' Δ' Δ : simplex_category} (i' : Δ'' Δ') (i : Δ' Δ) {X' : C} (f' : K.X Δ''.len X') :
@[simp]
theorem algebraic_topology.dold_kan.Γ₀.obj.termwise.map_mono_comp {C : Type u_1} (K : ) {Δ'' Δ' Δ : simplex_category} (i' : Δ'' Δ') (i : Δ' Δ)  :
noncomputable def algebraic_topology.dold_kan.Γ₀.obj.map {C : Type u_1} (K : ) {Δ' Δ : simplex_categoryᵒᵖ} (θ : Δ Δ') :

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

Equations
theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀_assoc {C : Type u_1} (K : ) {Δ Δ' : simplex_categoryᵒᵖ} {θ : Δ Δ'} {Δ'' : simplex_category} {e : Δ''} {i : Δ'' } (fac : e i = θ.unop A.e) {X' : C} (f' : X') :
theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀ {C : Type u_1} (K : ) {Δ Δ' : simplex_categoryᵒᵖ} {θ : Δ Δ'} {Δ'' : simplex_category} {e : Δ''} {i : Δ'' } (fac : e i = θ.unop A.e) :
theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand₀'_assoc {C : Type u_1} (K : ) {Δ Δ' : simplex_categoryᵒᵖ} (θ : Δ Δ') {X' : C} (f' : X') :
@[simp]
theorem algebraic_topology.dold_kan.Γ₀.obj_map {C : Type u_1} (K : ) (Δ Δ' : simplex_categoryᵒᵖ) (θ : Δ Δ') :
noncomputable def algebraic_topology.dold_kan.Γ₀.obj {C : Type u_1} (K : ) :

The functor Γ₀ : chain_complex C ℕ ⥤ simplicial_object C, on objects.

Equations
@[simp]

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand {C : Type u_1} (K : ) {Δ Δ' : simplex_categoryᵒᵖ} (θ : Δ Δ') {Δ'' : simplex_category} {e : Δ''} {i : Δ'' } (fac : e i = θ.unop A.e) :
theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand_assoc {C : Type u_1} (K : ) {Δ Δ' : simplex_categoryᵒᵖ} (θ : Δ Δ') {Δ'' : simplex_category} {e : Δ''} {i : Δ'' } (fac : e i = θ.unop A.e) {X' : C} (f' : X') :
theorem algebraic_topology.dold_kan.Γ₀.obj.map_on_summand'_assoc {C : Type u_1} (K : ) {Δ Δ' : simplex_categoryᵒᵖ} (θ : Δ Δ') {X' : C} (f' : X') :
theorem algebraic_topology.dold_kan.Γ₀.obj.map_mono_on_summand_id_assoc {C : Type u_1} (K : ) {Δ Δ' : simplex_category} (i : Δ' Δ) {X' : C} (f' : X') :
theorem algebraic_topology.dold_kan.Γ₀.obj.map_epi_on_summand_id_assoc {C : Type u_1} (K : ) {Δ Δ' : simplex_category} (e : Δ' Δ) {X' : C} (f' : X') :
noncomputable def algebraic_topology.dold_kan.Γ₀.map {C : Type u_1} {K K' : } (f : K K') :

The functor Γ₀ : chain_complex C ℕ ⥤ simplicial_object C, on morphisms.

Equations
@[simp]
theorem algebraic_topology.dold_kan.Γ₀.map_app {C : Type u_1} {K K' : } (f : K K') (Δ : simplex_categoryᵒᵖ) :
= (λ (A : , f.f (opposite.unop A.fst).len
@[simp]
theorem algebraic_topology.dold_kan.Γ₀'_map_F {C : Type u_1} (K K' : ) (f : K K') :
@[simp]
noncomputable def algebraic_topology.dold_kan.Γ₀' {C : Type u_1}  :

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.Γ₀'_map_f {C : Type u_1} (K K' : ) (f : K K') (i : ) :
= f.f i
@[simp]
theorem algebraic_topology.dold_kan.Γ₀_obj_map {C : Type u_1} (X : ) (Δ Δ' : simplex_categoryᵒᵖ) (θ : Δ Δ') :
@[simp]
@[simp]
theorem algebraic_topology.dold_kan.Γ₀_map_app {C : Type u_1} (_x _x_1 : ) (f : _x _x_1) (Δ : simplex_categoryᵒᵖ) :
= (λ (A : , f.f (opposite.unop A.fst).len
noncomputable def algebraic_topology.dold_kan.Γ₀ {C : Type u_1}  :

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.Γ₂_map_f_app {C : Type u_1} (f : P Q) (Δ : simplex_categoryᵒᵖ) :
= (λ (A : , f.f.f (opposite.unop A.fst).len

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

Equations
@[simp]
theorem algebraic_topology.dold_kan.Γ₂_obj_X_map {C : Type u_1} (Δ Δ' : simplex_categoryᵒᵖ) (θ : Δ Δ') :
@[simp]
@[simp]
@[simp]