nLab restriction category

Restriction category

Restriction category


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:XYf\colon X\to Y is encoded in a specified idempotent endomorphism f¯\overline{f} of XX.


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

  • ff¯=ff\circ \overline{f} = f,
  • f¯g¯=g¯f¯\overline{f}\circ \overline{g} = \overline{g}\circ\overline{f} whenever s(f)=s(g)s(f)=s(g),
  • gf¯¯=g¯f¯\overline{g\circ \overline{f}} = \overline{g}\circ \overline{f} whenever s(f)=s(g)s(f)=s(g), and
  • g¯f=fgf¯\overline{g}\circ f = f\circ \overline{g\circ f} whenever s(g)=t(f)s(g) = t(f)

where s(f)=dom(f)s(f) = \text{dom}(f) is the domain of ff. 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 f¯\overline{f} is idempotent for composition: f¯f¯=f¯\overline{f}\circ \overline{f} = \overline{f}, and that the operation ff¯f \mapsto \overline{f} is also idempotent: f¯¯=f¯\overline{\overline{f}} = \overline{f} (among other properties).


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

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

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


Last revised on November 3, 2021 at 07:15:31. See the history of this page for a list of all contributions to it.