Equivalence Relation

definition example program

Let $A$ be a Set. An equivalence relation on $A$ is a binary Relation, written with infix $\sim$, such that for all $a,b,c\in A$:

(a) $a\sim a$ — reflexivity; (b) $a\sim b$ iff $b\sim a$ — symmetry; (c) if $a\sim b$ and $b\sim c$ then $a\sim c$ — transitivity.

Sources: 7 Sketches Definition 1.18, Remark 1.31, Example 1.72; Kittenlab Lecture 9; CTfS Definition 2.6.1.1, Examples 2.6.1.2–2.6.1.4, Definition 2.6.1.7, Exercises 2.6.1.3–2.6.1.10, 3.2.1.15

Relation to other notions

• A Preorder is an equivalence relation without the symmetry condition (Remark 1.31); a preorder that is symmetric is a Dagger Preorder (Example 1.72). Kittenlab: an equivalence relation is a preorder in which every morphism is invertible, i.e. a Groupoid that is thin.
• Equivalence relations on $A$ are in bijection with partitions of $A$: Partitions Correspond to Equivalence Relations. The set of classes is the Quotient Set $A/\sim$.
• Every preorder induces an equivalence relation $x\cong y$ iff $x\le y$ and $y\le x$ (Example 1.49); see Equivalent Elements of a Preorder.
• In a category, equivalence relations arise as coequalizers: “declaring by fiat” that two elements are equal (Kittenlab Lecture 9, 11).

Examples from Category Theory for Scientists

• $x\sim y$ iff $x+7n=y$ for some $n\in \mathbb{Z}$ (congruence mod 7) — reflexive with $n=0$, symmetric with $-n$, transitive with $m+n$ (CTfS Example 2.6.1.2). ”$x$ spends a lot of time thinking about $y$” is none of reflexive, symmetric, transitive (CTfS Exercise 2.6.1.3).
• Kernels: for any function $f:X\to B$, "$f(x)=f(y)$" is an equivalence relation, and every equivalence relation arises this way (take $f$ the quotient map $X\to X/\sim$) — partitions, fibers and equivalence relations are three faces of one idea (CTfS Exercise 2.6.1.5). “Being isomorphic” on a set of sets, and “being in the same orbit” of a Group Action, are equivalence relations (CTfS Exercise 3.2.1.15).
• Generated equivalence relations (CTfS Definition 2.6.1.7): the smallest equivalence relation containing $R\subseteq X\times X$. Drawn in the plane $\mathbb{R}\times \mathbb{R}$, reflexivity is the diagonal, symmetry is mirror symmetry in the diagonal; the relation generated by $\{(1,2),(1,3)\}$ is the diagonal plus the nine points of $\{1,2,3{\}}^2$. On $\mathbb{Z}$, $\{(n,n+1)\}$ generates everything — a single class. For a network, the relation “joined by an edge” generates “in the same connected component”, and the quotient is the set of components (CTfS Exercise 2.6.1.10). The Pushout of $X\stackrel{{\pi }_1}{\leftarrow }R\stackrel{{\pi }_2}{\to }X$ is $X/\sim$ for the equivalence relation generated by $R$ (CTfS Exercise 2.6.2.7).

Union-find (Kittenlab Lecture 9)

For an equivalence relation on $\{1,\dots ,n\}$ generated by declaring pairs equal, the efficient data structure is a union-find storing a forest of representatives. Two elements are equivalent iff they have the same root. This is exactly what is needed to compute pushouts in $\mathbf{FinSet}$.

In compilers and databases

An equivalence relation that is compatible with the operations of an algebra is a Congruence; only congruences can be quotiented by while keeping the algebra, and only congruences license substitution of equals for equals inside programs (E-Graph, Contextual Equivalence).

JuliaLeanHaskell

Docs: Kittenlab Lecture 9

# Kittenlab Lecture 9
struct UnionFind
  parent::Vector{Int}
  UnionFind(n::Int) = new(Vector{Int}(1:n))
end
 
function find_root(uf::UnionFind, i::Int)
  p = uf.parent[i]
  p == i ? i : find_root(uf, p)
end
 
function unite!(uf::UnionFind, i::Int, j::Int)
  iroot, jroot = find_root(uf, i), find_root(uf, j)
  uf.parent[jroot] = iroot
end
 
equivalent(uf, i, j) = find_root(uf, i) == find_root(uf, j)
 
# Catlab uses DataStructures.IntDisjointSets for the same purpose in colimits
using DataStructures
s = IntDisjointSets(5); union!(s, 1, 2); in_same_set(s, 1, 2)  # true

-- Mathlib: `Setoid α` bundles an equivalence relation
example (α : Type) (r : Setoid α) (a : α) : r.r a a := r.iseqv.refl a
#check @Equivalence   -- structure with refl, symm, trans
-- equivalence relations on α ↔ partitions of α
#check @Setoid.partition_iff_setoid

-- an equivalence relation as a predicate satisfying the three laws
type Equiv a = a -> a -> Bool
 
-- e.g. congruence modulo n on Int
modEq :: Int -> Equiv Int
modEq n a b = (a - b) `mod` n == 0
 
-- laws (not enforced): modEq n a a; modEq n a b == modEq n b a;
--   modEq n a b && modEq n b c ==> modEq n a c
-- Data.Equivalence.STT / union-find packages provide the Kittenlab structure