Commit 2025-11-04 11:56 64694b02

View on Github →

feat(AlgebraicTopology): basic missing lemmas about the simplex category (#31248)

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

added theorem SimplexCategory.mkOfSucc_eq_id

added theorem SimplexCategory.mkOfSucc_one_eq_δ

added theorem SimplexCategory.mkOfSucc_zero_eq_δ

added theorem SimplexCategory.δ_one_eq_const

added theorem SimplexCategory.δ_zero_eq_const

Modified Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean

added theorem SimplexCategory.Truncated.Hom.tr_id

deleted def SimplexCategory.Truncated

Modified Mathlib/AlgebraicTopology/SimplexCategory/Truncated.lean

added theorem SimplexCategory.Truncated.δ₂_one_comp_σ₂_one

added theorem SimplexCategory.Truncated.δ₂_one_eq_const

added theorem SimplexCategory.Truncated.δ₂_zero_comp_δ₂_two

added theorem SimplexCategory.Truncated.δ₂_zero_eq_const

Modified Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

added theorem CategoryTheory.SimplicialObject.δ_def

added theorem CategoryTheory.SimplicialObject.σ_def

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

added theorem SSet.Truncated.comp_app

added theorem SSet.Truncated.id_app