Commit 2025-10-28 23:08 9ceda6f5

View on Github →

feat(AlgebraicTopology): the homotopy category functor preserves products (#25780) This proves that the homotopy category construction defines a monoidal functor from simplicial sets to categories. In particular, simplicially enriched categories have quotient categorically enriched categories, which might be thought of as "homotopy bicategories."

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean

added def SimplexCategory.homEquivFunctor

added def SimplexCategory.homEquivOrderHom

Modified Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

added def CategoryTheory.nerve.representableBy

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

added theorem CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplex

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

Modified Mathlib/CategoryTheory/Category/ULift.lean

added def CategoryTheory.ULiftHom.objEquiv

added def CategoryTheory.ULiftHomULiftCategory.equivCongrLeft.{v',

added def CategoryTheory.ULiftHomULiftCategory.objEquiv.{v',

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

added theorem CategoryTheory.CartesianMonoidalCategory.isLeftAdjoint_prod_functor

Modified Mathlib/CategoryTheory/ComposableArrows.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

added theorem CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimit

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

added theorem CategoryTheory.Limits.prodComparison_natural_of_natTrans

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

Modified Mathlib/Order/Hom/Basic.lean

added def OrderHom.uliftLeftMap

added theorem OrderHom.uliftLeftMap_uliftRightMap_eq

added def OrderHom.uliftRightMap

added theorem OrderHom.uliftRightMap_uliftLeftMap_eq