equivalence relation in nLab

Equivalence relations

Equivalence relations

Definition

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

• reflexive: x≡xx \equiv x for all x:Sx: S;
• symmetric: x≡yx \equiv y if y≡xy \equiv x; and
• transitive: x≡zx \equiv z if x≡y≡zx \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 x≡yx \equiv y indexed by elements x:Tx:T and y:Ty:T with witnesses of reflexivity, transitivity, and symmetry, and propositional truncation:

refl(x):x≡x\mathrm{refl}(x):x \equiv x

trans(x,y,z):x≡y×y≡z→x≡z\mathrm{trans}(x, y, z):x \equiv y \times y \equiv z \to x \equiv z

sym(x,y):x≡y→y≡x\mathrm{sym}(x, y):x \equiv y \to y \equiv x

proptrunc(x,y):∏ p:x≡y∏ q:x≡yp=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:A→Bf:A \to B consists of a function f 0:A 0→B 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:A→Aid_A:A \to A is an extensional function which consists of the identity function id A 0:A 0→A 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 g∘f:A→Cg \circ f:A \to C of extensional functions f:A→Bf:A \to B and g:B→Cg:B \to C is defined as

(g∘f) 0≔g 0∘f 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,

(g∘f) ≡(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:A→Bf: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:A→Bf: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:A→Bf: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:A→Bf: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:A→Bf:A \to B is an isomorphism if there exist an extensional functiom g:B→Ag:B \to A with witnesses ret(f,g):g∘f=id A\mathrm{ret}(f, g):g \circ f = id_{A} and sec(f,g):f∘g=id B\mathrm{sec}(f, g):f \circ g = id_{B}.

An extensional function f:A→Bf:A \to B is an equivalence if the function f 0:A 0→B 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, see there for more.

Variants and generalizations

• A partial equivalence relation is a symmetric and transitive relation.

• A congruence is a notion of equivalence relation internal to a suitable category.

• The generalization of this to (∞,1)-category theory is that of groupoid object in an (∞,1)-category.

• Bishop set

• congruence

• complete loop graph

• stable equivalence relation

• pseudo-equivalence relation

• quotient equivalence relation

• enriched set

• monoidal symmetric proset

• set-like structure in homotopy type theory?

• tolerance relation

References

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