Commit 2024-06-05 09:14 7ef586d0

View on Github →

feat(AlgebraicTopology): simplicial categories (#11398) This PR defines simplicial categories as categories that are enriched over simplicial sets in such a way that morphisms identify to 0-simplices of the enriched hom.

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SimplicialCategory/Basic.lean

added def CategoryTheory.SimplicialCategory.homEquiv'

added theorem CategoryTheory.SimplicialCategory.sHomWhiskerLeft_comp

added theorem CategoryTheory.SimplicialCategory.sHomWhiskerLeft_id

added theorem CategoryTheory.SimplicialCategory.sHomWhiskerRight_comp

added theorem CategoryTheory.SimplicialCategory.sHomWhiskerRight_id

added theorem CategoryTheory.SimplicialCategory.sHom_whisker_exchange

Modified Mathlib/CategoryTheory/Enriched/Basic.lean

added theorem CategoryTheory.e_assoc'