nLab category of PERs

The category of PERs

The category of PERs

Idea

The category of PERs over a partial combinatory algebra AA is a particularly concrete and simple subcategory of its realizability topos, which is especially well-suited to modelling “computable” objects relative to AA.

It is based on the idea that a “computable set” XX relative to AA is specified by saying which elements of AA are “codes” representing which elements of XX, such that no element of AA can code for more than one element of XX (but not all elements of AA need to code for any element of XX). Thus this sort of “computable set” (sometimes called a modest set) is equivalently a partition of a subset of AA, i.e. a partial equivalence relation on AA.

Definition

Let AA be a partial combinatory algebra. If EE is a partial equivalence relation on AA, we write A/EA/E for its set of equivalence classes. Now the category PER(A)PER(A) has:

  • as objects, the partial equivalence relations on AA.

  • as morphisms EEE\to E', for PERs EE and EE', the set-theoretic functions ϕ:A/EA/E\phi:A/E \to A/E' with the property of being “tracked”, i.e. such that there exists an element fAf\in A such that whenever (a,a)E(a,a)\in E we have ϕ([a])=[fa]\phi([a]) = [f\cdot a] (hence in particular (fa,fa)E(f\cdot a,f\cdot a)\in E'). Equivalently, it is the quotient of the set of elements fAf\in A such that (a,b)E(a,b)\in E implies (fa,fb)E(f\cdot a,f\cdot b)\in E' by the relation fgf\sim g meaning that (fa,ga)E(f\cdot a,g\cdot a)\in E' whenever (a,a)E(a,a)\in E.

Properties

Last revised on April 28, 2019 at 00:39:51. See the history of this page for a list of all contributions to it.