Theorems · Theorem · category theory

AlgebraicTopology.DoldKan.decomposition_Q

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n q : ℕ),
  (AlgebraicTopology.DoldKan.Q q).f (n + 1) =
    ∑ i with ↑i < q,
      CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P ↑i).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$.

Defined in

Mathlib.AlgebraicTopology.DoldKan.Decomposition

Cited by

4 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive