Restriction Category Perspectives of Partial Computation and Geometry

Abstract

This thesis introduces several structures based on Cockett and Lack’s restriction categories which find applications in partial computation, geometry, topology and two-dimensional category theory.

As monads may be thought of as modelling computation, we introduce restriction monads as a candidate to model partial computation. These structures are defined in the hope that any dependencies on the restriction structure of a category can be abstracted instead into an endofunctor on it. For example, we prove that the data of a small restriction category can be encoded as a restriction monad in Span(Set). We introduce restriction bimodules (bimodules whose actions are partially defined) and prove that they are algebras for these monads.

The Ehresmann-Schein-Nambooripad theorem asserts an equivalence between the categories of inverse semigroups and that of certain groupoids. We prove that this equivalence can be extended to an equivalence between inverse categories (categories in which all arrows are partially invertible) and top-heavy locally inductive groupoids (categories in which all arrows are totally invertible, all arrows have a notion of restriction and corestriction, and the objects may be partitioned into meet-semilattices) in two different ways (using two different notions of morphism). For any join inverse category X, we prove that the corresponding top-heavy locally inductive groupoid G(X) is locally localic and that each morphism in X gives an equivalence between the locales generated by the principal order ideals of its source and target. We then prove that G(X) can be naturally given the structure of an Ehresmann site, which then motivates our definition of ideally covering and ideally flat functors between Ehresmann sites that make the constructions of Lawson and Steinberg functorial.

Finally, we introduce double restriction categories (a double category equipped with two compatible restriction structures) and restriction bicategories (bicategories with a “weak” restriction operator). We show that the bicategory of restriction modules can be given the structure of a restriction bicategory and use these to organize restriction monads, restriction modules, monad morphisms, and module morphisms into a double restriction category.