# mathlib3documentation

algebraic_topology.dold_kan.decomposition

# Decomposition of the Q endomorphisms #

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

In this file, we obtain a lemma decomposition_Q which expresses explicitly the projection (Q q).f (n+1) : X _[n+1] ⟶ X _[n+1] (X : simplicial_object C with C a preadditive category) as a sum of terms which are postcompositions with degeneracies.

(TODO @joelriou: when C is abelian, define the degenerate subcomplex of the alternating face map complex of X and show that it is a complement to the normalized Moore complex.)

Then, we introduce an ad hoc structure morph_components X n Z which can be used in order to define morphisms X _[n+1] ⟶ Z using the decomposition provided by decomposition_Q. This shall play a critical role in the proof that the functor N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)) reflects isomorphisms.

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

theorem algebraic_topology.dold_kan.decomposition_Q {C : Type u_1} (n q : ) :
(n + 1) = (finset.filter (λ (i : fin (n + 1)), i < q) finset.univ).sum (λ (i : fin (n + 1)), (n + 1) X.δ (fin.rev i).succ X.σ (fin.rev i))

In each positive degree, this lemma decomposes the idempotent endomorphism Q q as a sum of morphisms which are postcompositions with suitable degeneracies. As Q q is the complement projection to P q, this implies that in the case of simplicial abelian groups, any $(n+1)$-simplex $x$ can be decomposed as $x = x' + \sum (i=0}^{q-1} σ_{n-i}(y_i)$ where $x'$ is in the image of P q and the $y_i$ are in degree $n$.

theorem algebraic_topology.dold_kan.morph_components.ext {C : Type u_1} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.preadditive C} {n : } {Z : C} (x y : Z) (h : x.a = y.a) (h_1 : x.b = y.b) :
x = y
@[nolint, ext]
structure algebraic_topology.dold_kan.morph_components {C : Type u_1} (n : ) (Z : C) :
Type u_2

The structure morph_components is an ad hoc structure that is used in the proof that N₁ : simplicial_object C ⥤ karoubi (chain_complex C ℕ)) reflects isomorphisms. The fields are the data that are needed in order to construct a morphism X _[n+1] ⟶ Z (see φ) using the decomposition of the identity given by decomposition_Q n (n+1).

Instances for algebraic_topology.dold_kan.morph_components
• algebraic_topology.dold_kan.morph_components.has_sizeof_inst
theorem algebraic_topology.dold_kan.morph_components.ext_iff {C : Type u_1} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.preadditive C} {n : } {Z : C} (x y : Z) :
x = y x.a = y.a x.b = y.b
noncomputable def algebraic_topology.dold_kan.morph_components.φ {C : Type u_1} {n : } {Z : C}  :

The morphism X _[n+1] ⟶ Z associated to f : morph_components X n Z.

Equations
@[simp]
theorem algebraic_topology.dold_kan.morph_components.id_b {C : Type u_1} (n : ) (i : fin (n + 1)) :
= X.σ i
noncomputable def algebraic_topology.dold_kan.morph_components.id {C : Type u_1} (n : ) :

the canonical morph_components whose associated morphism is the identity (see F_id) thanks to decomposition_Q n (n+1)

Equations
@[simp]
theorem algebraic_topology.dold_kan.morph_components.post_comp_b {C : Type u_1} {n : } {Z Z' : C} (h : Z Z') (i : fin (n + 1)) :
(f.post_comp h).b i = f.b i h
@[simp]
theorem algebraic_topology.dold_kan.morph_components.post_comp_a {C : Type u_1} {n : } {Z Z' : C} (h : Z Z') :
(f.post_comp h).a = f.a h
def algebraic_topology.dold_kan.morph_components.post_comp {C : Type u_1} {n : } {Z Z' : C} (h : Z Z') :

A morph_components can be postcomposed with a morphism.

Equations
@[simp]
theorem algebraic_topology.dold_kan.morph_components.post_comp_φ {C : Type u_1} {n : } {Z Z' : C} (h : Z Z') :
(f.post_comp h).φ = f.φ h
@[simp]
theorem algebraic_topology.dold_kan.morph_components.pre_comp_b {C : Type u_1} {X X' : category_theory.simplicial_object C} {n : } {Z : C} (g : X' X) (i : fin (n + 1)) :
(f.pre_comp g).b i = g.app f.b i

A morph_components can be precomposed with a morphism of simplicial objects.

Equations