A sind-object of a category is a formal sifted colimit of objects of . Here βformalβ means that the colimit is taken in the category of presheaves of (the free cocompletion of ). The category of sind-objects of is written - or . It is the sifted colimit completion of .
There is an analogy here with ind-objects, which are formal filtered colimits, and where the category of ind-objects is the filtered colimit completion of .
Typically the main case of interest here is the situation where is small with finite coproducts. If a small category has finite coproducts, the sifted colimit completion comprises the finite-product-preserving presheaves:
The analogy here is that if a small category has finite colimits, the filtered colimit completion comprises the finite limit preserving presheaves:
One reason this is often relevant because if has finite products, it can be regarded as an algebraic theory, and then the sifted colimit completion comprises the category of models of the theory.
Another point of relevance is that this is a canonical way of building a cartesian closed category out of a distributive category.
If has finite coproducts then consider the category of finite product preserving functors
The representable objects always preserves finite products, and so the Yoneda embedding factors through . This exhibits as the free sifted colimit completion of .
If is has sifted colimits then the Yoneda embedding induces a natural bijection between functors and sifted-colimit-preserving functors .
The construction has another universal property, as the free colimit completion of a category respecting the existing finite coproducts.
If is has colimits then the Yoneda embedding induces a natural bijection between finite-coproduct-preserving functors and colimit-preserving-functors .
The sifted-colimit-completion also gives a way of full and faithfully embedding a distributive category in a cartesian closed category, while preserving the structure. From a type-theoretic perspective, this shows that function types are a conservative extension of finite type theory.
Let be a small category with finite coproducts and products. The following are equivalent.
is a distributive category.
is cartesian closed.
Jiri Adamek, Jiri Rosicky, Enrico Vitale, What are sifted colimits?, TAC 23 (2010) pp. 251β260. (web)
Jiri Adamek, Jiri Rosicky, On sifted colimits and generalized varieties, TAC 8 (2001) pp 33β53. (web)
The idea of product-preserving-functors as a cartesian closed category is in various sources, including:
Marcelo Fiore, βEnrichment and representation theorems for categories of domains and partial functionsβ. 1996. web.
John Power, βGeneric models for computational effectsβ, Theor. Comput. Sci. 364(2): 254-269 (2006)
Younesse Kaddar, βIdeal distributorsβ, Section 1. 2020. report.
G. A. Kavvos, Two-dimensional Kripke Semantics II: Stability and Completeness, arXiv:2406.03578 (2024).
Last revised on July 4, 2024 at 10:12:03. See the history of this page for a list of all contributions to it.