nLab equivalence relation

Equivalence relations

Equivalence relations

Definition

An equivalence relation on a set SS is a binary relation \equiv on SS that is:

  • reflexive: xxx \equiv x for all x:Sx: S;
  • symmetric: xyx \equiv y if yxy \equiv x; and
  • transitive: xzx \equiv z if xyzx \equiv y \equiv z.

Thus, an equivalence relation is a symmetric preorder.

(One can also define it as a relation that is both reflexive and euclidean.) The de Morgan dual of an equivalence relation is an apartness relation.

If RR is any relation on SS, there is a smallest equivalence relation containing RR (noting that an intersection of an arbitrary family of equivalence relations is again such; see also Moore closure), called the equivalence relation generated by RR.

In homotopy type theory

In homotopy type theory, since propositions are subsingletons, an equivalence relation on a type TT is a type family xyx \equiv y indexed by elements x:Tx:T and y:Ty:T with witnesses of reflexivity, transitivity, and symmetry, and propositional truncation:

refl(x):xx\mathrm{refl}(x):x \equiv x
trans(x,y,z):xy×yzxz\mathrm{trans}(x, y, z):x \equiv y \times y \equiv z \to x \equiv z
sym(x,y):xyyx\mathrm{sym}(x, y):x \equiv y \to y \equiv x
proptrunc(x,y): p:xy q:xyp=q\mathrm{proptrunc}(x, y):\prod_{p:x \equiv y} \prod_{q:x \equiv y} p = q

One then further distinguishes between a type with an equivalence relation (a symmetric preordered type) and an h-set with an equivalence relation (a symmetric proset).

Extensional functions

Let A(A 0, A)A \coloneqq (A_0, \equiv_A) and B:(B 0, B)B:\coloneqq (B_0, \equiv_B) be two symmetric preordered types. An extensional function f:ABf:A \to B consists of a function f 0:A 0B 0f_0:A_0 \to B_0 and for all elements a:A 0a:A_0 and b:A 0b:A_0 a function f (a,b):(a Ab)(f 0(a) Bf 0(b))f_\equiv(a, b):(a \equiv_A b) \to (f_0(a) \equiv_B f_0(b)).

The identity function id A:AAid_A:A \to A is an extensional function which consists of the identity function id A 0:A 0A 0id_{A_0}:A_0 \to A_0 for all elements a:A 0a:A_0 and b:A 0b:A_0, the identity function id (a,b):(a Ab)(a Ab))id_\equiv(a, b):(a \equiv_A b) \to (a \equiv_A b)).

Given symmetric preordered types A(A 0, A)A \coloneqq (A_0, \equiv_A), B:(B 0, B)B:\coloneqq (B_0, \equiv_B), and C(C 0, C)C \coloneqq (C_0, \equiv_C), the composition gf:ACg \circ f:A \to C of extensional functions f:ABf:A \to B and g:BCg:B \to C is defined as

(gf) 0g 0f 0(g \circ f)_0 \coloneqq g_0 \circ f_0

and for all objects a:A 0a:A_0 and b:A 0b:A_0,

(gf) (a,b)g equiv(f 0(a),f 0(b))f equiv(a,b)(g \circ f)_\equiv(a, b) \coloneqq g_equiv(f_0(a), f_0(b)) \circ f_equiv(a, b)

Injections, surjections, and bijections

An extensional function f:ABf:A \to B is a injection if for all elements b:B 0b:B_0 the type of elements a:A 0a:A_0 with a witness p(a,b):f 0(a)bp(a, b):f_0(a) \equiv b is a subsingleton.

An extensional function f:ABf:A \to B is a surjection if for all elements b:B 0b:B_0 the type of elements a:A 0a:A_0 with a witness p(a,b):f 0(a)bp(a, b):f_0(a) \equiv b is a pointed type.

An extensional function f:ABf:A \to B is a bijection if it is both an injection and a surjection; i.e. for all elements b:B 0b:B_0 the type of elements a:A 0a:A_0 with a witness p(a,b):f 0(a)bp(a, b):f_0(a) \equiv b is a pointed subsingleton, or a singleton.

Bijections, isomorphisms, and equivalences

An extensional function f:ABf:A \to B is a bijection if for all elements b:B 0b:B_0 the type of elements a:A 0a:A_0 with a witness p(a,b):f 0(a)bp(a, b):f_0(a) \equiv b is a singleton.

An extensional function f:ABf:A \to B is an isomorphism if there exist an extensional functiom g:BAg:B \to A with witnesses ret(f,g):gf=id A\mathrm{ret}(f, g):g \circ f = id_{A} and sec(f,g):fg=id B\mathrm{sec}(f, g):f \circ g = id_{B}.

An extensional function f:ABf:A \to B is an equivalence if the function f 0:A 0B 0f_0:A_0 \to B_0 is an equivalence of types and for all elements a:A 0a:A_0 and b:A 0b:A_0 the function f (a,b):(a Ab)(f 0(a) Bf 0(b))f_\equiv(a, b):(a \equiv_A b) \to (f_0(a) \equiv_B f_0(b)) is an equivalence of types.

The only symmetric preordered types for which bijection, isomorphism, and equivalence are the same are the symmetric posets, which are the h-sets.

A categorical view

A set equipped with an equivalence relation can be regarded as a groupoid enriched over the cartesian monoidal category of truth values. Equivalently, it is a groupoid that is 0-truncated. Then the equivalence relation on SS is a way of making SS into the set of objects of such a groupoid. Equivalently, a set with an equivalence relation is a (0,1)-category whose each morphism is iso, or a symmetric preordered set.

It may well be useful to consider several possible equivalence relations on a given set. When considering a single equivalence relation once and for all, however, it is common to take the quotient set S/ S/_{\equiv} and use that instead. As a groupoid, any set with an equivalence relation is equivalent to a set in this way (although in the absence of the axiom of choice, it is only a “weak” or ana-equivalence).

A set equipped with an equivalence relation is sometimes called a setoid; however the term setoid is primarily used for a pseudo-equivalence relation instead, and the usage on the nLab follows the latter.

This terminology is particularly common in foundations of mathematics where quotient sets don't always exist and the above equivalence to a set cannot be carried out. However, arguably this is a terminological mismatch, and such people should say ‘set’ where they say ‘setoid’ and something else (such as ‘preset’, ‘type’, or ‘completely presented set’) where they say ‘set’. (See Bishop set and page 9 of these lecture notes.)

Variants and generalizations

References

For the history of the notion of equivalence relation see this MO discussion.

Last revised on December 8, 2022 at 13:34:09. See the history of this page for a list of all contributions to it.