Commit 2026-01-12 14:46 4920a637

View on Github →

feat(AlgebraicTopology): a computable monoidal functor instance for hoFunctor (#31325) We construct a computable equivalence of categories (X ⊗ Y).HomotopyCategory ≌ X.HomotopyCategory × Y.HomotopyCategory for 2-truncated simplicial sets X and Y. This allows to make the bicategory instance on quasicategories computable.

Estimated changes

Modified Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean

added def SSet.QCat.forgetEnrichment.equiv

Modified Mathlib/AlgebraicTopology/SimplicialSet/HoFunctorMonoidal.lean

added def SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.associativity'Iso_hom_app

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.associativity

added def SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso_hom_app

added def SSet.Truncated.HomotopyCategory.BinaryProduct.curriedInverse

added def SSet.Truncated.HomotopyCategory.BinaryProduct.equivalence

added def SSet.Truncated.HomotopyCategory.BinaryProduct.functor

added def SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functor_map

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.functor_obj

added def SSet.Truncated.HomotopyCategory.BinaryProduct.idProdMapHomotopyCategoryCompInverseIso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse

added def SSet.Truncated.HomotopyCategory.BinaryProduct.inverse

added def SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app

added def SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategoryFstIso

added def SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategorySndIso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_functor

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_obj

added def SSet.Truncated.HomotopyCategory.BinaryProduct.iso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality

added def SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategoryProdIdCompInverseIso

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality

added theorem SSet.Truncated.HomotopyCategory.BinaryProduct.square

deleted theorem SSet.Truncated.HomotopyCategory.square

added def SSet.hoFunctor.unitHomEquiv

added theorem SSet.hoFunctor.unitHomEquiv_eq

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

deleted def CategoryTheory.hoFunctor.unitHomEquiv

deleted theorem CategoryTheory.hoFunctor.unitHomEquiv_eq