Commit 2026-08-13 09:18 32aa3e89

View on Github →

feat(AlgebraicTopology): non-degenerate simplices in Δ[p] ⊗ Δ[q] (#41624) We show that any non-degenerate simplex in Δ[p] ⊗ Δ[q] is contained in the subcomplex generated by a (p + q)-dimensional non-degenerate simplex. (CosimplicialObject is also made an abbrev, similarly as SimplicialObject.) From https://github.com/joelriou/topcat-model-category

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

deleted def CategoryTheory.CosimplicialObject

Modified Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean

added theorem SSet.prodStdSimplex.exists_nonDegenerate_max_dim

modified theorem SSet.prodStdSimplex.objEquiv_apply_fst

modified theorem SSet.prodStdSimplex.objEquiv_apply_snd

added theorem SSet.prodStdSimplex.objEquiv_apply_symm_apply

modified theorem SSet.prodStdSimplex.objEquiv_δ_apply

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

added theorem SSet.stdSimplex.mem_ofSimplex_obj_iff

modified theorem SSet.yonedaEquiv_symm_app

Created Mathlib/Order/Fin/Prod.lean