Definition. Isomorphism (morphisms) [002s]

November 29, 2025

A morphism \(f : X \to Y\) is called an Isomorphism if there exists a morphism \(g : Y \to X\) such that the following hold (1):

\[ g \circ f = 1_X \quad f \circ g = 1_Y \]

Sometimes an isomorphism is also denoted

\[ X \xrightarrow {\cong } Y \]

References

Reference. 2-Dimensional Categories [johnson-yau-2d-categories-2020]

June 17, 2020
Johnson, Niles, Yau, Donald
https://arxiv.org/abs/2002.06055v3

Context

Blog. A simple Bool category in Lean4 [002u]

November 29, 2025

Definition. Category [002m]

November 27, 2025

There are a few ways you can define a category. In the most basic intuitive sense a category consists of a collection of things called objects and binary relationships (or transitions) between those objects called morphisms (or arrows). We can combine these relationships by composing them, and for each object there is an identity morphism that acts as a neutral element for composition. (1)

In the context of quivers a category can be defined as a quiver with a rule saying for how we can compose two edges that fit together to get a new edge. Furthermore, each vertex (object) has an edge starting and ending at that vertex (the identity morphism). The classical definition is something like this:

The data

November 27, 2025

A category \(C\) consists of:

A collection (or class (2)) of objects, denoted as \(\text {Ob}(C)\) or \(C_0\).
A collection (or set (2)) of morphisms (or arrows), denoted \(C_1\) or \(C(x, y)\) for \(x, y \in \text {Ob}(C)\).
- For every morphism \(f \in C(x, y)\), there are two associated objects: the source (or domain) \(x\) and the target (or co-domain) \(y\). In standard function notation, we write \(f: x \to y\) where \(x = \text {dom}(f)\) and \(y = \text {cod}(f)\). NLab has a nice convention where it denotes the source \(s\) of a morphism as \(s(f)\) and the target \(t\) as \(t(f)\).
- For every pair of morphisms \(f \in C(x, y)\) and \(g \in C(y, z)\) (s.t. \(t(f) = s(g)\) i.e. the morphisms type check), there is a composition morphism \(g \circ f \in C(x, z)\). Written out we can denote this as: \[ C(x, y) \times C(y, z) \to C(x, z) \] in diagrammatic order this is often written as \(f; g\) we can equivalently use a more graphical notation:
- For every object \(x \in \text {Ob}\) there is an identity morphism: \[ (\text {id}_x : x \to x) \in C(x, x) \]
Note: Some additional notations for morphisms include \(\text {hom}(x, y)\), \(\text {hom}_C(x, y)\) or \(C_1(x, y)\). Additionally, people use the notation \(\text {Mor(C)}\) to denote the following disjoint union \[ \text {Mor}(C) = \bigsqcup _{x, y \in \text {Ob}(C)} C(x, y) \] Which just expresses the idea that the collection of all morphisms in a category is made up of the morphisms between each pair of objects.

The axioms

November 27, 2025

The above are often called data of a category. In addition to this data, a category must satisfy the following axioms or (conditions):

Morphisms need to be associative which means that for every triple of morphisms \(f \in C(w, x)\), \(g \in C(x, y)\), and \(h \in C(y, z)\) the following holds: \[ h \circ (g \circ f) = (h \circ g) \circ f \]
For each morphism \(f \in C(x, y)\) the identity morphisms act as neutral elements for composition: \[ \text {id}_y \circ f = f = f \circ \text {id}_x \] This is also known as the left and right unit laws or just unity in general.

Remarks

November 27, 2025

A category such as the one described above is often also called a 1-category to distinguish it from higher categories such as 2-categories, n-categories.

Definition. Isomorphism (morphisms) [002s]

November 29, 2025

A morphism \(f : X \to Y\) is called an Isomorphism if there exists a morphism \(g : Y \to X\) such that the following hold (1):

\[ g \circ f = 1_X \quad f \circ g = 1_Y \]

Sometimes an isomorphism is also denoted

\[ X \xrightarrow {\cong } Y \]

Example. The category

November 29, 2025

The data

November 29, 2025

We want to start off by defining the data of our category. On a high level we want to define a category with two objects, \(\texttt {true}\) and \(\texttt {false}\). Starting with the object representation we have:


      /-- A wrapper type to make a custom category on Bool -/
      structure BoolCat : Type where
        val : Bool
      deriving DecidableEq, Repr

      /-- The two objects -/
      def BoolCat.tt : BoolCat := ⟨true⟩
      def BoolCat.ff : BoolCat := ⟨false⟩

Next we want to define the morphisms between these objects. For each pair of objects we express 3 kinds of morphisms: the identity morphism, a morphism from \(\texttt {false}\) to \(\texttt {true}\), \(\texttt {false}\)from \(\texttt {true}\) to \(\texttt {false}\). We can express this in Lean as follows:


      /-- Morphisms: we allow identity on each, plus iso between them -/
      inductive BCHom : BoolCat → BoolCat → Type
        | id (b : BoolCat) : BCHom b b
        | swap : BCHom BoolCat.tt BoolCat.ff
        | swapInv : BCHom BoolCat.ff BoolCat.tt

Formally what this describes is a kind of piecewise function:

\[ \text {f}(x, y) = \begin {cases} 1_x &: x \to x & \texttt {if } x = y \\ \texttt {swap} &: \text {tt} \to \text {ff} & \texttt {if } x = \text {tt} \land y = \text {ff} \\ \texttt {swapInv} &: \text {ff} \to \text {tt} & \texttt {if } x = \text {ff} \land y = \text {tt} \end {cases} \]

Composition and Category instance

November 29, 2025

Now we have some notion of objects and morphisms between them, we can move on to defining composition of morphisms.


      def comp : {X Y Z : BoolCat} → BCHom Y Z → BCHom X Y → BCHom X Z
        | _, _, _, id _, f => f
        | _, _, _, f, id _ => f
        | _, _, _, swapInv, swap => id _
        | _, _, _, swap, swapInv => id _

This defines composition by pattern matching on the possible morphism combinations. Note that we have to explicitly handle the cases where we compose \(\texttt {swap}\) and \(\texttt {swapInv}\) to get the identity morphism on the respective objects. To construct our category we have to provide proofs for the category axioms, namely associativity and identity.


      @[simp] theorem id_comp' {X Y : BoolCat} (f : BCHom X Y) 
          : comp (id Y) f = f := by
        cases f <;> rfl

      @[simp] theorem comp_id' {X Y : BoolCat} (f : BCHom X Y) 
          : comp f (id X) = f := by
        cases f <;> rfl

      theorem assoc'  (f : BCHom W X) (g : BCHom X Y) (h : BCHom Y Z) :
          comp h (comp g f) = comp (comp h g) f := by
        cases f <;> cases g <;> cases h <;> rfl

With all this in place we can finally define our category instance:


      instance : Category BoolCat where
        -- The data
        Hom     := BCHom
        id      := BCHom. id
        comp    := fun f g => BCHom. comp g f

        -- Category laws
        id_comp := fun f     => BCHom.comp_id' f
        comp_id := fun f     => BCHom.id_comp' f
        assoc   := fun f g h => BCHom.assoc' f g h

Isomorphisms in the Bool category

November 29, 2025

Since we clearly see that the morphisms \(\texttt {swap}\) and \(\texttt {swapInv}\) are inverses of each other, we can construct an isomorphism between the two objects \(\texttt {tt}\) and \(\texttt {ff}\) as follows:


      def ttFfIso : BoolCat.tt ≅ BoolCat.ff where
        hom := BCHom.swap
        inv := BCHom.swapInv
        hom_inv_id := rfl
        inv_hom_id := rfl

We can see that lean uses a similar notation for isomorphism as we do in our notes, namely the \(\texttt {≅}\) symbol between the two objects. We can see that an isomorphism consists of a \(\texttt {hom}\) and an \(\texttt {inv}\) morphism along with proofs that composing them in either order yields the respective identity morphism. In Lean4 its defined as follows:


      structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
        /-- The forward direction of an isomorphism. -/
        hom : X ⟶ Y
        /-- The backwards direction of an isomorphism. -/
        inv : Y ⟶ X
        /-- Composition is the identity on the source. -/
        hom_inv_id : hom ≫ inv = 𝟙 X := by cat_disch
        /-- Composition, in reverse, is the identity on the target. -/
        inv_hom_id : inv ≫ hom = 𝟙 Y := by cat_disch

      ...

      /-- Notation for an isomorphism in a category. -/
      infixr:10 " ≅ " => Iso

We can check out some properties of our isomorphism like so:


      -- Verify it's an isomorphism
      #check ttFfIso           -- BoolCat.tt ≅ BoolCat.ff
      #check ttFfIso.hom       -- BoolCat.tt ⟶ BoolCat.ff
      #check ttFfIso.inv       -- BoolCat.ff ⟶ BoolCat.tt

Furthermore we can also show the identity isomorphism \(tt \cong tt\):


      -- Every object is isomorphic to itself (trivially)
      def ttSelfIso : BoolCat.tt ≅ BoolCat.tt := Iso.refl _

      #check ttSelfIso -- BoolCat.tt ≅ BoolCat.tt

Finally for the sake of completeness we can also demonstrate the isomorphism laws in examples as so:


      -- The isomorphism laws
      example : ttFfIso.hom ≫ ttFfIso.inv = 𝟙 BoolCat.tt 
        := ttFfIso.hom_inv_id

      example : ttFfIso.inv ≫ ttFfIso.hom = 𝟙 BoolCat.ff 
        := ttFfIso.inv_hom_id

Backlinks

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