# Decomposition of the Q endomorphisms #

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 : SimplicialObject 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 MorphComponents 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₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ)) reflects isomorphisms.

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

theorem AlgebraicTopology.DoldKan.decomposition_Q {C : Type u_1} [] (n : ) (q : ) :
(n + 1) = iFinset.filter (fun (i : Fin (n + 1)) => i < q) Finset.univ, CategoryTheory.CategoryStruct.comp (.f (n + 1)) (CategoryTheory.CategoryStruct.comp (X i.rev.succ) (X i.rev))

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 AlgebraicTopology.DoldKan.MorphComponents.ext_iff {C : Type u_1} :
∀ {inst : } {X : } {n : } {Z : C} {x y : }, x = y x.a = y.a x.b = y.b
theorem AlgebraicTopology.DoldKan.MorphComponents.ext {C : Type u_1} :
∀ {inst : } {X : } {n : } {Z : C} {x y : }, x.a = y.ax.b = y.bx = y
structure AlgebraicTopology.DoldKan.MorphComponents {C : Type u_1} [] (n : ) (Z : C) :
Type u_2

The structure MorphComponents is an ad hoc structure that is used in the proof that N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex 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
def AlgebraicTopology.DoldKan.MorphComponents.φ {C : Type u_1} [] {n : } {Z : C} (f : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.id_a {C : Type u_1} [] (n : ) :
= AlgebraicTopology.DoldKan.PInfty.f (n + 1)
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.id_b {C : Type u_1} [] (n : ) (i : Fin (n + 1)) :
= X i

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

Equations
• = { a := AlgebraicTopology.DoldKan.PInfty.f (n + 1), b := fun (i : Fin (n + 1)) => X i }
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.postComp_b {C : Type u_1} [] {n : } {Z : C} {Z' : C} (f : ) (h : Z Z') (i : Fin (n + 1)) :
(f.postComp h).b i =
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.postComp_a {C : Type u_1} [] {n : } {Z : C} {Z' : C} (f : ) (h : Z Z') :
(f.postComp h).a =
def AlgebraicTopology.DoldKan.MorphComponents.postComp {C : Type u_1} [] {n : } {Z : C} {Z' : C} (f : ) (h : Z Z') :

A MorphComponents can be postcomposed with a morphism.

Equations
• f.postComp h = { a := , b := fun (i : Fin (n + 1)) => }
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.postComp_φ {C : Type u_1} [] {n : } {Z : C} {Z' : C} (f : ) (h : Z Z') :
(f.postComp h) =
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.preComp_b {C : Type u_1} [] {X' : } {n : } {Z : C} (f : ) (g : X' X) (i : Fin (n + 1)) :
(f.preComp g).b i = CategoryTheory.CategoryStruct.comp (g.app ) (f.b i)
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.preComp_a {C : Type u_1} [] {X' : } {n : } {Z : C} (f : ) (g : X' X) :
def AlgebraicTopology.DoldKan.MorphComponents.preComp {C : Type u_1} [] {X' : } {n : } {Z : C} (f : ) (g : X' X) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgebraicTopology.DoldKan.MorphComponents.preComp_φ {C : Type u_1} [] {X' : } {n : } {Z : C} (f : ) (g : X' X) :
(f.preComp g) = CategoryTheory.CategoryStruct.comp (g.app (Opposite.op (SimplexCategory.mk (n + 1)))) f