Commit 2025-02-10 09:35 69b0864b
View on Github →refactor(CategoryTheory/Limits): split MultispanIndex into two structures (#20988)
Before this PR, multiequalizers were defined for a structure MulticospanIndex C which contained information about the shape of the diagram, and the diagram itself (objects and maps in a category C). In this PR, we introduce the shape MulticospanShape which consists of two types and two maps between these types. If J : MulticospanShape and C is a category, we now have MultispanIndex J C which contains the information about the multiequalizer diagram. If I : MulticospanIndex J C, we now have a functor I.multicospan : WalkingMulticospan J ⥤ C.
This refactor will ease the study of multiequalizers. For example, if I and I' are two terms in MulticospanIndex J C, it makes sense to show that the associated functors WalkingMulticospan J ⥤ C are isomorphic, etc.