nLab restriction category

Idea

The concept of restriction category is an element-free formalisation of the idea of a category of partial maps, where the domain of a map $f\colon X\to Y$ is encoded in a specified idempotent endomorphism $\overline{f}$ of $X$.

Definition

Given a category $C$, a restriction structure consists of the assignment to each morphism $f\colon X\to Y$ a morphism $\overline{f}\colon X\to X$ satisfying the following conditions:

• $f\circ \overline{f} = f$,
• $\overline{f}\circ \overline{g} = \overline{g}\circ\overline{f}$ whenever $s(f)=s(g)$,
• $\overline{g\circ \overline{f}} = \overline{g}\circ \overline{f}$ whenever $s(f)=s(g)$, and
• $\overline{g}\circ f = f\circ \overline{g\circ f}$ whenever $s(g) = t(f)$

where $s(f) = \text{dom}(f)$ is the domain of $f$. A restriction category is a category with a restriction structure.

Note that a restriction structure is a structure in the technical sense of the word, not a property. Note that it follows from the above definition that $\overline{f}$ is idempotent for composition: $\overline{f}\circ \overline{f} = \overline{f}$, and that the operation $f \mapsto \overline{f}$ is also idempotent: $\overline{\overline{f}} = \overline{f}$ (among other properties).

Examples

Every category admits the trivial restriction structure, with $\overline{f} = id_{s(f)}$.

Conversely the wide subcategory consisting off all the objects together with the morphisms $f$ satsfying $\overline{f}=id_{s(f)}$—the total morphisms—has a trivial induced restriction structure.

The category $PF$ of sets and partial functions is the prototypical example, where for a partial function $X \supseteq U \stackrel{f}{\to} Y$, the partial endomorphism $\overline{f}$ is the partially-defined identity function $X \supseteq U \hookrightarrow X$. Many other examples are listed in (Cockett–Lack 2002)

Related concepts

• partial function
• cartesian restriction category
• Turing category

References

• Robin Cockett and Steve Lack, Restriction categories I: categories of partial maps, Theoretical Computer Science 270 1-2 (2002) 223-259 [doi:10.1016/S0304-3975(00)00382-0]

• Robin Cockett and Steve Lack, Restriction categories II: partial map classification, Theoretical Computer Science 294 1-2 (2003) 61-102 [doi:10.1016/S0304-3975(01)00245-6]

• Robin Cockett and Steve Lack, Restriction categories III: colimits, partial limits and extensivity, Mathematical Structures in Computer Science 17 4 (2007) 775-817 [arXiv:math/0610500, doi:10.1017/S0960129507006056]

The following provides some historical context for the notion of restriction category in §2, and describe the relation to allegories:

• Robin Cockett and Ernie Manes, Boolean and classical restriction categories, Mathematical Structures in Computer Science 19.2 (2009): 357-416.

• Robin Cockett and Richard Garner, Restriction categories as enriched categories, Theoretical Computer Science 523 (2014) 37-55 [arXiv:1211.6170, doi:10.1016/j.tcs.2013.12.018]

A double categorical approach to restriction categories is proposed in:

• Robert Paré, A double category take on restriction categories, (slides)

On showing that restriction categories are categories enriched in a double category?:

• Robin Cockett and Richard Garner, Restriction categories as enriched categories, Theoretical Computer Science 523 (2014): 37-55.

On free cocompletions of restriction categories:

• Richard Garner and Daniel Lin, Cocompletion of restriction categories, Theory and Applications of Categories 35.22 (2020): 809-844.

On using restriction categories to model essentially algebraic theories:

• Ivan Di Liberti, Fosco Loregian, Chad Nester?, Paweł Sobociński. Functorial semantics for partial theories, Proceedings of the ACM on Programming Languages 5.POPL (2021): 1-28.

On range restriction categories:

• Xiuzhan Guo, Ranges, restrictions, partial maps, and fibrations (2004), Master’s thesis (pdf).