## Like equality but not equal to it

Another common type of relation is the following.

**Definition**. An *equivalence relation* is a relation $\cong$ that is

- reflexive
- symmetric and
- transitive

Equivalence relations are already built in to Lean’s core code

The prototypical example of an equivalence relation is equality $=$. Here is another example prominent example.

**Example**. Let $m \in \mathbb{Z}$. Given two integers $a,b$, we say $a$ is equivelant to $b$ *modulo* $m$ if $m \mid b-a$. We write $a \equiv b \mod m$ to denote this relation.

Let’s check this is reflexive. To say that $a \equiv a \mod m$, we need, by definition, $m \mid a - a = 0$. But all integers divide $0$: $0 = 0 \cdot m$. So indeed this is reflexive.

For symmetry, assume that $a \equiv b \mod m$. Then there is some $c$ with $b - a = cm$. We also have \(a - b = -(b-a) = -(cm) = (-c)m\) so we have $b \equiv a \mod m$.

Now let’s check transitivity. Assume that $a \equiv b \mod m$ and that $b \equiv c \mod m$. Unfolding the definitions, we have $d_1$ and $d_2$ with \(b - a = d_1 m,~ c - b = d_2 m\) Then \(c - a = c - b + b - a = d_1 m + d_2 m = (d_1+d_2)m\) so $m \mid c -a$.

Another example we have already seen.

**Example**. Bijection of sets is an equivalence relation. For reflexivity, we use that the identity function $\operatorname{id}_X : X \to X$ is a bijection.

Assume that $f : X \to Y$ is a bijection. Then we seen that we have an inverse $f^{-1} : Y \to X$ which is also a bijection. Thus, being in bijection is symmetric.

Finally, given bijections $f: X \to Y$ and $g: Y \to Z$, the composition $g \circ f : X \to Z$ is a bijection giving transitivity.

One last example from the beginning of class.

**Example**. Bi-implication of proposition is an equivalence relation. We need to check

- For all propositional formula $X$, we have $X \leftrightarrow X$.
- If $X \leftrightarrow Y$, then $Y \leftrightarrow X$ for any pair of propositional formula.
- Given $X, Y, Z$ with $X \leftrightarrow Y$ and $Y \leftrightarrow Z$, we have $X \leftrightarrow Z$.

Here are the proofs in Lean

Very often, properties of interest are preserved by an equivalence relation. Mentally, we start to treat equivalent elements as equal even through they are not.

But there is a construction by which equivalence becomes equality.

**Definition**. Let $X$ be a set with an equivalence relation $\cong$. For $x$ in $X$, the *equivalence class* of $x$ is \([x] := \lbrace x^\prime \mid x \cong x^\prime \rbrace\) In other words, $[x]$ is the set of elements that are equivalent to $x$.

**Example**. Let’s take $m = 2$ and consider the equivalence class of $0$ modulo $2$. Say $0 \equiv d \mod 2$ is just saying that $2 \mid d - 0 = d$. Thus, $d \in [0]$ if and only if $d$ is even. Similarly, $d \in [1]$ if and only if $d$ is odd.

**Lemma**. $[x^\prime] = [x]$ if and only if $x \cong x^\prime$.

## **Proof**. (Expand to view)

Assume that $[x^\prime] = [x]$ then $x^\prime \in [x^\prime]$ since $x^\prime \cong x^\prime$ from reflexivity of $\cong$. Then $x^\prime \in [x]$ so by definition $x \cong x^\prime$. Now assume that $x \cong x^\prime$. We have to show that $[x] = [x^\prime]$ as sets. Assume that $y \in [x]$. By definition, we have $x \cong y$. From reflexivity, we have $x^\prime \cong x$. Then transitivity tells us that $x^\prime \cong y$. So by definition $y \in [x^\prime]$. Now assume that $y \in [x^\prime]$. Then $x^\prime \cong y$ be definition. Using transitivity, we get $x \cong y$ and $y \in [x]$. Thus, $[x] = [x^\prime]$ as sets. ■

Using the previous lemma, we learn that $[0]$ and $[1]$ are the only equivalence classes mod $2$. If $d$ is odd, then $[d] = [1]$. If $d$ is even, $[d] = [0]$.

**Definition**. The *quotient* by an equivalence relation $\cong$ is the set of equivalence classes of $\cong$: \(X/\cong := \lbrace [x] \mid x \in X \rbrace\)

The quotient comes with a *quotient function* \(\pi : X \to X/ \cong \\ x \mapsto [x]\)

**Example**. Thus, $\mathbb{Z}/\equiv_2 = \lbrace [0],[1] \rbrace$. More generally, \(\mathbb{Z}/\equiv_m = \lbrace [0], [1], [2], \ldots, [m-1] \rbrace\) Since any integers $a$ can be written as $a = r + qm$ for $0 \leq r < m$. Here $r$ is the remainder under division by $m$.

**Example**. The quotient of `Prop`

by `↔`

is in bijection with the set of truth tables. This follows from completeness and soundness of propositional logic.

The set $X/\cong$ satisfies a *universal property* with respect to functions $f : X/\cong \to Y$. More precisely, we have the following theorem.

**Theorem**. Let $(X,\cong)$ be a set with an equivalence relation. Then, for any function $f : X \to Y$ which satisfies the condition $x \cong x^\prime \to f(x) = f(x^\prime)$, we have a unique function $\overline{f} : X / \cong \to Y$ with $\overline{f} \circ \pi = f$.

## **Proof**. (Expand to view)

First, we tackle uniqueness. Since $\pi$ is surjective, it has a right inverse. Thus, if $\overline{f} \circ \pi = \overline{f}^\prime \circ \pi$, we can compose with the right inverse to get $\overline{f} = \overline{f}^\prime$. Thus, the condition that $\overline{f} \circ \pi = f$ uniquely determines $\overline{f}$ _if_ it exists. To show existence, we "try" to define $\overline{f}([x]) = f(x)$. The essential problem here is that, as we have seen, we can have $[x] = [x^\prime]$, with $x \neq x^\prime$. So from this definition if $x \cong x^\prime$, we also have $\overline{f}([x]) = f(x^\prime)$. So we need to check that if $[x] = [x^\prime]$ that $\overline{f}([x]) = \overline{f}([x^\prime])$. If $[x] = [x^\prime]$, we know that $x \cong x^\prime$. By assumption we have $f(x) = f(x^\prime)$, but this says that $$ \overline{f}([x]) = f(x) = f(x^\prime) = \overline{f}([x^\prime]) $$ and our attempt at a function is actually a well-defined function. ■

The previous theorem says that composing with $\pi$ gives a bijection between the following two sets of functions \(\lbrace g : X/\cong \to Y \rbrace \overset{- \circ \pi}{\to} \lbrace f : X \to Y \mid f(x) = f(x^\prime) \text{ whenever } x \cong x^\prime \rbrace\) Thus, we can understand functions out of $X/\cong$ in terms of data that does not explicitly reference $X/\cong$ itself. This is what is meant by a universal property: the set of functions out of $X/\cong$ to $Y$ are all functions $X \to Y$ satisfies some condition.