Definition. Equivalence [002x]

November 30, 2025

We say that a functor \(F : C \to D\) is an equivalence if and only if it is both fully faithful and essentially surjective meaning that:

To be fully faithful it means that each function \[ C(X, Y) \to D(F(X), F(Y)) \] on morphism sets is a bijection.
To be essentially surjective it means that for each object \(Y \in \mathrm {Ob}(D)\) and \(X \in \text {Ob}(C)\) there exists an isomorphism: \[ F(X) \xrightarrow {\cong } Y \]

Backlinks

Definition. (Essentially/Locally) small categories [002o]

November 27, 2025

Definition. Small category

November 27, 2025

A category \(\mathcal {C}\) is called small (or \(U\)-small) if both the collection of objects \(\mathrm {Ob}(\mathcal {C})\) and the collection of morphisms \(\mathrm {Mor}(\mathcal {C})\) are sets (i.e. elements of the universe \(U\)). In lean where we correspond universes to types this just means that we instatiate the universe levels of morphisms and objects to the same thing, we can see this clearly in the definition of a \(\texttt {SmallCategory}\) in mathlib.


    abbrev SmallCategory (C : Type u) : Type (u + 1) := Category.{u} C

Definition. Locally small

November 27, 2025

A locally small category \(\mathcal {C}\) is a category satisfying the following conditions:

The collection of objects \(\mathrm {Ob}(\mathcal {C})\) and morphisms \(\mathrm {Mor}(\mathcal {C})\) are classes. (1)
For every pair of objects \(X, Y \in \mathrm {Ob}(\mathcal {C})\) the hom-set \(\mathcal {C}(X, Y)\) is a set (or small set) instead of a proper class.

The lean definition

November 27, 2025

This one is a little bit more interesting, first let's look at the definition in mathlib:


      class Small (α : Type v) : Prop where
        /-- If a type is `Small.{w}`, 
          then there exists an equivalence with some `S : Type w` -/
        equiv_small : ∃ S : Type w, Nonempty (α ≃ S)

      ...
      class LocallySmall (C : Type u) [Category.{v} C] : Prop where
        /-- A locally small category has small hom-types. -/
        hom_small : ∀ X Y : C, Small.{w} (X ⟶ Y) := by infer_instance

So we can see that in lean a locally small category is defined as a normal category with the added property that for every pair of objects \(X, Y \in \mathrm {Ob}\) the hom-type \(X ⟶ Y\) is \(\texttt {Small}\), which as we can see from the definition of \(\texttt {Small}\) means that there exists some type \(\texttt {S : Type w}\) such that there is an equivalence \(α ≃ S\). We can informally correspond to the lean definition as follows:

Our objects \(\texttt {C : Type u}\) live in some universe level \(u\) which we assoicate with being a class i.e. possibly large collection.
The morphisms between any two objects \(\texttt {X, Y : C}\) live in some other universe level \(w\) where the equivalence to some type \(\texttt {S : Type w}\) expresses the notion that the hom-sets are small sets.

Honestly I think quite reasonably its fair to ask: wait what how does that represent smallness ? What is \(\texttt {w}\) even supposed to be? So I think an example is warranted.

Example of a locally small category

November 27, 2025

This is arguably a bit contrived but let's consider objects as being containers for types in some universe level \(0\) i.e. sets. So we can define our objects and morphisms as follows:


      structure TWrapper : Type 1 where
        carrier : Type 0

      /-- Morphisms are functions - each Hom(A,B) is a set -/
      def TWHom (A B : TWrapper) : Type 0 := A.carrier → B.carrier

Importantly we can note here that the type of objects \(\texttt {TWrapper : Type 1}\) lives in universe level \(1\) which we can think of as a class of sets. However the morphisms between any two objects \(\texttt {TWHom (A B : TWrapper) : Type 0}\) live in universe level \(0\) which we can think of as small sets. Using this we can define a category instance:


      instance TWrapper.category : Category TWrapper where
        -- The data
        Hom     := TWHom
        id      := fun _ => id
        comp    := 
          fun {X Y Z} (f : TWHom X Y) (g : TWHom Y Z) => fun x => g (f x)

        -- The laws
        id_comp := fun _ => rfl
        comp_id := fun _ => rfl
        assoc := fun _ _ _ => rfl

Now we want to define the locally small instance:


      instance TWrapper.locallySmall : LocallySmall.{0} TWrapper where
        hom_small := fun X Y => ⟨⟨TWHom X Y, ⟨Equiv.refl _⟩⟩⟩

This now answers a few questions that arose earlier:

We instantiated the universe level of our hom-sets \(\texttt {w}\) to \(0\) which corresponds to small sets.
The equivalence \(\texttt {α ≃ S}\) in this case is just the identity equivalence \(\texttt {Equiv.refl}\) since our hom-sets are already small sets. On other words here:
```
        Small.{w} (X ⟶ Y)
      
```
We have that \(\texttt {X ⟶ Y}\) represents our set which exists in universe level \(0\), since we are instantiating \(\texttt {w}\) to \(0\) the \(\texttt {Small}\) definition is satisfied by the identity equivalence.

So we can see that in the context of lean a locally small category is just a category where the objects live in some universe level (class) and the hom-sets live in some smaller universe level (set) and we must provide an equivalence showing that the hom-sets are indeed small sets.

Definition. Essentially small

November 27, 2025

A category \(\mathcal {C}\) is called essentially small if there exists a small category \(\mathcal {D}\) and a functor:

\[ F : \mathcal {D} \to \mathcal {C} \]

That is fully faithful and essentially surjective on objects, i.e. it represents an equivalence. In other words we call a category essentially small if its isomorphism classes of objects form a set.

To elaborate a bit more, we say that a functor \(F : C \to D\) is an equivalence if there exists:

A functor \(G : D \to C\)
The natural isomorphisms: \[ \eta : \text {Id}_C \xrightarrow {\cong } G \circ F \quad \epsilon : F \circ G \xrightarrow {\cong } \text {Id}_D \] in other words the natural transformations \(\eta \) and \(\epsilon \) are isomorphisms. Equivalently using diagrammatic notation we can express this as: \[ \eta : 1_C \xrightarrow {\cong } F ; G \quad \epsilon : G ; F \xrightarrow {\cong } 1_D \] in plain english we can see this as saying that the round trip we take by applying \(F\) then \(G\) (or vice versa) is naturally isomorphic to doing nothing at all (the identify functor).

In diagrammatic form we can represent this as follows:

The main takeaway here being that an essentially small category is one which is equivalent to a small category. Hence the problem of demonstrating a category is essentially small reduces to demonstrating isomorphisms between the unit and counit natural transformations.

The lean definition

November 27, 2025

We can again examine the definition in mathlib:


      /-- A category is `EssentiallySmall.{w}` if there exists
      an equivalence to some `S : Type w` with `[SmallCategory S]`. -/
      @[pp_with_univ]
      class EssentiallySmall (C : Type u) [Category.{v} C] : Prop where
        /-- An ES category is equivalent to some small category. -/
        equiv_smallCategory : ∃ (S : Type w) (_ : SmallCategory S), Nonempty (C ≌ S)

We can see quite nicely here how the lean definition corresponds to the informal one. We have our category \(\texttt {C : Type u}\) living in some universe level \(u\) (class) and we require the existence of some small category \(\texttt {S : Type w}\) living in some smaller universe level \(w\) (set) such that there exists an equivalence \(\texttt {C ≌ S}\).

Example of an essentially small category

November 27, 2025

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:

In the object mapping we are taking in a finite set object \(\texttt {A : FinSetObj}\) and mapping it to the corresponding finite ordinal represented by the natural number \(\texttt {A.n}\).
Our morphism mapping is a bit more complex, since we are going from the category of finite sets our source and target objects \(\texttt {A}\) and \(\texttt {B}\) represent the finite set objects. For all pairs of objects the map function demands:
```
          ∀ {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y))
        
```
we are provided with the set of morphisms \(\texttt {f : A.carrier → B.carrier}\) and we need to produce a function between the corresponding finite sets \(\texttt {Fin A.n → Fin B.n}\). Here we utilize an important property that comes with equivalences: they can be used to transport functions between types. To explain what this means let's consider the isolated example:


          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


          @[simp, norm_cast]
          lemma _root_.EquivLike.coe_coe {F} [EquivLike F α β] (e : F) :
              ((e : α ≃ β) : α → β) = e := rfl


          ⇑B.equiv      B.carrier → Fin B.n
          ⇑A.equiv.symm Fin A.n   → A.carrier


          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

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

Definition. Full and faithful functors [002w]

November 30, 2025

We consider a functor between two (locally small) categories \(F : C \to D\). For each pair of objects \(X, Y \in \mathrm {Ob}(C)\) the functor induces a function between hom-sets:

\[ F_{X, Y} : C(X, Y) \to D(F(X), F(Y)) \]

We can describe functors based on the properties of these induced functions as follows:

The functor \(F\) is called faithful if for every pair of objects \(X, Y \in \mathrm {Ob}(C)\) the function \(F_{X, Y}\) is injective. We can also denote this as: \[ (x \xrightarrow {f} y) \mapsto (F(x) \xrightarrow {F(f)} F(y)) \] or using the notation of an embedding as: \[ C(X, Y) \hookrightarrow D(F(X), F(Y)) \] An important note to make here is that a faithful functor only presereves distinctness of morphisms, so what this means is that:
no two different arrows with the same domain and codomain in \(C\) are mapped to (or get identified by) the same arrow in \(D\)
It does not say
- different objects in \(C\) are mapped to different objects in \(D\).
- two morphisms with different domains/codomains in \(C\) are mapped to different morphisms in \(D\).
So in a diagrammatic sense a faithful functor essentially guarantees this:
The functor \(F\) is called full if for every pair of objects \(X, Y \in \mathrm {Ob}(C)\) the function \(F_{X, Y}\) is surjective. Likewise here its important to note that
a full functor only guarantees that any morphism between two objects in the image of \(F\) comes from a morphism in \(C\)
It does not say
- every object in \(D\) is in the image of \(F\). In other words objects in \(D\) outside the image of \(F\) may not have any preimage in \(C\).
- every morphism with a domain/codomain outside the image of \(F\) comes from a morphism in \(C\). Similarly morphisms between objects in the image of \(F\) may not have a preimage in \(C\).
We can again demonstrate this diagrammatically as follows:
The main idea being that a full functor only guarantees that if we have some arrow between two objects in the image (application) of \(F\) then there exists some preimage arrow in \(C\) that maps to it. But we can have objects and morphisms outside the image of \(F\) that do not have any preimage in \(C\).

does not mean

surjective on objects

morphisms

The functor \(F\) is called fully faithful if for every pair of objects \(X, Y \in \mathrm {Ob}(C)\) the function \(F_{X, Y}\) is bijective. We say that a fully faithful functor is necessarily injective on objects up to isomorphism, that is assuming \(F\) is fully faithful then we have: \[ F(X) \cong F(Y) \implies X \cong Y \] This means that if two objects in the image of \(F\) are isomorphic then their preimages in \(C\) must also be isomorphic. In other words what this means is that a fully faithful functor preserves distinctness of objects up to the point of being the same for all practical purposes (i.e. isomorphism).