Commit 2023-04-21 12:33 88850ab9

View on Github →

feat: port AlgebraicTopology.DoldKan.SplitSimplicialObject (#3563)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/DoldKan/PInfty.lean

added theorem AlgebraicTopology.DoldKan.QInfty_f

deleted theorem AlgebraicTopology.DoldKan.qInfty_f

Created Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean

added theorem SimplicialObject.Splitting.PInfty_comp_πSummand_id

added theorem SimplicialObject.Splitting.comp_PInfty_eq_zero_iff

added theorem SimplicialObject.Splitting.decomposition_id

added theorem SimplicialObject.Splitting.ιSummand_comp_PInfty_eq_zero

added theorem SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero

added theorem SimplicialObject.Splitting.ι_πSummand_eq_id

added theorem SimplicialObject.Splitting.ι_πSummand_eq_zero

added theorem SimplicialObject.Splitting.πSummand_comp_ιSummand_comp_PInfty_eq_PInfty

added theorem SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero