Commit 2023-12-27 05:26 f9e2c2ca

View on Github →

refactor(AlgebraicTopology): using the cofan API for SplitSimplicialObject (#8531) This PR changes the definition of a splitting of simplicial objects. The new definition makes a better use of the cofan API. As a result, it is no longer necessary to assume that the category has finite coproducts.

Estimated changes

Modified Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean

deleted theorem AlgebraicTopology.DoldKan.Γ₀.splitting_iso_hom_eq_id

deleted theorem AlgebraicTopology.DoldKan.Γ₀.splitting_map_eq_id

Modified Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean

Modified Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

Modified Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean

added theorem SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero

added theorem SimplicialObject.Splitting.cofan_inj_πSummand_eq_id

added theorem SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero

deleted theorem SimplicialObject.Splitting.ιSummand_comp_PInfty_eq_zero

deleted theorem SimplicialObject.Splitting.ι_πSummand_eq_id

deleted theorem SimplicialObject.Splitting.ι_πSummand_eq_zero

added theorem SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty

deleted theorem SimplicialObject.Splitting.πSummand_comp_ιSummand_comp_PInfty_eq_PInfty

Modified Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

added theorem SimplicialObject.Split.cofan_inj_naturality_symm

added def SimplicialObject.Split.natTransCofanInj

deleted def SimplicialObject.Split.natTransιSummand

deleted theorem SimplicialObject.Split.ιSummand_naturality_symm

added def SimplicialObject.Splitting.cofan'

added def SimplicialObject.Splitting.cofan

added theorem SimplicialObject.Splitting.cofan_inj_comp_app

added theorem SimplicialObject.Splitting.cofan_inj_epi_naturality

added theorem SimplicialObject.Splitting.cofan_inj_eq

added theorem SimplicialObject.Splitting.cofan_inj_id

added def SimplicialObject.Splitting.isColimit

deleted def SimplicialObject.Splitting.iso

deleted theorem SimplicialObject.Splitting.iso_hom

deleted theorem SimplicialObject.Splitting.iso_inv

deleted def SimplicialObject.Splitting.map

deleted def SimplicialObject.Splitting.ιCoprod

deleted def SimplicialObject.Splitting.ιSummand

deleted theorem SimplicialObject.Splitting.ιSummand_comp_app

deleted theorem SimplicialObject.Splitting.ιSummand_epi_naturality

deleted theorem SimplicialObject.Splitting.ιSummand_eq

deleted theorem SimplicialObject.Splitting.ιSummand_id