category of partial equivalence relations

Given a theory in first-order logic with equality (categorically, this can be taken as a first-order hyperdoctrine), its category of partial equivalence relations represents all the subquotients the theory can “see” of its given sorts and all the functions the theory can “see” between them.

Specifically, the objects of this category are pairs (X,R)(X, R) where XX is a sort in the first-order theory and RR is a binary predicate which the theory proves to be a partial equivalence relation on XX. A morphism between objects (X,R)(X, R) and (Y,S)(Y, S) can be taken to be a binary predicate FP(X×Y)F \in P(X \times Y) such that the theory proves FF is essentially the graph of a function between the specified subquotients (In detail: …). Composition is given in the obvious way (In detail: …).

In the case where the original hyperdoctrine was in fact a tripos, the resulting category of PERs will be a topos (while the converse isn’t quite true, the condition of being a tripos is just slightly stronger than necessary for this to happen).

Last revised on February 23, 2010 at 22:27:46. See the history of this page for a list of all contributions to it.