Commit 2025-07-22 07:13 f1a92a38

View on Github →

Feat(CategoryTheory): terminal categories with an application to hoFunctor (#25781) Some preliminary API around terminal categories is developed with an application for the infinity-cosmos project: proving that the homotopy category functor preserves terminal objects. We also include proofs that [0] is terminal in the simplex category and Δ[0] is the terminal simplicial set. Co-authored by Robin Carlier, Jakob von Raumer, Adam Topaz, and Zeyi Zhao.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

added def SimplexCategory.isTerminalZero

added theorem SimplexCategory.toCat.obj_eq_Fin

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

added def SSet.isTerminalHoFunctorDeltaZero

Modified Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

added theorem SSet.stdSimplex.ext₀

added def SSet.stdSimplex.isTerminalObj₀

Created Mathlib/CategoryTheory/Category/Cat/Terminal.lean

added def CategoryTheory.Cat.isTerminalDiscretePUnit

added def CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete

added def CategoryTheory.Cat.isoDiscretePUnitOfIsTerminal

Modified Mathlib/CategoryTheory/Category/ReflQuiv.lean

added theorem CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id

Modified Mathlib/CategoryTheory/EssentiallySmall.lean

Modified Mathlib/CategoryTheory/Quotient.lean