quiz: the smallest equivalence relation of `r`

Stream: lean4

[Bulhwi Cha]

Quiz: read the following excerpt from Section Quotients of #tpil4 and prove the theorems below.

universe u
#check (Quot.sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α},
  r a b → Quot.mk r a = Quot.mk r b)

This is the axiom that asserts that any two elements of α that are related by r become identified in the quotient. If a theorem or definition makes use of Quot.sound, it will show up in the #print axioms command.

Of course, the quotient construction is most commonly used in situations when r is an equivalence relation. Given r as above, if we define r' according to the rule r' a b iff Quot.mk r a = Quot.mk r b, then it's clear that r' is an equivalence relation. Indeed, r' is the kernel of the function a ↦ Quot.mk r a. The axiom Quot.sound says that r a b implies r' a b. Using Quot.lift and Quot.ind, we can show that r' is the smallest equivalence relation containing r, in the sense that if r'' is any equivalence relation containing r, then r' a b implies r'' a b. In particular, if r was an equivalence relation to start with, then for all a and b we have r a b iff r' a b.

import Mathlib.Logic.Basic
namespace Quot

-- `Ker r` is the *kernel* of the function `a ↦ Quot.mk r a`
def Ker {α : Type u} (r : α → α → Prop) : α → α → Prop :=
  sorry

-- `Ker r` is an equivalence relation
theorem Ker_is_equivalence {α : Type u} (r : α → α → Prop) : Equivalence (Ker r) where
  refl  := sorry
  symm  := sorry
  trans := sorry

-- `Ker r` is the smallest equivalence relation containing `r`
theorem Ker_is_smallest {α : Type u} {r r' : α → α → Prop} (eqv_r' : Equivalence r')
    (sub_r_r' : Subrelation r r') : Subrelation (Ker r) r' := by
  sorry

-- if `r` is an equivalence relation, then `r = Ker r`
theorem eqv_eq_Ker {α : Type u} {r : α → α → Prop} (eqv_r : Equivalence r) : r = Ker r :=
  sorry

end Quot

Solutions

import Mathlib.Logic.Basic
namespace Quot

-- `Ker r` is the *kernel* of the function `a ↦ Quot.mk r a`
def Ker {α : Type u} (r : α → α → Prop) : α → α → Prop :=
  fun a b : α ↦ Quot.mk r a = Quot.mk r b

-- `Ker r` is an equivalence relation
theorem Ker_is_equivalence {α : Type u} (r : α → α → Prop) : Equivalence (Ker r) where
  refl  := fun _ : α ↦ rfl
  symm  := fun {a b : α} (krab : Ker r a b) ↦ krab.symm
  trans := fun {a b c : α} (krab : Ker r a b) (krbc : Ker r b c) ↦ krab.trans krbc

-- `Ker r` is the smallest equivalence relation containing `r`
theorem Ker_is_smallest {α : Type u} {r r' : α → α → Prop} (eqv_r' : Equivalence r')
    (sub_r_r' : Subrelation r r') : Subrelation (Ker r) r' := by
  intro a b krab
  have respect_r (a₁ a₂ : α) (ra₁a₂ : r a₁ a₂) : r' a₁ b = r' a₂ b :=
    propext ⟨fun r'a₁b ↦ eqv_r'.trans (eqv_r'.symm (sub_r_r' ra₁a₂)) r'a₁b,
      fun r'a₂b ↦ eqv_r'.trans (sub_r_r' ra₁a₂) r'a₂b⟩
  show Quot.lift (fun a : α ↦ r' a b) respect_r (Quot.mk r a)
  rw [krab]
  show r' b b
  exact eqv_r'.refl b

-- if `r` is an equivalence relation, then `r = Ker r`
theorem eqv_eq_Ker {α : Type u} {r : α → α → Prop} (eqv_r : Equivalence r) : r = Ker r :=
  have sub_eqv_Ker : Subrelation r (Ker r) := sound
  have sub_Ker_eqv : Subrelation (Ker r) r := Ker_is_smallest eqv_r id
  funext₂ (fun _ _ : α ↦ propext ⟨sub_eqv_Ker, sub_Ker_eqv⟩)

end Quot

[Bulhwi Cha]

The theorem Ker_is_smallest was much harder to prove than I thought.