SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero

theorem SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X : CategoryTheory.SimplicialObject C} (s : SimplicialObject.Splitting X) {n : ℕ} (A : SimplicialObject.Splitting.IndexSet (Opposite.op (SimplexCategory.mk n))), ¬A.EqId → CategoryTheory.CategoryStruct.comp ((s.cofan (Opposite.op (SimplexCategory.mk n))).inj A) (AlgebraicTopology.DoldKan.PInfty.f n) = 0

The theorem `SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero` states that if `X` is a split simplicial object in an additive category `C`, then for any natural number `n`, and for any index `A` in the splitting index set not corresponding to the identity of `[n]`, the composition of `s.cofan` injected at `A` and the `n`-th component of the functor `PInfty` is equal to zero. In simpler terms, if an object in the category is split, then a specific combination of its components, as dictated by the functor `PInfty`, is nullified if the index does not correspond to the identity.

More concisely: If `X` is a split simplicial object in an additive category `C`, then for any natural number `n` and any index `A` not corresponding to the identity of `[n]`, the composition of `s.cofan` at index `A` and `PInfty`'s `n`-th component is zero.