definition example theorem proof

For any Graph , the free category (Kittenlab: the path category ) has objects the vertices and morphisms the paths from to . The identity on is the trivial (length-0) path; composition is concatenation of paths. We often elide the difference between a graph and its free category.

Sources: 7 Sketches Definition 3.7, Eq. (3.8), Example 3.13, Exercises 3.9, 3.10, 3.12, 3.15, 3.33; Remark 3.23; Kittenlab Lecture 6; DaoFP §8.1 (stick-figure categories), §10.9 (free constructions); CTfS §3.3.2 (Definition 3.3.2.1, Example 3.3.2.2, Exercises 3.3.2.3–3.3.2.4), Examples 4.1.2.19, 4.1.2.27, Exercises 4.1.2.28–4.1.2.31

Proof that it is a category (7S Exercise 3.9): define a path as with and ; concatenation when . Concatenating with a length-0 path returns the same tuple (unitality), and either bracketing of three paths yields the same tuple (associativity).

Examples

  • : two objects, three morphisms — the Walking Arrow.
  • : three objects, six morphisms (7S Exercise 3.10); has morphisms, has one object and one morphism, is empty (7S Exercise 3.12).
  • Example 3.13: the graph with one vertex and one loop has paths , one of each length: of it is the Natural Numbers as a one-object category, a Monoid (concatenation adds lengths, 7S Exercise 3.15).
  • The free square category has ten morphisms; adding the equation gives the commutative square with nine (Presentation of a Category).
  • The only isomorphisms in are identities, since lengths add (7S Exercise 3.33).

From Category Theory for Scientists. In the graph , , , , there is no path , one path , two paths ( and ) and infinitely many (words in and ) (CTfS Example 3.3.2.2). The paths of a graph do not form a monoid under concatenation — there is no single identity and not every pair concatenates — which is exactly why categories, with one identity per object and partial composition, are needed (CTfS Exercise 3.3.2.4). For the graph of US cities and airline flights, the free category is the category of itineraries: sequences of connecting flights (CTfS Exercise 4.1.2.29). The paths-graph functor is the Monad of the free/underlying adjunction: its unit views an arrow as a path of length one, its multiplication concatenates a path of paths, and “a category is a graph with a map ” satisfying the algebra laws (CTfS Remark 4.3.1.7, Eilenberg-Moore Category).

Properties

  • Defining functors out of is easy (Kittenlab Lecture 6): pick an object for every vertex and a morphism for every edge; a path goes to the composite , and preservation of composition comes “for free”. Such functors are easy to store: an object per vertex, a morphism per edge — this is Kittenlab’s Diagram and Catlab’s FinDomFunctor. Functors are ACSets.
  • is a Functor , left adjoint to the underlying-graph functor (7 Sketches Example 3.74, DaoFP “free functors generate structure freely and lazily”). Similarly graphs generate free preorders (Hasse Diagram).
  • Free categories and preorders are two ends of a spectrum (Remark 3.23): with no equations every path is a distinct morphism; with all equations, parallel paths are identified (Preorder Reflection). Every Presentation of a Category lies in between.
  • The free category on a graph is the Free Monoid “with types”: DaoFP’s free monoid on an alphabet is the free category on a one-vertex graph.

Docs: FinCats · ACSets API · Graphs — Kittenlab Lecture 6

Builds on: Category (Category) — run that note’s Julia code first.

# Kittenlab src/FinCats.jl: a finitely presented (here: free) category with paths as morphisms
struct FinCatMorphism{L}
  dom::L; codom::L; path::Vector{L}
end
struct FinCat{L} <: Category{L, FinCatMorphism{L}}
  objects::Set{L}
  homs::Dict{L, Tuple{L, L}}          # generator => (source, target)
end
Categories.dom(::FinCat, f::FinCatMorphism) = f.dom
Categories.codom(::FinCat, f::FinCatMorphism) = f.codom
function Categories.compose(::FinCat{L}, f::FinCatMorphism{L}, g::FinCatMorphism{L}) where {L}
  @assert f.codom == g.dom
  FinCatMorphism(f.dom, g.codom, L[f.path; g.path])
end
Categories.id(::FinCat{L}, x::L) where {L} = FinCatMorphism{L}(x, x, L[])
 
C = FinCat(Set([:a, :b, :c]), Dict(:f => (:a, :b), :g => (:b, :c)))

Catlab version (run in a fresh Julia session — Catlab exports its own compose, id, FinFunction, …):

# Catlab: free category on a graph
using Catlab
g = @acset Graph begin V = 3; E = 2; src = [1, 2]; tgt = [2, 3] end
C = FinCat(g)
hom_generators(C)              # the two edges
#check CategoryTheory.Paths        -- Paths V : the free category on a quiver V
#check CategoryTheory.Paths.of     -- the prefunctor V ⥤q Paths V
#check CategoryTheory.Paths.lift   -- a prefunctor V ⥤q C extends uniquely to Paths V ⥤ C
-- the adjunction Free ⊣ Forget between quivers and categories (Mathlib.CategoryTheory.Category.Quiv):
#check CategoryTheory.Quiv.adj     -- Cat.free ⊣ Quiv.forget
-- the free category on a graph: morphisms are lists of edges (paths)
data Path e = Path [e]         -- with implicit source/target bookkeeping
instance Category' (Path e) where   -- sketch: composition is concatenation, identity is []
  idP = Path []
  Path q `after` Path p = Path (p ++ q)
 
-- DaoFP-style free structure: a free monoid is a list, the free category is a typed list