Commit 2022-11-14 15:10 ed98c07fView on Github →
feat(algebraic_topology/dold_kan): a few basic lemmas and a property of P_infty (#17538)
This PR introduces some very basic lemmas for the complement projection
P. We also obtain the lemma
ι_summand_comp_P_infty_eq_zero which states that in a given degree,
P_infty vanishes on all the summands of a split simplicial object except one.