Commit 2025-12-15 09:35 cd5830e8

View on Github →

feat(AlgebraicTopology): binary products of standard simplices (#32237) We start the study of nondegenerate simplices in Δ[p] ⊗ Δ[q]. In particular, we show that it is of dimension ≤ p + q. From https://github.com/joelriou/topcat-model-category

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

Created Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean

added def SSet.prodStdSimplex.isoNerve

added theorem SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv

added theorem SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv

added def SSet.prodStdSimplex.objEquiv

added theorem SSet.prodStdSimplex.objEquiv_apply_fst

added theorem SSet.prodStdSimplex.objEquiv_apply_snd

added theorem SSet.prodStdSimplex.objEquiv_map_apply

added theorem SSet.prodStdSimplex.objEquiv_naturality

added theorem SSet.prodStdSimplex.objEquiv_δ_apply

added def SSet.prodStdSimplex.orderHomOfSimplex

added theorem SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff