nLab partial equivalence relation

Redirected from "PER".
Partial equivalence relations

Partial equivalence relations

Definitions

A partial equivalence relation (sometimes abbreviated PER) is a binary relation satisfying the symmetry and transitivity conditions of an equivalence relation, but not necessarily the reflexivity condition. That is, a partial equivalence relation on XX is a binary relation R(x,y)X 2R(x, y) \subseteq X^2 such that for all xx and yy in XX, R(x,y)R(x, y) implies R(y,x)R(y, x), and for all xx, yy, and zz in XX, R(x,y)R(x, y) and R(y,z)R(y, z) together imply R(x,z)R(x, z).

Just as unary relations on a set XX correspond to subsets of XX and equivalence relations on XX correspond to quotients of XX, so partial equivalence relations on XX correspond to subquotients of XX. That is, the elements satisfying R(x,x)R(x, x) comprise a subset of XX, on which the relation restricts to a total equivalence relation specifying a further quotient.

Examples

Consider the set XX of all infinite sequences of rational numbers. Let such sequences xx and yy be related if

lim i,j|x iy j|=0. \lim_{i,j\to \infty} {|x_i - y_j|} = 0 .

Then this defines a partial equivalence relation RR on XX; the corresponding subquotient of XX is the set of Cauchy real numbers. Normally, this definition of real number is split into two parts: those sequences satsifying the reflexivity condition of RR are the Cauchy sequences of rational numbers (under the absolute-value metric), and then we impose a total equivalence relation on the Cauchy sequences. But a single partial equivalence relation does all of the work. (This example generalises in the usual ways.)

Category of PERs

If AA is a partial combinatory algebra, then the partial equivalence relations on AA are the objects of the category of PERs over AA, a locally cartesian closed Heyting category that is a full subcategory of the quasitopos of assemblies, which is in turn a full subcategory of the realizability topos over AA.

Last revised on May 31, 2018 at 17:07:00. See the history of this page for a list of all contributions to it.