Link Search Menu Expand Document
Math 300

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

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
  refl  : ∀ x, r x x
  symm  : ∀ {x y}, r x y → r y x
  trans : ∀ {x y z}, r x y → r y z → r x z

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

variable (X Y Z : Prop) 

theorem biimp_refl : X ↔ X := ⟨fun h => h,fun h => h⟩ 

theorem biimp_symm (h : X ↔ Y) : Y ↔ X := ⟨h.mpr, h.mp⟩ 

theorem biimp_trans (h₁ : X ↔ Y) (h₂ : Y ↔ Z) : X ↔ Z := 
  ⟨h₂.mp ∘ h₁.mp, h₁.mpr ∘ h₂.mpr⟩

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.