Quotients

In mathematics, we often want to consider objects modulo some form of identification—treating different representatives as essentially the same. This practice leads us naturally to the notion of equivalence relations, which formally define when two elements should be considered indistinguishable for our purposes.

Once we have an equivalence relation, we can group elements into equivalence classes—collections of elements that are all equivalent to each other. The process of forming a new structure out of these equivalence classes is called taking a quotient. Quotients allow us to construct new types that “forget” unnecessary distinctions while preserving the structure we care about.

This chapter introduces the foundations of working with quotients in a formal setting. We begin by reviewing equivalence relations and exploring concrete examples. We then move to the notion of setoids, which package a type together with an equivalence relation—an essential concept in Lean.

Next, we delve into the construction of quotients themselves. We examine how to reason about their elements, understand the projection function from a type to its quotient, and work through illustrative examples.

Finally, we explore how functions behave in the presence of quotient types. Specifically, we study how functions defined on a type can be astricted, coastricted, and biastricted. These ideas are key when reasoning about quotient structures in a type-theoretic setting.

The chapter concludes with exercises to reinforce our understanding and help us apply these concepts.

Equivalence relations

A relation R : A → A → Prop is an equivalence relation if it is Reflexive, Symmetric and Transitive. This is already implemented as Equivalence.

If we #print Equivalence, Lean returns:

structure Equivalence.{u} : {α : Sort u} → (α → α → Prop) → Prop
number of parameters: 2
constructor:
Equivalence.mk : ∀ {α : Sort u} {r : α → α → Prop},
  (∀ (x : α), r x x) → (∀ {x y : α}, r x y → r y x) → (∀ {x y z : α}, r x y → r y z → r x z) → Equivalence r
fields:
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

This structure takes two parameters: a type α : Sort u and a binary relation r : α → α → Prop. It encapsulates the three fundamental properties that define an equivalence relation: reflexivity, symmetry, and transitivity. The Equivalence.mk constructor allows us to create an instance of Equivalence r by providing proofs for these three properties. Specifically, the refl field ensures that every element is related to itself ∀ (x : α), r x x, the symm field guarantees that the relation is symmetric ∀ {x y : α}, r x y → r y x, and the trans field enforces transitivity ∀ {x y z : α}, r x y → r y z → r x z.

Examples of equivalence relations

The diagonal relation

Given a type A, the diagonal relation on A is an equivalence relation on A.

Diagonal.lean

theorem TDiagEqv {A : Type} : Equivalence (@diag A) := {
  refl  := by
    intro a
    exact TDiagRefl
  symm  := by
    intro a1 a2
    exact TDiagSymm
  trans := by
    intro a1 a2 a3
    exact TDiagTrans
}

The total relation

Given a type A, the total relation on A is an equivalence relation on A.

Total.lean

theorem TTotalEqv {A : Type} : Equivalence (@total A) := {
  refl  := by
    intro _
    exact trivial
  symm  := by
    intro a1 a2 _
    exact trivial
  trans := by
    intro a1 a2 a3 _ _
    exact trivial
}

The kernel of a function

We introduce the kernel of a function and demonstrate that it defines an equivalence relation. Given two types A and B and a function f : A → B, we define the kernel of f, denoted as Ker f, as a binary relation on A where two elements a1, a2 : A are related if and only if they have the same image under f, i.e., f a1 = f a2. We then establish that Ker f satisfies the properties of an equivalence relation.

Kernel.lean

def Ker {A B : Type} (f : A → B) : A → A → Prop := by
  intro a1 a2
  exact f a1 = f a2

-- The kernel of a function is an equivalence relation
theorem TKerEqv {A B : Type} {f : A → B} : Equivalence (Ker f) := {
  refl  := by
    intro a
    exact rfl
  symm  := by
    intro a1 a2 h1
    exact h1.symm
  trans := by
    intro a1 a2 a3 h1 h2
    exact h1.trans h2
}

Setoids

A Setoid is a type class that encapsulates an equivalence relation on a given type.

If we #print Setoid, Lean returns

class Setoid.{u} : Sort u → Sort (max 1 u)
number of parameters: 1
constructor:
Setoid.mk : {α : Sort u} → (r : α → α → Prop) → Equivalence r → Setoid α
fields:
r : α → α → Prop
iseqv : Equivalence Setoid.r

Given a type α, a Setoid α consists of a binary relation r : α → α → Prop and a proof that r is an equivalence relation. The constructor Setoid.mk allows defining such structures by providing both the relation and its proof of equivalence. An element of type A Setoid α has two fields, r : α → α → Prop the equivalence relation on α and iseqv : Equivalence Setoid.r, a proof that r is an equivalence relation.

Examples of setoids

Since both the diagonal relation and the total relation are equivalence relations, we can define their corresponding setoids. Additionally, we can construct the setoid associated with the kernel of a function.

The diagonal setoid

Diagonal.lean

instance DiagSetoid {A : Type} : Setoid A := {
  r     := @diag A
  iseqv := TDiagEqv
}

The total setoid

Total.lean

instance TotalSetoid {A : Type} : Setoid A := {
  r     := @total A
  iseqv := TTotalEqv
}

The kernel setoid

Kernel.lean

instance KerSetoid {A B : Type} (f : A → B) : Setoid A := {
  r     := Ker f
  iseqv := TKerEqv
}

Quotients

The significance of Setoid lies in its role in quotienting, where elements of α can be grouped into equivalence classes based on r, leading to the Quotient construction. The Quotient type provides a structured way to form quotient types based on equivalence relations.

If we #print Quotient, Lean returns

def Quotient.{u} : {α : Sort u} → Setoid α → Sort u :=
fun {α} s => Quot Setoid.r

The Quotient type constructs the quotient of a given setoid, encapsulating an equivalence relation on a type. It takes an implicit type α along with an instance of Setoid α, which defines an equivalence relation r on α. By applying Quot Setoid.r, it forms a new type in which elements of α are identified according to r. The resulting type remains in the same universe level Sort u, preserving the type hierarchy of α. Unlike Quot, which can be defined for arbitrary binary relations, Quotient is specifically tailored for equivalence relations, ensuring a structured and well-behaved quotienting mechanism in Lean.

Note that for a type A and an element S of type Setoid Am, the term Quotient S is a type.

Quotient.lean

variable (A : Type)
variable (S : Setoid A)
#check Quotient S

Examples of quotients

With the setoids defined above, we can construct the quotient of a type A by its diagonal relation, the quotient of A by the total relation and the quotient of A by the kernel of a function.

The diagonal quotient

Diagonal.lean

def QDiag {A : Type} := Quotient (@DiagSetoid A)

The total quotient

Total.lean

def Qtotal {A : Type} := Quotient (@TotalSetoid A)

The kernel quotient

Kernel.lean

def QKer {A B : Type} (f : A → B) := Quotient (KerSetoid f)

Elements of a quotient

To create an element of Quotient S, we use the Quotient.mk S a function, which maps an element a : A to its equivalence class, that is, the elements of type A that are related with a.

Quotient.lean

variable (a : A)
#check Quotient.mk S a

Two equivalence classes are equal if and only if their representatives are related by the underlying equivalence relation. First, we use Quotient.exact, which states that if two classes are equal, then their representatives must be related. Conversely, we apply Quotient.sound, which ensures that if two elements are related, then their classes are equal. This result confirms that quotient types faithfully represent equivalence classes, ensuring that equality in the quotient type corresponds precisely to the equivalence relation in the original type.

Equality.lean

theorem TEqQuotient {A : Type} {S : Setoid A} {a1 a2 : A} : 
Quotient.mk S a1 = Quotient.mk S a2 ↔ S.r a1 a2 := by
  apply Iff.intro
  -- Quotient.mk S a1 = Quotient.mk S a2 → Setoid.r a1 a2
  apply Quotient.exact
  -- Setoid.r a1 a2 → Quotient.mk S a1 = Quotient.mk S a2
  apply Quotient.sound

The projection function

The projection function is a function of a type into its quotient: it simply constructs the class of a given element.

Projection.lean

-- The projection function
def pr {A : Type} (S : Setoid A) : A → Quotient S := by
  intro a
  exact Quotient.mk S a

An essential property of quotient types is that every element q of type Quotient S has a representative in A, meaning there exists some a : A such that Quotient.mk S a produces the element q. This property is formalized by Quotient.exists_rep. This proposition implies, in particular, that the projection function is always surjective.

Projection.lean

-- The projection function is surjective
theorem TprSurj {A : Type} (S : Setoid A) : surjective (pr S) := by
  intro q 
  apply Quotient.exists_rep 

Functions and Quotient types

Astriction

We can formalize the notion of astricting functions to quotients. Any function f : A → B can be astricted to a quotient by a setoid S on B by considering classes on the images under f. Astriction provides a way to transform elements of type A → B into elements of type A → Quotient S.

Astriction.lean

def ast {A B : Type} {S : Setoid B} (f : A → B) : A → Quotient S := by
  intro a
  exact Quotient.mk S (f a)

Coastriction

Given a function f : A → B and a setoid R on A, we can coastrict f to Quotient R, provided that every pair related according to the underlying relation of R is also related according to Ker f. For this we will apply the keyword Quotient.lift. If the above condition holds, coastriction provides a way to transform elements of type A → B into elements of type Quotient R → B.

Coastriction.lean

def coast {A B : Type} {R : Setoid A} (f : A → B) (h : ∀ (a1 a2 : A), 
R.r a1 a2 → (Ker f) a1 a2) : Quotient R → B := by
  apply Quotient.lift f
  intro a1 a2 h1
  exact (h a1 a2) h1

Biastriction

Given a function f : A → B, a setoid R on A and a setoid S on B, we can biastrict f to the respective quotient types, provided that if a pair a1 a2 : A is related according to the underlying relation of R then the pair (f a1), (f a2) : B is related according to the underlying relation of S. If the above condition holds, biastriction provides a way to transform elements of type A → B into elements of type Quotient R → Quotient S.

Biastriction.lean

def biast {A B : Type} {R : Setoid A} {S : Setoid B} (f : A → B) 
(h : ∀ (a1 a2 : A), R.r a1 a2 → S.r (f a1) (f a2)) : Quotient R → Quotient S := by
  apply coast (ast f)
  intro a1 a2 hR
  specialize h a1 a2 
  apply Quotient.sound
  exact h hR

In particular, given two setoids R1 and R2 on a type A, the following function establishes a transformation from the type Quotient R1 to the type Quotient R2, provided that the underlying relation of R1 implies the underlying relation of R2. This is achieved by biastricting the identity function.

QuottoQuot.lean

def QuottoQuot {A : Type} {R1 R2 : Setoid A} (h : ∀ (a1 a2 : A), 
R1.r a1 a2 → R2.r a1 a2) : Quotient R1 → Quotient R2 := biast id h

Exercises

Prove that the meet of two equivalence relations is an equivalence relation.

Exercises.lean

instance TMeetEqv {A : Type} {R S : A → A → Prop} (hR : Equivalence R) 
(hS : Equivalence S) : Equivalence (R ∧ S) := by sorry

If two setoids have equivalent underlying relations, the corresponding quotient types are equal.

Exercises.lean

theorem TEqQuotype {A : Type} {R1 R2 : Setoid A}
(h : ∀ (a1 a2 : A), R1.r a1 a2 ↔ R2.r a1 a2) : Quotient R1 = Quotient R2 := by sorry

Prove the The Universal Property of Quotient types, which states that the Kernel of the projection function is precisely the original relation of the setoid.

Exercises.lean

-- Ker (pr R) = R.r
theorem TUPQuot {A : Type} {R : Setoid A} : Ker (pr R) = R.r := by sorry

The astriction ast f is equal to pr ∘ f.

Exercises.lean

theorem TAst {A B : Type} {f : A → B} {S : Setoid B}: (@ast A B S f) = 
(@pr B S) ∘ f := by sorry

Theorems TUPCoast and TUPCoasttUn establish the universal property of the coastriction of a function. The first result, TUPCoast, states that for any function f : A → B that respects a setoid relation R on A (i.e., for every pair a1 a2 : A, if R.r a1 a2 then f a1 = f a2)), the function f can be expressed as the composition of its coastriction coast f h with the projection function pr, that is f = coast ∘ pr. The second result, TUPCoastUn, establishes the uniqueness of the coastriction. If there exists another function g : Quotient R → B such that f = g ∘ pr, then g must be exactly coast f h.

Exercises.lean

-- f = coast ∘ pr
theorem TUPCoast {A B : Type} {R : Setoid A} {f : A → B} (h : ∀ (a1 a2 : A), 
R.r a1 a2 → (Ker f) a1 a2) : f =  (coast f h) ∘ (@pr A R) := by sorry
  
-- Unicity
theorem TUPCoastUn {A B : Type} {R : Setoid A} {f : A → B} (h : ∀ (a1 a2 : A), 
R.r a1 a2 → (Ker f) a1 a2) (g : Quotient R → B) (h1 : f = g ∘ (@pr A R)) : 
(coast f h) = g := by sorry

We next introduce the concept of isomorphic types and establish that, under Classical.choice, isomorphism defines an equivalence relation. We first define Iso A B as the subtype of all functions from A to B that are isomorphisms, meaning they admit a two-sided inverse. Two types A and B are then said to be isomorphic, written A ≅ B, if there exists at least one such isomorphism, formalized as the proposition Nonempty (Iso A B). Prove that being isomorphic is an equivalence relation on Type.

Exercises.lean

-- The subtype of all isomorphisms from a type `A` to a type `B`
def Iso (A B : Type) := {f : A → B // isomorphism f}

-- Two types A and B are isomorphic if there is some isomorphism from `A` to `B`
def Isomorphic : Type → Type → Prop := by
  intro A B
  exact Nonempty (Iso A B)

-- Notation for Isomorphic types (`\cong`)
notation : 65 lhs:65 " ≅ " rhs:66 => Isomorphic lhs rhs

-- Being isomorphic is an equivalence relation
theorem TIsoEqv : Equivalence Isomorphic := by sorry

Assuming Classical.choice, every type A is isomorphic to the quotient of A by the diagonal relation, A / diag.

Exercises.lean

theorem TDiag {A : Type} : A ≅ @QDiag A := by sorry

Under Classical.choice, any two Nonempty types A and B have isomorphic quotients A / Total and B / Total.

Exercises.lean

theorem TTotal {A B : Type} (hA : Nonempty A) (hB : Nonempty B) : 
@Qtotal A ≅ @Qtotal B := by sorry

Assuming Classical.choice prove that, for every function f : A → B, the quotient A / Ker f is isomorphic to Im f.

Exercises.lean

theorem TKerIm {A B : Type} (f : A → B) : QKer f ≅ Im f := by sorry