AlgebraicTopology.DoldKan.decomposition_Q

theorem AlgebraicTopology.DoldKan.decomposition_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (n q : ℕ), (AlgebraicTopology.DoldKan.Q q).f (n + 1) = (Finset.filter (fun i => ↑i < q) Finset.univ).sum fun i => CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P ↑i).f (n + 1)) (CategoryTheory.CategoryStruct.comp (X.δ i.rev.succ) (X.σ i.rev))

The theorem `AlgebraicTopology.DoldKan.decomposition_Q` states that, in the context of algebraic topology, for any simplicial object `X` in a given category `C`, and for any natural numbers `n` and `q`, the idempotent endomorphism `Q q` at degree `n+1` can be expressed as a sum of morphisms, each of which is a postcomposition with appropriate degeneracy maps. Specifically, it is the sum over all `i` in the universal finite set, filtered such that `i` is less than `q`, of the composition of morphisms involving the face map `X.δ i.rev.succ` and the degeneracy map `X.σ i.rev`. This decomposition has significant implications in the case of simplicial abelian groups. It implies that any `(n+1)`-simplex `x` can be written 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`.

More concisely: In algebraic topology, for any simplicial object `X` in a category `C` and natural numbers `n` and `q`, the idempotent endomorphism `Q q` at degree `n+1` can be expressed as a sum of morphisms, each being a postcomposition of appropriate degeneracy maps and face maps.