Commit 2024-10-09 15:32 b13c461d

View on Github →

feat(AlgebraicTopology/SimplicialSet): SimplicialSet (co)skeleton properties (#16781) Some assorted properties of the simplex category and simplicial sets. Co-Authored-By: Emily Riehl eriehl@jhu.edu Co-Authored-By: Pietro Monticone 38562595+pitmonticone@users.noreply.github.com Co-Authored-By: Joël Riou 37772949+joelriou@users.noreply.github.com

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

added theorem SimplexCategory.Truncated.Hom.ext

added theorem SimplexCategory.const_fac_thru_zero

added theorem SimplexCategory.eq_const_of_zero

added theorem SimplexCategory.eq_const_to_zero

added theorem SimplexCategory.eq_of_one_to_one

added theorem SimplexCategory.eq_of_one_to_two

added theorem SimplexCategory.exists_eq_const_of_zero

added def SimplexCategory.mkOfLe

added def SimplexCategory.mkOfLeComp

added def SimplexCategory.mkOfSucc

Modified Mathlib/AlgebraicTopology/SimplicialObject.lean

deleted def CategoryTheory.CosimplicialObject.sk

added def CategoryTheory.CosimplicialObject.truncation

deleted def CategoryTheory.SimplicialObject.sk

added def CategoryTheory.SimplicialObject.truncation

Modified Mathlib/AlgebraicTopology/SimplicialSet.lean

added def SSet.Truncated.uliftFunctor

deleted def SSet.sk

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.castSucc_le_castSucc_iff

added theorem Fin.castSucc_le_succ

modified theorem Fin.castSucc_lt_succ_iff

modified theorem Fin.succ_le_castSucc_iff

Modified Mathlib/Order/Category/NonemptyFinLinOrd.lean

added def Fin.hom_succ