Example of an essentially small category
As an example we will take the categories \(\texttt {FinSet}\) and \(\texttt {FinOrd}\). Starting with the former, the category of finite sets \(\texttt {FinSet}\) is defined as follows:
/-- Finite sets as a category - objects are Fin n for various n -/
structure FinSetObj : Type 1 where
n : ℕ
carrier : Type 0
equiv : carrier ≃ Fin n -- witness that carrier has exactly n elements
/-- Morphisms are functions between the carriers -/
def FSHom (A B : FinSetObj) : Type 0 := A.carrier → B.carrier
/-- First, we need a Category instance -/
instance FinSetObj.category : Category FinSetObj where
Hom := FSHom
id := fun _ => id
comp :=
fun {X Y Z} (f : FSHom X Y) (g : FSHom Y Z) => fun x => g (f x)
id_comp := fun _ => rfl
comp_id := fun _ => rfl
assoc := fun _ _ _ => rfl
It's defined as the category who's objects are finite sets and who's morphisms are functions between said sets. Here we are defining a custom variant of a finite set object \(\texttt {FinSetObj}\) which contains:
-
A natural number \(\texttt {n : ℕ}\) representing the cardinality of the set.
-
A carrier type \(\texttt {carrier : Type 0}\) representing the actual elements of the set.
-
An equivalence \(\texttt {equiv : carrier ≃ Fin n}\) which acts as a witness that the carrier has exactly \(\texttt {n}\) elements.
We then define our morphisms as functions between the carrier types of two finite set objects. Finally we provide a category instance in the standard way.
Next we want to define the category of all finite ordinal numbers \(\texttt {FinOrd}\). This is defined as follows:
/-- The skeleton: the discrete category on ℕ -/
abbrev FinSetSkeleton := ℕ
/-- The skeleton category:
objects are ℕ, morphisms are functions between Fin types -/
structure FinSkel : Type 0 where
n : ℕ
instance : SmallCategory FinSkel where
Hom := fun A B => Fin A.n → Fin B.n
id := fun _ => id
comp := fun f g => g ∘ f
In our case we can define the finite ordinals as the skeleton of the finite sets category. So our objects are just natural numbers \(\texttt {n : ℕ}\) representing the finite ordinals and our morphisms are functions between the corresponding finite sets \(\texttt {Fin n}\). Again we provide a small category instance in the standard way.
Now central to the definition of an essentially small category is the existence of an equivalence, in other words we need to functors with a natural transformation witnessing the equivalence. We'll start by defining the functor from the finite ordinals to the finite sets:
/-- Canonical embedding of FinSkel into FinSetObj -/
def skelToFinSetObj : FinSkel ⥤ FinSetObj where
obj := fun A => ⟨A.n, Fin A.n, Equiv.refl _⟩
map := fun f => f
map_id := fun _ => rfl
map_comp := fun _ _ => rfl
We can note here that:
-
The object mapping takes a finite ordinal \(\texttt {A : FinSkel}\) and maps it to the corresponding finite set object with carrier \(\texttt {Fin A.n}\). The equivalence is just the identity equivalence since \(\texttt {Fin A.n}\) obviously has exactly \(\texttt {A.n}\) elements.
-
The morphism mapping is just the identity since morphisms in both categories are functions between finite sets.
-
The functor laws are satisfied by reflexivity.
The other way around is a little bit more involved, we can construct the functor as follows:
def finSetObjToSkel : FinSetObj ⥤ FinSkel where
obj := fun A => ⟨A.n⟩
map := fun {A B} f => B.equiv ∘ f ∘ A.equiv.symm
map_id := fun A => by
funext x
show A.equiv ((id : A.carrier → A.carrier) (A.equiv.symm x))
= (id : Fin A.n → Fin A.n) x
simp only [id_eq, Equiv.apply_symm_apply]
map_comp := fun {A B C} f g => by
funext x
show C.equiv (g (f (A.equiv.symm x)))
= (C.equiv ∘ g ∘ B.equiv.symm) ((B.equiv ∘ f ∘ A.equiv.symm) x)
simp only [Function.comp_apply, Equiv.symm_apply_apply]
Again to break this down by components:
variable (A B : FinSetObj) (f : FinSetObj.category.Hom A B)
#check B.equiv ∘ f -- ⇑B.equiv ∘ f : A.carrier → Fin B.n
#check f ∘ A.equiv.symm -- f ∘ ⇑A.equiv.symm : Fin A.n → B.carrier
Whats going on here is that the composition coerces the equivalences into functions i.e.
@[simp, norm_cast]
lemma _root_.EquivLike.coe_coe {F} [EquivLike F α β] (e : F) :
((e : α ≃ β) : α → β) = e := rfl
Since the equivalence is between the carrier (set) type and the upper bound witness we have the function
⇑B.equiv B.carrier → Fin B.n
⇑A.equiv.symm Fin A.n → A.carrier
hence composing this with our morphism gives
A.carrier → B.carrier → Fin B.n -- so A.carrier → Fin B.n
Fin A.n → A.carrier → B.carrier -- so Fin A.n → B.carrier
and composing these two results in the desired function \(\texttt {Fin A.n → Fin B.n}\).
Next we want to show that the functor preserves identities. In our case this means the following:
map_id : ∀ (A : FinSetObj),
⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm = 𝟙 { n := A.n }
As our probelm is of the shape
\[
(\forall x, f x = g x)
\]
We can apply the \(\texttt {funext}\) tactic which reduces the goal to showing that the two sides are equal when applied to an arbitrary input \(\texttt {x}\). Our goal then becomes:
(⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x = (𝟙 { n := A.n }) x
It might be helpful at this point to take a look at the underlying types:
... : Fin { n := A.n }.n → Fin { n := A.n }.n
=
... : { n := A.n } ⟶ { n := A.n }
The purpose of the \(\texttt {show}\) tactic here is to explicitly specify the goal we want to prove, i.e. create a definitionally equal variant of the goal to replace the current one with, if we look at the goals before and after the show tactic we have:
-- before
⊢ (⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x = 𝟙 { n := A.n } x
-- after
⊢ A.equiv (id (A.equiv.symm x)) = id x
looking at the types of the goal after the \(\texttt {show}\) tactic we have:
... : Fin A.n
=
... : Fin A.n
our final two simplifications then do
A.equiv (id (A.equiv.symm x)) = A.equiv (A.equiv.symm x)
-- id_eq : ... (a : α), id a = a
A.equiv (A.equiv.symm x) = x
-- apply_symm_apply : ... (e : α ≃ β) (x : β), e (e.symm x) = x
x = x
For the sake of completeness I want to go into the \(\texttt {show}\) tactic a bit more. Startign with the right hand side, after the funext we have:
𝟙 { n := A.n } x
The braces here are just syntactic sugar for defining a FinSkel structure inline, so unfolding it we can equivalently display this as:
variable (A : FinSetObj) (x : Fin (FinSkel.mk A.n).n)
#check FinSkel.cat.id (FinSkel.mk A.n) x
but what we can notice if we look at the definition of our category is that the arrows between objects are actually arrows between their \(\texttt {n}\) fields (with the Fin proof) i.e.
fun A B => Fin A.n → Fin B.n
so in reality our identity morphism is actually:
𝟙 { n := A.n } : Fin A.n → Fin A.n
hence applying it to \(\texttt {x}\) gives us:
(𝟙 { n := A.n }) x = id x
The left hand side follows a similar logic, in that we can again replace the identity morphism on the object with the identity function on the carrier type directly so we have:
(⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x
-> (⇑A.equiv ∘ id ∘ ⇑A.equiv.symm) x
and then if we avoid the syntactic sugar of function composition we have:
⇑A.equiv (id (⇑A.equiv.symm x))
we can equivalently just automate this step by just prepending \(\texttt {Function.comp}\) into our simplification steps.
For the case of showing that our functor preserves composition of morphisms we have a similar situation as to the identity case, here just to keep things not dragging on too long i'll just say that again we are more or less following the same logic as before. We are using show to reduce or goal into a form that is easier to reason about, and then we are just simplifying using the properties of equivalences and function composition.
Moving on we now have two create our natural transformations, here things should now be rather straightforward. In lean we have:
def unitNatTrans
: 𝟭 FinSetObj ⟶ finSetObjToSkel ⋙ skelToFinSetObj where
app := fun A => (A.equiv : A.carrier → Fin A.n)
naturality := fun A B f => by
funext x
show B.equiv (f x)
= (B.equiv ∘ f ∘ A.equiv.symm) (A.equiv x)
simp only [Function.comp_apply, Equiv.symm_apply_apply]
def unitInvNatTrans
: finSetObjToSkel ⋙ skelToFinSetObj ⟶ 𝟭 FinSetObj where
app := fun A => (A.equiv.symm : Fin A.n → A.carrier)
naturality := fun A B f => by
funext x
show B.equiv.symm ((B.equiv ∘ f ∘ A.equiv.symm) x)
= f (A.equiv.symm x)
simp only [Function.comp_apply, Equiv.symm_apply_apply]
/-- The unit isomorphism -/
def unitIsoFinSetObj : 𝟭 FinSetObj ≅ finSetObjToSkel ⋙ skelToFinSetObj where
hom := unitNatTrans
inv := unitInvNatTrans
hom_inv_id := by
ext A
funext x
show A.equiv.symm (A.equiv x) = x
simp only [Equiv.symm_apply_apply]
inv_hom_id := by
ext A
funext x
show A.equiv (A.equiv.symm x) = x
simp only [Equiv.apply_symm_apply]
in lean composition of functors is denoted by the operator \(\texttt {⋙}\) so we can see that our unit natural transformation has the correct type. The components of the natural transformation are just given by the equivalences we have in our finite set objects, and the naturality conditions again follow from unfolding the definitions and simplifying.
/-- Naturality lemma for counit transformations -/
lemma counit_naturality {A B : FinSkel} (f : A ⟶ B) :
(𝟭 FinSkel).map f ≫ id = id ≫ (skelToFinSetObj ⋙ finSetObjToSkel).map f := by
simp only [Functor.id_obj, Functor.comp_obj, skelToFinSetObj, finSetObjToSkel]
simp only [Functor.id_map, Functor.comp_map]
rfl
/-- The counit natural transformation: skelToFinSetObj ⋙ finSetObjToSkel → id -/
def counitNatTrans : skelToFinSetObj ⋙ finSetObjToSkel ⟶ 𝟭 FinSkel where
app := λ _ => id
naturality := fun _ _ f => counit_naturality f |>.symm
/-- The inverse of counit -/
def counitInvNatTrans : 𝟭 FinSkel ⟶ skelToFinSetObj ⋙ finSetObjToSkel where
app := λ _ => id
naturality := fun _ _ f => counit_naturality f
/-- The counit isomorphism -/
def counitIsoFinSkel : skelToFinSetObj ⋙ finSetObjToSkel ≅ 𝟭 FinSkel where
hom := counitNatTrans
inv := counitInvNatTrans
hom_inv_id := by ext A; rfl
inv_hom_id := by ext A; rfl
Finally we can define the equivalence and then construct the essentially small instance:
/-- The equivalence between FinSetObj and FinSkel -/
def finSetObjEquiv : FinSetObj ≌ FinSkel where
functor := finSetObjToSkel
inverse := skelToFinSetObj
unitIso := unitIsoFinSetObj
counitIso := counitIsoFinSkel
functor_unitIso_comp := fun A => by
funext x
show (id : Fin A.n → Fin A.n) (A.equiv (A.equiv.symm x)) = x
simp only [id_eq, Equiv.apply_symm_apply]
/-- Now we show FinSetObj is essentially small.
We construct an explicit equivalence with the small category FinSkel. -/
instance FinSetObj.essentiallySmall : EssentiallySmall.{0} FinSetObj :=
EssentiallySmall.mk' finSetObjEquiv