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. We then 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. Finally, we explore the notion of the coequalizer of two functions.

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 α 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
}

Equivalence relation generated by a relation

The following Lean code defines the equivalence closure of a relation as an inductive type and proves that it forms an equivalence relation. Specifically, the inductive type Eqvgen constructs the smallest equivalence relation generated by a given relation R : A → A → Prop on a type A. The Eqvgen type is defined with four constructors: base, which includes the original relation R; and refl, symm, and trans, ensuring that Eqvgen R satisfies the properties for reflexivity, symmetry, and transitivity, respectively.

Eqvgen.lean

inductive Eqvgen {A : Type} (R : A → A → Prop) : A → A → Prop where
  | base : ∀ {a1 a2 : A}, (R a1 a2 → Eqvgen R a1 a2)
  | refl : ∀ (a : A), Eqvgen R a a
  | symm : ∀ {a1 a2 : A}, Eqvgen R a1 a2 → Eqvgen R a2 a1
  | trans : ∀ {a1 a2 a3 : A}, (Eqvgen R a1 a2) → (Eqvgen R a2 a3) → (Eqvgen R a1 a3)

-- The equivalence generated by a relation is an equivalence relation
theorem TEqvgen {A : Type} (R : A → A → Prop) : Equivalence (Eqvgen R) := {
  refl  := Eqvgen.refl
  symm  := Eqvgen.symm
  trans := Eqvgen.trans
}

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 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

The diagonal relation, total relation, and a function’s kernel, as equivalence relations, allow us to define their corresponding setoids.

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. 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, 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 A, 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 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

Coequalizer

In this section, we introduce the concept of the coequalizer of two functions, a construction that identifies elements in the codomain where the two functions produce equivalent outputs. Beyond its definition as a quotient type, the coequalizer is characterized by a universal property: it serves as the most general type equipped with a map from B that makes the two functions agree.

Given two functions f, g : A → B, the coequalizer of f and g is the quotient of B by the equivalence relation generated by identifying f a with g a for all a : A.

Coequalizer.lean

-- We define the relation on B relating elements of the form f a and g a for some a : A
def CoeqRel {A B : Type} (f g : A → B) : B → B → Prop := by
  intro b1 b2
  exact ∃ (a : A), (f a = b1) ∧ (g a = b2)

-- We next consider the equivalence relation generated by the previous relation
def CoeqEqv {A B : Type} (f g : A → B) := Eqvgen (CoeqRel f g)

-- The coequalizer setoid
instance CoeqSetoid {A B : Type} (f g : A → B): Setoid B := {
  r     := CoeqEqv f g
  iseqv := TEqvgen (CoeqRel f g)
}

-- The coequalizer Coeq f g
def Coeq {A B : Type} (f g : A → B) : Type := Quotient (CoeqSetoid f g)

It comes equipped with the quotient map from B to the coequalizer.

Coequalizer.lean

def prCoeq {A B : Type} (f g : A → B) : B → Coeq f g := @pr B (CoeqSetoid f g)

This projection satisfies that (prCoeq f g) ∘ f = (prCoeq f g) ∘ g.

Coequalizer.lean

theorem TCoeqPr {A B : Type} (f g : A → B) : (prCoeq f g) ∘ f = (prCoeq f g) ∘ g := by
  apply funext
  intro a
  apply Quotient.sound
  apply Eqvgen.base
  apply Exists.intro a
  apply And.intro
  exact rfl
  exact rfl

Universal property of the coequalizer

The universal property of the coequalizer characterizes it not merely as a quotient type, but as a universal solution to the problem of mediating between f and g. The universal property states that the pair (Coeq f g, prCoeq f g) is final among all pairs (C, h), where C is a type and h : B → C is a function satisfying h ∘ f = h ∘ g.

That is, if C is a type and h : B → C is a function satisfying h ∘ f = h ∘ g, then there exists a unique function u : (Coeq f g) → C such that u ∘ (prCoeq f g) = h.

Coequalizer.lean

-- If there is another function h : B → C satisfying h ∘ f = h ∘ g, then there exists a function u : Coeq f g → C
def u {A B C : Type} {f g : A → B} {h : B → C} (h1 : h ∘ f = h ∘ g) : Coeq f g → C := by
  apply Quotient.lift h
  intro b1 b2 h2
  induction h2
  -- Base case
  rename_i c1 c2 h2
  apply Exists.elim h2
  intro a ⟨h2, h3⟩
  calc
    h c1  = h (f a)   := congrArg h (h2.symm)
    _     = (h ∘ f) a := rfl
    _     = (h ∘ g) a := congrFun h1 a
    _     = h (g a)   := rfl
    _     = h c2      := congrArg h h3
  -- Rfl Case
  rename_i c
  exact rfl
  -- Symm Case
  rename_i c1 c2 _ h3
  exact h3.symm
  -- Trans Case
  rename_i c1 c2 c3 _ _ h4 h5
  exact h4.trans h5

-- The function u satisfies that u ∘ prCoeq f g = h
theorem TCoeqPrEq {A B C : Type} {f g : A → B} {h : B → C} (h1 : h ∘ f = h ∘ g) : (u h1) ∘ (prCoeq f g) = h := by
  apply funext
  intro b
  exact rfl

-- The function u is unique in the sense that if there is another function
-- v : Coeq f g → C satisfying v ∘ (prCoeq f g) = h, then v = u
theorem TCoeqUni {A B C : Type} {f g : A → B} {h : B → C} (h1 : h ∘ f = h ∘ g) (v : Coeq f g → C) (h2 : v ∘ (prCoeq f g) = h) : v = u h1 := by
  apply funext
  intro z
  have h3 : ∃ (b : B), Quotient.mk (CoeqSetoid f g) b = z := Quotient.exists_rep z
  apply Exists.elim h3
  intro b h4
  calc
    v z = v (prCoeq f g b)                        := congrArg v (h4.symm)
    _   = (v ∘ prCoeq f g) b                      := rfl
    _   = h b                                     := congrFun h2 b
    _   = ((u h1) ∘ (prCoeq f g)) b               := congrFun (TCoeqPrEq h1) b
    _   = (u h1) (prCoeq f g b)                   := rfl
    _   = (u h1) z                                := congrArg (u h1) (h4)

In other words, any function from B that “coequalizes” f and g factors uniquely through the coequalizer. This property ensures that the coequalizer is the most general and canonical way to capture the quotient where the images the two functions are identified.

Exercises

Equivalences

Exercises.lean

-- The meet of two equivalence relations is an equivalence relation
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
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

Astriction

Exercises.lean

-- The astriction ast f is equal to pr ∘ f.
theorem TAst {A B : Type} {f : A → B} {S : Setoid B}: (@ast A B S f) = 
(@pr B S) ∘ f := by sorry

Coastriction

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

Isomorphisms

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

Coequalizers

Exercises.lean

-- The function prCoeq is an epimorphism
theorem TprCoeqEpi {A B : Type} {f g : A → B} : epimorphism (prCoeq f g) := by sorry
  
-- A monic prCoeq is an isomorphism
theorem TprCoeqMon {A B : Type} {f g : A → B} : monomorphism (prCoeq f g) → isomorphism (prCoeq f g) := by sorry