mathlib3 documentation

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]

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

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

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

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

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