Commit 2026-08-19 11:50 059e9bba

View on Github →

feat(AlgebraicTopology/SimplicialSet): induction principle for morphisms of the homotopy category of a simplicial set (#42673)

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

added def SSet.HomotopyCategory.homMk

added theorem SSet.HomotopyCategory.homMk_comp_homMk

added theorem SSet.HomotopyCategory.homMk_id

added theorem SSet.HomotopyCategory.hom_rec

added def SSet.HomotopyCategory.mk

added def SSet.HomotopyCategory.objEquiv

added def SSet.HomotopyCategory.rec

added theorem SSet.HomotopyCategory.rec_mk

deleted def SSet.hoFunctor.obj.equiv

modified def SSet.hoFunctor

added def SSet.mapHomotopyCategory

added theorem SSet.mapHomotopyCategory_map_homMk

added theorem SSet.mapHomotopyCategory_obj_mk

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

added theorem CategoryTheory.Limits.map_braiding_hom_comp_prodComparison