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:

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

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

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

References

    Reference. category [nlab-category]

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

    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

      Related

        Definition. Quiver [002l]

        • November 27, 2025

        A quiver is a collection of edges which may stretch between (ordered) pairs of points called vertices. Thus making a quiver a kind of graph. In the graph theoretical sense a quiver is a directed pseudo-multigraph so breaking that down [0]:

        • It's directed meaning each arrow has a direction associated with it going from a source vertex to a target vertex
        • It's a pseudograph meaning each pair of vertices has some number of edges (including zero) between them, and loops (edges that connect a vertex to itself) are allowed
        • It's a multigraph which means we constrain the kinds of edges to disallow loops (an edge from a vertex to itself.)

        Lean representation

        • November 27, 2025

        The lean representation of this construct is given as follows: 

        
    universe v v₁ v₂ u u₁ u₂

    class Quiver (V : Type u) where
      Hom : V → V → Sort v