Presentation of a Category

definition example

A finite presentation of a category is a finite Graph together with path equations: equations $p=q$ between parallel paths (same source vertex and same target vertex). The resulting category — paths modulo the equations and their consequences — is a finitely presented category. A Database Schema is exactly such a presentation.

Sources: 7 Sketches §3.2.2, Examples 3.18, 3.38, 3.41, Exercises 3.16, 3.17, 3.19, 3.21, Remark 3.20; Kittenlab Lecture 6 (“finitely-presented categories, i.e. categories generated by a graph”); Catlab @present; CTfS §3.5.2, §4.2.2 (Slogan 4.2.2.1 “A database schema is a category presentation”, Example 4.2.2.2, Exercises 4.2.2.3–4.2.2.4), §4.4

Examples

Free square vs. commutative square.

Left, no equations: ten morphisms $A,A;f,A;g,A;f;h,A;g;i,B,B;h,C,C;i,D$ (identities named by their objects; 7S Exercise 3.16). Right, with $f;h=g;i$: nine morphisms, because the two composites $A\to D$ are now one and the same morphism. Adding a diagonal $j:A\to D$ with $f;h=j=g;i$ still gives nine (7S Exercise 3.17).

Equations imply more equations (Example 3.18): with one vertex $z$, one loop $s$ and $s;s=z$, we get $s;s;s=s$ etc.; the category is $\{z,s\}$ with $s;s=z$ — the Group $\mathbb{Z}/2\mathbb{Z}$. With $s^4=s^2$ instead, there are four morphisms $z,s,s^2,s^3$ (7S Exercise 3.19).

Preorders as presented categories. A Hasse Diagram presents a preorder: all parallel paths are equated (§3.2.3, 7S Exercise 3.21); e.g. the partition lattice Eq. (1.5) needs $a;d=b;e=c;f$. Every presentation lies between the free category and the Preorder Reflection.

“A database schema is a category presentation” (CTfS Slogan 4.2.2.1). The difference between a schema and its category is like that between generators-and-relations and the monoid they present: a finite schema can present an infinite category — the one-loop schema $\mathrm{Loop}$ presents the monoid $\mathbb{N}$ (a morphism $f^n$ for every $n$). With the PED $c;f={\mathrm{id}}_F$ for “a father has as first child a child, which has as father a father”, the category has exactly five morphisms ${\mathrm{id}}_F,{\mathrm{id}}_C,c,f,f;c$, the last an idempotent on $C$ (CTfS Exercise 4.2.2.3). Many presentations give the same category, which is why schemas and categories are only equivalent (Categories and Schemas are Equivalent).

Functors out of presented categories (Example 3.38, 3.41): there is exactly one functor from the free square $\mathcal{F}$ to the commutative square $\mathcal{C}$ matching the objects — the equations are satisfied; but there is none $\mathcal{C}\to \mathcal{F}$ matching objects, because functors preserve equations: $f^{\prime };h^{\prime }=F(f;h)=F(g;i)=g^{\prime };i^{\prime }$ would have to hold in the free category. Functors preserving composition is exactly what enforces database business rules.

JuliaLeanHaskell

Docs: ThCategory (GATlab) · Theories & presentations — Kittenlab Lecture 6

# Catlab: presentations with path equations
using Catlab
@present CommSquare(FreeCategory) begin
  (A, B, C, D)::Ob
  f::Hom(A, B); g::Hom(A, C); h::Hom(B, D); i::Hom(C, D)
  compose(f, h) == compose(g, i)
end
equations(CommSquare)          # the one path equation
 
@present Z2(FreeCategory) begin
  z::Ob
  s::Hom(z, z)
  compose(s, s) == id(z)
end
 
# 7 Sketches' mySchema, with the two business rules
@present MySchema(FreeSchema) begin
  (Employee, Department)::Ob
  Mngr::Hom(Employee, Employee); WorksIn::Hom(Employee, Department); Secr::Hom(Department, Employee)
  String::AttrType
  FName::Attr(Employee, String); DName::Attr(Department, String)
  compose(Secr, WorksIn) == id(Department)
  compose(Mngr, WorksIn) == WorksIn
end

-- Mathlib: a presented category is a quotient of the free (paths) category by a relation
#check CategoryTheory.Quotient     -- Quotient r for a hom-relation r, with the functor Paths V ⥤ Quotient r

-- a presentation: generators plus equations between parallel paths (as data)
data Presentation v e = Presentation
  { gens :: Graph v e
  , eqs  :: [([e], [e])]    -- pairs of parallel paths declared equal
  }