nLab equivalence relation

Redirected from "symmetric prosets".
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, see there for more.

Variants and generalizations

References

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

Last revised on June 17, 2023 at 06:43:41. See the history of this page for a list of all contributions to it.