Equivalence Relations & Partial Orders

An equivalence relation says that several representations should count as the same abstract object. A partial order says that distinct objects can be no greater than one another without requiring every pair to be comparable. Quotients, dependency graphs, version constraints, inheritance, dataflow, and state-space reduction all depend on knowing which of those two structures is actually present.

Property names are quantified contracts #

Let $R\subseteq A\times A$. The variables below range over all of $A$; they are not assumed distinct.

These words are not interchangeable:

• “not reflexive” means $\exists x\;\neg xRx$; irreflexive means no element relates to itself.
• Antisymmetric does not mean “not symmetric.” Equality is both symmetric and antisymmetric. The subset relation $\subseteq$ is antisymmetric but not symmetric.
• An asymmetric relation is automatically irreflexive. A strict order such as $<$ is asymmetric; a non-strict order such as $\le$ is reflexive and antisymmetric.
• Transitivity never requires $x,y,z$ to be different. Adding that restriction produces a weaker, nonstandard property.

Equivalence relations turn representations into classes #

Reflexivity puts $a$ in its own class. Symmetry makes class membership direction-independent. Transitivity makes overlap collapse into equality:

$$a\sim b \iff [a]=[b].$$

For the forward direction, if $x\in[a]$, then $x\sim a$ and $a\sim b$, so $x\sim b$ and $x\in[b]$; reverse the roles for the other inclusion. For the reverse direction, $a\in[a]=[b]$, so $a\sim b$.

The equivalence–partition theorem #

Every equivalence relation produces the partition

$$A/{\sim}=\{[a]:a\in A\}.$$

The proof has three invariants:

1. $[a]$ is nonempty because $a\sim a$.
2. The classes cover $A$ because every $a$ lies in $[a]$.
3. If $[a]$ and $[b]$ overlap at $x$, then $a\sim x\sim b$, so $a\sim b$ and the classes are equal. Thus unequal classes are disjoint.

Conversely, a partition $\mathcal P$ defines

$$x\sim_{\mathcal P}y \iff \exists P\in\mathcal P\;(x\in P\land y\in P).$$

Coverage and disjointness give each element a unique block. “Same block” is immediately reflexive, symmetric, and transitive. The two constructions undo each other, which is why formal libraries can move between setoids and partitions; Mathlib exposes this correspondence through its setoid/partition API.

flowchart TD
  A["representations in A"]
  E["equivalence test x ~ y"]
  C1["class [a]"]
  C2["class [b]"]
  Q["quotient A / ~<br/>one point per class"]
  A --> E
  E -->|"collect all equivalents"| C1
  E -->|"different class or same class"| C2
  C1 --> Q
  C2 --> Q

The quotient forgets which representative was used but retains the class. That is useful only if later operations cannot observe the discarded difference.

Kernels, fibers, and canonical abstraction #

Every function $f:A\to B$ induces an equivalence relation

$$x\sim_f y \iff f(x)=f(y).$$

Reflexivity, symmetry, and transitivity come directly from equality. Its classes are exactly the nonempty fibers $f^{-1}[\{b\}]$. The map factors as

$$A\xrightarrow{q}A/{\sim_f}\xrightarrow{\bar f}\mathop{\mathrm{ran}}(f),$$

where $q(a)=[a]$ and $\bar f([a])=f(a)$. The second map is bijective:

• it is well-defined because all representatives in $[a]$ have the same $f$-value;
• it is injective because equal outputs mean equal classes;
• it is surjective by the definition of the range.

Well-defined functions on quotients #

Suppose $\sim$ is an equivalence relation on $A$, $\approx$ one on $B$, and we want

$$\bar f:A/{\sim}\to B/{\approx},\qquad \bar f([a])=[f(a)].$$

The formula mentions a representative $a$, so it defines a function only if changing representatives cannot change the output class:

$$a\sim a'\Rightarrow f(a)\approx f(a').$$

This is the compatibility or well-definedness condition. Proving it is mandatory; writing brackets around a formula does not make it true.

The same test governs quotient automata, normalized paths, case-insensitive identifiers, and values modulo a representation invariant.

Orders keep identity but constrain direction #

Preorder

A reflexive, transitive relation. Distinct elements may satisfy both directions.

Partial order

A preorder that is antisymmetric.

Linear or total order

A partial order in which every pair is comparable.

Strict partial order

An irreflexive, transitive relation. It is automatically asymmetric.

For a partial order $\le$, define

$$x<y \iff x\le y\land x\ne y.$$

Conversely, from a strict partial order $<$ define $x\le y$ iff $x=y$ or $x<y$. Under the stated axioms these translations recover the corresponding strict/non-strict views. Formal order libraries make the same distinction: a preorder supplies reflexivity and transitivity, while a partial order adds antisymmetry; see Mathlib's partial-order definitions.

Examples clarify what each axiom does:

Hasse diagrams show only covers #

In a finite poset, $x$ is covered by $y$ when $x<y$ and there is no $z$ with $x<z<y$. A Hasse diagram draws cover edges upward and omits reflexive loops, arrowheads, and edges implied by transitivity.

flowchart BT
  n1["1"] --- n2["2"]
  n1 --- n3["3"]
  n2 --- n4["4"]
  n2 --- n6["6"]
  n3 --- n6
  n4 --- n12["12"]
  n6 --- n12

This is the divisibility order on the divisors of $12$. The missing edge $1\to12$ is not a missing relation: transitivity recovers $1\mid12$. Nodes $4$ and $6$ are incomparable because neither divides the other. A Hasse diagram is therefore a transitive reduction of the order, not the complete adjacency relation.

Least, minimal, bounds, meet, and join #

Let $S$ be a subset of a poset $(P,\le)$.

In the divisibility poset above:

• for $S=\{2,3\}$, both elements are minimal and maximal within $S$, but $S$ has no least or greatest element;
• the lower bounds of $\{4,6\}$ are $\{1,2\}$, so the greatest lower bound is $2$;
• the only upper bound of $\{4,6\}$ within the displayed carrier is $12$, so its least upper bound is $12$.

The distinction is not vocabulary trivia. “Pick any minimal dependency” may admit several safe choices; “the least dependency” asserts a unique element below every other one.

Two canonical examples fix the notation:

• $(\mathcal P(U),\subseteq)$ is a lattice with $X\wedge Y=X\cap Y$ and $X\vee Y=X\cup Y$.
• Positive divisors of $n$, ordered by divisibility, form a lattice with meet $\gcd$ and join $\mathop{\mathrm{lcm}}$.

Not every poset is a lattice. The subposet $\{2,3,6\}$ under divisibility has no meet for $2$ and $3$, because their natural greatest common divisor $1$ is outside the carrier.

From dependency graphs to orders #

A directed dependency graph is not automatically a partial order.

1. Start with a direct-edge relation $R$.
2. Its reflexive-transitive closure $R^*$ means “reachable in zero or more steps” and is always a preorder.
3. If the graph is acyclic, mutual reachability implies equality, so $R^*$ is antisymmetric and therefore a partial order.
4. If cycles exist, distinct vertices in one cycle are mutually reachable; antisymmetry fails.

The repair is principled: define

$$x\sim y \iff xR^*y\land yR^*x.$$

These are the strongly connected components (SCCs). Quotienting by $\sim$ collapses every cycle, and reachability between SCCs is a partial order. The resulting condensation graph is a DAG.

flowchart LR
  a["a"] --> b["b"]
  b --> a
  b --> c["c"]
  c --> d["d"]
  d --> c
  subgraph quotient["SCC quotient"]
    ab["[a,b]"] --> cd["[c,d]"]
  end

The four-state graph contains two cycles. The boxed SCC quotient has two abstract nodes and one directed order relation. This equivalence-then-order pattern is fundamental in module dependency analysis, automata minimization, build scheduling, and fixed-point computation.

Every preorder has a partial-order quotient #

The SCC construction is a special case. For any preorder $\preceq$, define

$$x\sim y \iff x\preceq y\land y\preceq x.$$

This is an equivalence relation:

• reflexivity follows from $x\preceq x$;
• symmetry is built into the conjunction;
• transitivity follows by composing both directions.

Define $[x]\le_q[y]$ iff $x\preceq y$. This is well-defined: if $x'\sim x$ and $y\sim y'$, then

$$x'\preceq x\preceq y\preceq y'.$$

The quotient relation is reflexive and transitive, and if both $[x]\le_q[y]$ and $[y]\le_q[x]$, then $x\sim y$, hence $[x]=[y]$. Antisymmetry has been recovered precisely by identifying the pairs that violated it.

Linear extensions and scheduling #

A linear extension of a finite poset is a total order that preserves every original comparison. Orient each Hasse edge from prerequisite to dependent; any topological ordering of that DAG is a linear extension.

The algorithmic invariant is simple: a node with indegree zero has no unplaced predecessor, so choosing it next cannot violate the partial order. Remove it and repeat. Different choices among currently minimal nodes produce different valid schedules.

Equivalence closure versus transitive closure #

Given an arbitrary relation $R$:

• reflexive closure adds all $(x,x)$;
• symmetric closure adds reversed pairs;
• transitive closure adds positive-length consequences;
• equivalence closure is the least relation containing $R$ that is reflexive, symmetric, and transitive.

For a finite undirected edge list, equivalence closure is exactly “belongs to the same connected component,” which disjoint-set union (union–find) maintains efficiently. For a directed relation, ordinary connected components are not enough: direction matters, so use SCCs for mutual reachability or transitive closure for one-way reachability. Mathlib treats these as distinct formal constructions (ReflGen, SymmGen, TransGen, ReflTransGen, and EqvGen) rather than overloading one word “closure.”

Diagnostic checklist #

Before using a relation as an equivalence or order, test the intended meaning:

1. Are the carrier and relation type fixed? Congruence modulo $n$ on $\mathbb Z$ produces $\mathbb Z/n\mathbb Z$; silently switching the carrier to $\mathbb N$ changes the quotient.
2. Does “same” really satisfy transitivity? “Shares a tag with” is symmetric but need not be transitive.
3. Are partition blocks nonempty, covering, and pairwise disjoint?
4. Is every quotient operation independent of representatives?
5. Does two-way comparability force equality? If not, the structure is a preorder; quotient the mutual pairs.
6. Are incomparable elements allowed? If yes, do not apply linear-order intuitions.
7. Is an element least/greatest, merely minimal/maximal, or only a bound outside the subset?
8. Does a Hasse diagram show cover edges only, with crossings that do not imply junctions?

The decisive habit is to translate each word back into its quantifiers and then search for a smallest counterexample.