10. Relations
Just as sets provide a convenient language for properties of the objects in a type, relations provide a convenient language for the properties of the pairs of objects in a type. This might sound dry and abstract, but such properties turn up all over mathematics: the property of one real number being less than another; the property of one integer being congruent to another modulo 5; the property of one set being a subset of another; the property of one function being inverse to another.
In this chapter we introduce some of the important properties which relations themselves can have: they can be reflexive, symmetric, antisymmetric or transitive, or any combination of these.
10.1. Reflexive, symmetric, antisymmetric, transitive
10.1.1. Example
Definition
A relation \(\sim\) on a type \(X\) is reflexive, if for all \(x\) of type \(X\), it is true that \(x\sim x\).
Problem
Prove that the relation \(|\) on \(\mathbb{N}\) is reflexive.
Solution
We must show that for all natural numbers \(x\), \(x\mid x\). Indeed, let \(x\) be a natural number; then \(x=x\cdot 1\).
example : Reflexive ((·:ℕ) ∣ ·) := by
dsimp [Reflexive]
intro x
use 1
ring
Definition
A relation \(\sim\) on a type \(X\) is symmetric, if for all \(x\) and \(y\) of type \(X\), if \(x\sim y\), then \(y\sim x\).
Problem
Prove that the relation \(|\) on \(\mathbb{N}\) is not symmetric.
Solution
We must show that there exist natural numbers \(x\) and \(y\) such that, \(x\mid y\) and \(y\mid x\). Indeed, we have \(2=1\cdot 2\), so \(1\mid 2\), and \(2\cdot 0<1<2\cdot 1\), so \(2\not \mid 1\).
example : ¬ Symmetric ((·:ℕ) ∣ ·) := by
dsimp [Symmetric]
push_neg
use 1, 2
constructor
· use 2
numbers
· apply Nat.not_dvd_of_exists_lt_and_lt
use 0
constructor
· numbers
· numbers
Definition
A relation \(\sim\) on a type \(X\) is antisymmetric, if for all \(x\) and \(y\) of type \(X\), if \(x\sim y\) and \(y\sim x\), then \(x=y\).
Problem
Prove that the relation \(|\) on \(\mathbb{N}\) is antisymmetric.
Solution
We first note the following fact (\(\star\)): if \(m\) and \(n\) are natural numbers with \(m=0\) and \(m\mid n\), then \(m=n\). Indeed, since \(m\mid n\) there exists a natural number \(k\) such that \(n=mk\), and then
We now return to the original problem. We must show that for all natural numbers \(x\) and \(y\), if \(x\mid y\) and \(y\mid x\), then \(x=y\). Indeed, let \(x\) and \(y\) be natural numbers and suppose \(x\mid y\) and \(y\mid x\). If \(x=0\) then by (\(\star\)) we are done; likewise if \(y=0\). Otherwise, \(x>0\), so since \(y\mid x\) we have \(y\le x\), and \(y>0\), so since \(x\mid y\) we have \(x\le y\), Putting these together, \(x=y\).
example : AntiSymmetric ((·:ℕ) ∣ ·) := by
have H : ∀ {m n}, m = 0 → m ∣ n → m = n
· intro m n h1 h2
obtain ⟨k, hk⟩ := h2
calc m = 0 := by rw [h1]
_ = 0 * k := by ring
_ = m * k := by rw [h1]
_ = n := by rw [hk]
dsimp [AntiSymmetric]
intro x y h1 h2
obtain hx | hx := Nat.eq_zero_or_pos x
· apply H hx h1
obtain hy | hy := Nat.eq_zero_or_pos y
· have : y = x := by apply H hy h2
rw [this]
apply le_antisymm
· apply Nat.le_of_dvd hy h1
· apply Nat.le_of_dvd hx h2
Definition
A relation \(\sim\) on a type \(X\) is transitive, if for all \(x\), \(y\) and \(z\) of type \(X\), if \(x\sim y\) and \(y\sim z\), then \(x\sim z\).
Problem
Prove that the relation \(|\) on \(\mathbb{N}\) is transitive.
Solution
We must show that for all natural numbers \(a\), \(b\) and \(c\), if \(a\mid b\) and \(b\mid c\) then \(a\mid c\).
Indeed, let \(a\), \(b\) and \(c\) be natural numbers with these properties. Since \(a\mid b\) there exists a natural number \(k\) such that \(b=ak\), and since \(b\mid c\) there exists a natural number \(l\) such that \(c=bl\). We then have
so \(a\mid c\).
example : Transitive ((·:ℕ) ∣ ·) := by
dsimp [Transitive]
intro a b c hab hbc
obtain ⟨k, hk⟩ := hab
obtain ⟨l, hl⟩ := hbc
use k * l
calc c = b * l := by rw [hl]
_ = (a * k) * l := by rw [hk]
_ = a * (k * l) := by ring
10.1.2. Example
Problem
Determine which of these properties hold for the relation \(=\) on \(\mathbb{R}\):
reflexive;
symmetric;
antisymmetric;
transitive.
example : Reflexive ((·:ℝ) = ·) := by
dsimp [Reflexive]
intro x
ring
example : Symmetric ((·:ℝ) = ·) := by
dsimp [Symmetric]
intro x y h
rw [h]
example : AntiSymmetric ((·:ℝ) = ·) := by
dsimp [AntiSymmetric]
intro x y h1 h2
rw [h1]
example : Transitive ((·:ℝ) = ·) := by
dsimp [Transitive]
intro x y z h1 h2
rw [h1, h2]
10.1.3. Example
Problem
Determine which of these properties hold for the relation \(\sim\) on \(\mathbb{R}\), defined by, \(x\sim y\) if \((x-y)^2\leq 1\):
reflexive;
symmetric;
antisymmetric;
transitive.
local infix:50 "∼" => fun (x y : ℝ) ↦ (x - y) ^ 2 ≤ 1
example : Reflexive (· ∼ ·) := by
dsimp [Reflexive]
intro x
calc (x - x) ^ 2 = 0 := by ring
_ ≤ 1 := by numbers
example : Symmetric (· ∼ ·) := by
dsimp [Symmetric]
intro x y h
calc (y - x) ^ 2 = (x - y) ^ 2 := by ring
_ ≤ 1 := by rel [h]
example : ¬ AntiSymmetric (· ∼ ·) := by
dsimp [AntiSymmetric]
push_neg
use 1, 1.1
constructor
· numbers
constructor
· numbers
· numbers
example : ¬ Transitive (· ∼ ·) := by
dsimp [Transitive]
push_neg
use 1, 1.9, 2.5
constructor
· numbers
constructor
· numbers
· numbers
10.1.4. Example
Consider the following finite inductive type Hand.
inductive Hand
| rock
| paper
| scissors
Consider the following relation \(\prec\) on the Hand type.
@[reducible] def r : Hand → Hand → Prop
| rock, rock => False
| rock, paper => True
| rock, scissors => False
| paper, rock => False
| paper, paper => False
| paper, scissors => True
| scissors, rock => True
| scissors, paper => False
| scissors, scissors => False
local infix:50 " ≺ " => r
Problem
Determine which of these properties hold for the relation \(\prec\):
reflexive;
symmetric;
antisymmetric;
transitive.
example : ¬ Reflexive (· ≺ ·) := by
dsimp [Reflexive]
push_neg
use rock
exhaust
example : ¬ Symmetric (· ≺ ·) := by
dsimp [Symmetric]
push_neg
use rock, paper
exhaust
example : AntiSymmetric (· ≺ ·) := by
dsimp [AntiSymmetric]
intro x y
cases x <;> cases y <;> exhaust
example : ¬ Transitive (· ≺ ·) := by
dsimp [Transitive]
push_neg
use rock, paper, scissors
exhaust
10.1.5. Exercises
Show that the relation \(<\) on \(\mathbb{R}\) is not symmetric.
example : ¬ Symmetric ((·:ℝ) < ·) := by sorry
Show that the relation \(\sim\) on \(\mathbb{Z}\), defined by, \(x\sim y\) if \(x\equiv y \mod 2\), is not antisymmetric.
local infix:50 "∼" => fun (x y : ℤ) ↦ x ≡ y [ZMOD 2] example : ¬ AntiSymmetric (· ∼ ·) := by sorry
Consider the following finite inductive type Little, and the following relation \(\sim\) on the Little type. Determine which of these properties hold for the relation \(\sim\):
reflexive;
symmetric;
antisymmetric;
transitive.
section inductive Little | meg | jo | beth | amy deriving DecidableEq open Little @[reducible] def s : Little → Little → Prop | meg, meg => True | meg, jo => True | meg, beth => True | meg, amy => True | jo, meg => True | jo, jo => True | jo, beth => True | jo, amy => False | beth, meg => True | beth, jo => True | beth, beth => False | beth, amy => True | amy, meg => True | amy, jo => False | amy, beth => True | amy, amy => True local infix:50 " ∼ " => s
example : Reflexive (· ∼ ·) := by sorry example : ¬ Reflexive (· ∼ ·) := by sorry example : Symmetric (· ∼ ·) := by sorry example : ¬ Symmetric (· ∼ ·) := by sorry example : AntiSymmetric (· ∼ ·) := by sorry example : ¬ AntiSymmetric (· ∼ ·) := by sorry example : Transitive (· ∼ ·) := by sorry example : ¬ Transitive (· ∼ ·) := by sorry
Determine which of these properties hold for the relation \(\sim\) on \(\mathbb{Z}\), defined by, \(x\sim y\) if \(y\equiv x+1\mod 5\):
reflexive;
symmetric;
antisymmetric;
transitive.
Also sketch (a representative portion of) this relation as a directed graph.
local infix:50 "∼" => fun (x y : ℤ) ↦ y ≡ x + 1 [ZMOD 5] example : Reflexive (· ∼ ·) := by sorry example : ¬ Reflexive (· ∼ ·) := by sorry example : Symmetric (· ∼ ·) := by sorry example : ¬ Symmetric (· ∼ ·) := by sorry example : AntiSymmetric (· ∼ ·) := by sorry example : ¬ AntiSymmetric (· ∼ ·) := by sorry example : Transitive (· ∼ ·) := by sorry example : ¬ Transitive (· ∼ ·) := by sorry
Determine which of these properties hold for the relation \(\sim\) on \(\mathbb{Z}\), defined by, \(x\sim y\) if \(x+y\equiv 0\mod 3\):
reflexive;
symmetric;
antisymmetric;
transitive.
Also sketch (a representative portion of) this relation as a directed graph.
local infix:50 "∼" => fun (x y : ℤ) ↦ x + y ≡ 0 [ZMOD 3] example : Reflexive (· ∼ ·) := by sorry example : ¬ Reflexive (· ∼ ·) := by sorry example : Symmetric (· ∼ ·) := by sorry example : ¬ Symmetric (· ∼ ·) := by sorry example : AntiSymmetric (· ∼ ·) := by sorry example : ¬ AntiSymmetric (· ∼ ·) := by sorry example : Transitive (· ∼ ·) := by sorry example : ¬ Transitive (· ∼ ·) := by sorry
Determine which of these properties hold for the relation \(\subseteq\) on \(\mathcal{P}(\mathbb{N})\), the type of sets of natural numbers.
reflexive;
symmetric;
antisymmetric;
transitive.
Also sketch (a representative portion of) this relation as a directed graph.
example : Reflexive ((· : Set ℕ) ⊆ ·) := by sorry example : ¬ Reflexive ((· : Set ℕ) ⊆ ·) := by sorry example : Symmetric ((· : Set ℕ) ⊆ ·) := by sorry example : ¬ Symmetric ((· : Set ℕ) ⊆ ·) := by sorry example : AntiSymmetric ((· : Set ℕ) ⊆ ·) := by sorry example : ¬ AntiSymmetric ((· : Set ℕ) ⊆ ·) := by sorry example : Transitive ((· : Set ℕ) ⊆ ·) := by sorry example : ¬ Transitive ((· : Set ℕ) ⊆ ·) := by sorry
Determine which of these properties hold for the relation \(\prec\) on \(\mathbb{R}^2\), defined by, \((x_1, y_1) \prec (x_2,y_2)\) if \(x_1\le x_2\) and \(y_1\le y_2\):
reflexive;
symmetric;
antisymmetric;
transitive.
local infix:50 "≺" => fun ((x1, y1) : ℝ × ℝ) (x2, y2) ↦ (x1 ≤ x2 ∧ y1 ≤ y2) example : Reflexive (· ≺ ·) := by sorry example : ¬ Reflexive (· ≺ ·) := by sorry example : Symmetric (· ≺ ·) := by sorry example : ¬ Symmetric (· ≺ ·) := by sorry example : AntiSymmetric (· ≺ ·) := by sorry example : ¬ AntiSymmetric (· ≺ ·) := by sorry example : Transitive (· ≺ ·) := by sorry example : ¬ Transitive (· ≺ ·) := by sorry
10.2. Equivalence relations
10.2.1. Example
Definition
A relation is an equivalence relation, if it is reflexive, symmetric and transitive.
Problem
Let \(n\) be an integer. Show that the relation \(\sim\) on \(\mathbb{Z}\) defined by, \(x\sim y\) if \(x\equiv y\mod n\) is an equivalence relation.
Solution
By Example 3.3.10, the relation \(\sim\) is reflexive.
By two of the exercises to Section 3.3, the relation \(\sim\) is symmetric and transitive.
variable (n : ℤ)
local infix:50 "∼" => fun (x y : ℤ) ↦ x ≡ y [ZMOD n]
example : Reflexive (· ∼ ·) := by
dsimp [Reflexive]
apply Int.ModEq.refl
example : Symmetric (· ∼ ·) := by
dsimp [Symmetric]
apply Int.ModEq.symm
example : Transitive (· ∼ ·) := by
dsimp [Transitive]
apply Int.ModEq.trans
Let’s sketch (a portion of) this relation as a directed graph, say for \(n=3\).
It’s a mess, but it’s just possible to make out a pattern: the numbers form cliques, with, for example, … -5, -2, 1, 4, 7, … all connected to each other and to nothing else. We introduce the following visual shorthand for such a directed graph: when nodes are given different colours, this represents the directed graph in which all nodes of a given colour are connected bi-directionally to all nodes of that colour (including themselves) and to no other nodes.
10.2.2. Example
Problem
Show that the relation \(\sim\) on \(\mathbb{Z}\) defined by \(a\sim b\) if \(a^2=b^2\) is an equivalence relation.
Solution
For all integers \(x\), we have \(x^2=x^2\), so \(x\sim x\). Therefore the relation \(\sim\) is reflexive.
For all integers \(x\) and \(y\), we have that if \(x\sim y\) then \(x^2=y^2\), so \(y^2=x^2\), so \(y\sim z\). Therefore the relation \(\sim\) is symmetric.
For all integers \(x\), \(y\) and \(z\), we have that if \(x\sim y\) and \(y\sim z\) then \(x^2=y^2\) and \(y^2=z^2\), so
so \(x\sim z\). Therefore the relation \(\sim\) is transitive.
local infix:50 "∼" => fun (x y : ℤ) ↦ x ^ 2 = y ^ 2
example : Reflexive (· ∼ ·) := by
dsimp [Reflexive]
intro x
ring
example : Symmetric (· ∼ ·) := by
dsimp [Symmetric]
intro x y hxy
rw [hxy]
example : Transitive (· ∼ ·) := by
dsimp [Transitive]
intro x y z hxy hyz
calc x ^ 2 = y ^ 2 := by rw [hxy]
_ = z ^ 2 := by rw [hyz]
If you try to sketch the directed graph for this relation, you will see that it has the same “clique” behaviour as the previous relation. After sketching the directed graph, sketch the multicoloured “clique” version.
10.2.3. Example
You have probably guessed that the colouring can be made consistent in this way for any equivalence relation. Let’s make this mathematically rigorous.
Let \(r\) be a relation on a type \(\alpha\), denoted \(\sim\) in infix notation.
Definition
For \(a\) in \(\alpha\), the equivalence class of \(a\) (denoted \([a]\)) is \(\{b:\alpha\mid a\sim b\}\).
Theorem
If the relation \(r\) is symmetric and transitive, then for all \(a_1\) and \(a_2\), if \(a_1\sim a_2\), then \([a_1]=[a_2]\).
Proof
We must show that for all \(b\) in \(\alpha\), \(a_1\sim b\) if and only if \(a_2\sim b\).
First, suppose that \(a_1\sim b\). Since \(a_1\sim a_2\), by symmetry \(a_2\sim a_1\), and so by transitivity \(a_2\sim a_1\sim b\).
Conversely, suppose that \(a_2\sim b\). Then since \(a_1\sim a_2\), by transitivity \(a_1\sim a_2\sim b\).
notation:arg "⦍" a "⦐" => { b | a ∼ b }
theorem EquivalenceClass.eq_of_rel (h_symm : @Symmetric α r) (h_trans : @Transitive α r)
{a1 a2 : α} (ha : a1 ∼ a2) :
⦍a1⦐ = ⦍a2⦐ := by
ext b
dsimp
constructor
· intro ha1b
apply h_trans (y := a1)
· apply h_symm ha
· apply ha1b
· intro ha2b
apply h_trans ha ha2b
Theorem
If the relation \(r\) is reflexive, then every \(a\) is an element of its own equivalence class: \(a\in [a]\).
Proof
We must show that for all \(a\), it is true that \(a\sim a\), and this is the definition of reflexivity.
theorem EquivalenceClass.mem_self (h_refl : @Reflexive α r) (a : α) :
a ∈ { b : α | a ∼ b } := by
dsimp
apply h_refl
10.2.4. Example
Consider the relation \(=\) on \(\mathbb{Z}\). It is an equivalence relation, by Example 10.1.2.
Exercise: Sketch this relation, by drawing (a portion of) the underlying type \(\mathbb{Z}\) along a line, then colouring each equivalence class in a different colour.
10.2.5. Example
Problem
Show that the relation \(\sim\) on \(\mathbb{Z}\times\mathbb{N}\) defined by, \((a,b)\sim(c,d)\) if \(a(d+1)=c(b+1)\), is an equivalence relation.
Solution
For all \((a,b)\) in \(\mathbb{Z}\times\mathbb{N}\), \(a(b+1)=a(b+1)\), so \((a,b)\sim (a,b)\). Therefore \(\sim\) is reflexive.
For all \((a,b)\) and \((c,d)\) in \(\mathbb{Z}\times\mathbb{N}\), if \((a,b)\sim (c,d)\) then \(a(d+1)=c(b+1)\), so \(c(b+1)=a(d+1)\), so \((c,d)\sim (a,b)\). Therefore \(\sim\) is symmetric.
For all \((a,b)\), \((c,d)\) and \((e,f)\) in \(\mathbb{Z}\times\mathbb{N}\), if \((a,b)\sim (c,d)\) and \((c,d)\sim (e,f)\) then \(a(d+1)=c(b+1)\) and \(c(f+1)=e(d+1)\). We will show that \(a(f+1)=e(b+1)\), which will imply that \((a,b)\sim (e,f)\), which proves the transitivity of \(\sim\).
Since \(d+1>0\), it suffices to prove that \((d+1)\left[a(f+1)\right]=(d+1)\left[e(b+1)\right]\). Let \(B:= b+1\), \(D:= d+1\), and \(F:= f+1\): then we know that \(aD=cB\) and \(cF=eD\) and need to prove that \(D(aF)=D(eB)\).
Indeed,
local infix:50 "∼" => fun ((a, b) : ℤ × ℕ) (c, d) ↦ a * (d + 1) = c * (b + 1)
example : Reflexive (· ∼ ·) := by
dsimp [Reflexive]
intro (a, b)
dsimp
example : Symmetric (· ∼ ·) := by
dsimp [Symmetric]
intro (a, b) (c, d) h
dsimp at *
rw [h]
example : Transitive (· ∼ ·) := by
dsimp [Transitive]
intro (a, b) (c, d) (e, f) h1 h2
dsimp at *
set B := (b:ℤ) + 1
set D := (d:ℤ) + 1
set F := (f:ℤ) + 1
have :=
calc D * (a * F) = (a * D) * F := by ring
_ = (c * B) * F := by rw [h1]
_ = (c * F) * B := by ring
_ = (e * D) * B := by rw [h2]
_ = D * (e * B) := by ring
cancel D at this
Now, sketch the relation \(\sim\), by drawing (a portion of) the underlying type \(\mathbb{Z}\times\mathbb{N}\) in the plane, then colouring each equivalence class in a different colour.
10.2.6. Example
Theorem
The relation \(\sim\) on the type of level-0 types defined by, \(\alpha\sim\beta\) if there exists a bijective function \(f:\alpha\to\beta\), is an equivalence relation.
local infix:50 "∼" => fun (α β : Type) ↦ ∃ f : α → β, Bijective f
example : Reflexive (· ∼ ·) := by
dsimp [Reflexive]
intro α
use id
rw [bijective_iff_exists_inverse]
use id
constructor
· rfl
· rfl
example : Symmetric (· ∼ ·) := by
dsimp [Symmetric]
intro α β h
obtain ⟨f, hf⟩ := h
rw [bijective_iff_exists_inverse] at hf
obtain ⟨g, hfg1, hfg2⟩ := hf
use g
rw [bijective_iff_exists_inverse]
use f
constructor
· apply hfg2
· apply hfg1
example : Transitive (· ∼ ·) := by
dsimp [Transitive]
intro α β γ h1 h2
obtain ⟨f1, hf1a, hf1b⟩ := h1
obtain ⟨f2, hf2a, hf2b⟩ := h2
use f2 ∘ f1
constructor
· apply Injective.comp
· apply hf2a
· apply hf1a
· apply Surjective.comp
· apply hf2b
· apply hf1b
10.2.7. Exercises
Consider the relation \(\sim\) on \(\mathbb{Z}\) defined by, \(a\sim b\) if there exist positive integers \(m\) and \(n\) such that \(am=bn\).
Show that \(\sim\) is an equivalence relation.
Sketch the relation \(\sim\), by drawing (a portion of) the underlying type \(\mathbb{Z}\) along a line, then colouring each equivalence class in a different colour.
local infix:50 "∼" => fun (a b : ℤ) ↦ ∃ m n, m > 0 ∧ n > 0 ∧ a * m = b * n example : Reflexive (· ∼ ·) := by sorry example : Symmetric (· ∼ ·) := by sorry example : Transitive (· ∼ ·) := by sorry
Consider the relation \(\sim\) on \(\mathbb{N}^2\) defined by, \((a,b)\sim(c,d)\) if \(a+d=b+c\).
Show that \(\sim\) is an equivalence relation.
Sketch the relation \(\sim\), by drawing (a portion of) the underlying type \(\mathbb{N}^2\) in the plane, then colouring each equivalence class in a different colour.
local infix:50 "∼" => fun ((a, b) : ℕ × ℕ) (c, d) ↦ a + d = b + c example : Reflexive (· ∼ ·) := by sorry example : Symmetric (· ∼ ·) := by sorry example : Transitive (· ∼ ·) := by sorry
Consider the relation \(\sim\) on \(\mathbb{Z}^2\) defined by, \((a,b)\sim(c,d)\) if there exist positive integers \(m\) and \(n\) with \(mb(b^2-3a^2)=nd(d^2-3c^2)\).
Show that \(\sim\) is an equivalence relation.
Sketch the relation \(\sim\), by drawing (a portion of) the underlying type \(\mathbb{Z}^2\) in the plane, then colouring each equivalence class in a different colour.
local infix:50 "∼" => fun ((a, b) : ℤ × ℤ) (c, d) ↦ ∃ m n, m > 0 ∧ n > 0 ∧ m * b * (b ^ 2 - 3 * a ^ 2) = n * d * (d ^ 2 - 3 * c ^ 2) example : Reflexive (· ∼ ·) := by sorry example : Symmetric (· ∼ ·) := by sorry example : Transitive (· ∼ ·) := by sorry