Equivalence Relations

Classical Set Theory

  1. A binary relation \(\star\) on a set \(S\) is the following information: for each \((s,t)\in S^2\) we have a proposition \(s \star t\). An example is the less-than relation \(<\) on \(\mathbb{R}\); for each pair of real numbers \(a\) and \(b\) we have a true-false statement \(a<b\).
  2. Two other equivalent ways of modelling the definition: a binary relation can be thought of as a subset of \(S^2\), the dictionary being that \((s,t)\) is in the subset iff \(s \star t\). Or it could be thought of as a map from \(S^2\) to the set \(\{T,F\}\).
  3. A binary relation \(\sim\) on a set \(S\) is reflexive if
\[\forall s\in S, s\sim s,\]

and it is symmetric if

\[\forall s,t\in S, s \sim t \to t \sim s\]

It is transitive if

\[\forall s, t, u\in S, s \sim t \land t \sim u \to s \sim u,\]

and it is an equivalence relation if it is reflexive, symmetric and transitive. Examples show that none of the three axioms for an equivalence relation can be dropped. For example the binary relation \(\le\) is reflexive and transitive, but not symmetric.

  1. If \(\sim\) is an equivalence relation on \(S\), we may partition \(S\) into disjoint equivalence classes; these form a partition of \(S\). One can check that conversely, from a partition of \(S\) one can construct an equivalence relation, defined by \(s \sim t\) if \(s\) and \(t\) are in the same part of the partition, and these two dictionaries provide two distinct ways of thinking about the same idea.

Universal properties of the quotient

Let S be a set and let \(\star\) be an equivalence relation on S. We would like to characterise the set Q of equivalence classes of S under \(star\) by writing down properties which will determine it uniquely. Here are some which spring to mind.

  1. There is a natural map \(m:S\to Q\).
  2. This map is surjective.
  3. If \(s_1, s_2\in S\) then \(m(s_1)=m(s_2)\) if and only if \(s_1\star s_2\).

One can put all of these properties together to deduce the universal property of Q , which a mathematician would describe thus: “If X is any set, then to give a map \(f:Q\to X\) is to give a map \(g:S\to X\) such that for \(s,t\in S\) , \(s\star t\implies f(s)=f(t)\) . Given f , one defines \(g=m\circ f\) , and one uses the properties above to show that this induces a bijection between the f s and the g s.

Lean’s dependent type theory.

The quotient construction is actually not a standard part of dependent type theory, but mathematicians could get nowhere without it so it has been explicitly added to Lean as a third kind of type – a quotient type.

quot(*)=Q

quot.mk(*)=m

quot.ind