nLab theory of categories

Idea

The geometric theory of categories $\mathbb{K}$ is a first-order axiomatisation of the concept of a category. $\mathbb{K}$ is (morally) an essentially algebraic theory, and literally a cartesian theory i.e. grosso modo a regular theory where existential quantification is provably unique.

Historically, the first axiomatisation was given by F. William Lawvere in his dissertation in 1963 as part of a formalisation of the category of categories (cf. Lawvere (1963) or ETCC for further information).

Definition

The signature $\Sigma_\mathbb{K}$ has two sorts $O$ and $A$ for objects and arrows, respectively, three function symbols $d_0:A\to O$ , $d_1:A\to O$ and $id:O\to A$, assiging to morphisms their domain, respectively, codomain and to the objects their identity morphisms, as well as a relation symbol $C\rightarrowtail A\times A\times A$ expressing composition of morphisms.

The theory of categories is the theory $\mathbb{K}$ over the signature $\Sigma_\mathbb{K}$ with the following sequents:¹

• $\top\vdash d_0(id(x))=x\wedge d_1(id(x))=x\quad$ ,

• $C(f_1,f_2,f_3)\vdash d_0(f_1)=d_0(f_3)\wedge d_1(f_1)=d_0(f_2)\wedge d_1(f_2)=d_1(f_3)\quad$ ,

• $C(f_1,f_2,f_3)\wedge C(f_1,f_2,f_4)\vdash f_3=f_4\quad$ ,

• $d_1(f_1)=d_0(f_2)\vdash\exists f_3 C(f_1,f_2,f_3)\quad$ ,

• $\top \vdash C(f,id(d_1(f)),f)\wedge C(id(d_0(f)),f,f)\quad$ ,

• $C(f_1,f_2,f_4)\wedge C(f_2,f_3,f_5)\wedge C(f_4,f_3,f_6)\wedge C(f_1,f_5,f_7)\vdash f_6=f_7\quad$.

Remark

The third axiom implies that the existential quantification occurring in the fourth axioms is unique thus $\mathbb{K}$ is indeed cartesian. Since the chosen signature uses a composition relation instead of a partial composition operation the theory as given here is not literally essentially algebraic in the syntactic sense, though, of course, it is Morita equivalent to an essentially algebraic axiomatisation. Other signatures, like a single sorted “arrows only” one, are also possible, the one used here (taken from Johnstone 1977) leans on the so called elementary theory of abstract categories as presented in Lawvere (1966).

Properties

Foremost, we have

Proposition

Let $\mathcal{E}$ be a Grothendieck topos. Then $Mod_{\mathbb{K}}(\mathcal{E})=cat(\mathcal{E})$ with $cat(\mathcal{E})$ the category of (small) internal categories in $\mathcal{E}$ with internal functors as morphisms.$\qed$

Proposition

The classifying topos $Set[\mathbb{K}]$ is the presheaf topos on the opposite of the category of finitely presentable categories in $Set$.

This follows from the fact that the classifying toposes of cartesian theories are generally given as the presheaf toposes on the opposite of the category of finitely presentable models in $Set$ (cf. Johnstone 2002, p.891).² The proposition holds more generally with $Set$ replaced by an arbitrary topos $\mathcal{E}$ with a natural numbers object (cf. Johnstone-Wraith 1978, p.226).$\qed$

Some related theories

• The theory $\mathbb{K}^2$ of $\mathbb{K}$-model homomorphisms is the theory of functors.

• Recall that a discrete opfibration is an internal functor $F\,:\,\mathbf{F}\to \mathbf{C}$ with the property that the following diagram

  $$\array{ & & \\ F_1 &\overset{d_0}{\longrightarrow}& F_0 \\ {}^{\mathllap{\gamma_1}} \downarrow & & \downarrow^{\mathrlap{\gamma_0}} \\ C_1 &\underset{d_0}{\longrightarrow}& C_0 \\ & & }$$

  is pullback. Whence by adding the appropriate geometric axiom to the theory $\mathbb{K}^2$ of functors one obtains as a quotient the theory of discrete opfibrations $\mathbb{K}^2_\downarrow$.

  Let $\mathbf{C}\in cat(\mathcal{E})$ be an internal category. By pulling back its classifying morphism $\overline{\mathbf{C}}\,:\,\mathcal{E}\to \mathcal{E}[\mathbb{K}]$ along the geometric morphism $d_1\,:\,\mathcal{E}[\mathbb{K}^2_\downarrow]\to \mathcal{E}[\mathbb{K}]$ that classifies the codomain of the generic discrete opfibration as an internal category

  $$\array{ \mathcal{E}[\mathbb{K}^\downarrow_\mathbf{C}] &\longrightarrow &\mathcal{E}[\mathbb{K}^2_{\downarrow}] \\ \downarrow & & \downarrow^{d_1} \\ \mathcal{E} &\underset{\overline{\mathbf{C}}}{\longrightarrow}& \mathcal{E}[\mathbb{K}] \\ & & }$$

  one obtains the classifying topos $\mathcal{E}[\mathbb{K}^{\downarrow}_\mathbf{C}]$ for discrete opfibrations on $\mathbf{C}$, or, equivalently, internal diagrams (=copresheaves) on $\mathbf{C}$. Since an internal profunctor $\mathbf{C} ⇸ \mathbf{D}$ is by definition an internal diagram on $\mathbf{C}^{op}\times\mathbf{D}\,$, one can use this construction to obtain the classifying topos for internal profunctors from $\mathbf{C}$ to $\mathbf{D}$ by pulling back along the classifying morphism for $\mathbf{C}^{op}\times\mathbf{D}$ (cf. Johnstone 1977, p.209).

• By adding the following sequents to the theory $\mathbb{K}$ of categories one obtains the theory of filtered categories $\mathbb{K}^\gt$ with models the internal filtered categories (cf. Johnstone 1977, p.203):

  $\array{\\ \top\vdash \exists x (x=x) \\ \\ \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\top\vdash \exists f_1\exists f_2 (d_0(f_1)=x\wedge d_0(f_2)=y\wedge d_1(f_1)=d_1(f_2)) \\ d_0(f_1)=d_0(f_2)\wedge d_1(f_1)=d_1(f_2)\vdash \exists f_3\exists f_4\big (C(f_1,f_3,f_4)\wedge C(f_2,f_3,f_4)\big )\quad}$

Related entries

• category

• category theory

• geometric theory

• theory of objects

• theory of model homomorphisms

• theory of flat functors

• ETCC

References

• P. J. Freyd, A. Scedrov, Categories, Allegories , North-Holland Amsterdam 1990.

• Peter Johnstone, Topos Theory , Academic Press New York (1977). (Also available as Dover Reprint, Mineola 2014, p.202f)

• Peter Johnstone, Sketches of an Elephant vol.2 , Oxford UP 2002. (D1.1.7(e), p.813, D1.3.4, p.833)

• Peter Johnstone, Gavin Wraith, Algebraic Theories in Toposes , pp.141-242 in Johnstone, Paré (eds.), Indexed Categories and Their Applications , Springer LNM 661 Heidelberg 1978.

• F. W. Lawvere, Functorial Semantics of Algebraic Theories , Ph.D. thesis, Columbia University New York 1963. (With an author’s comment and a supplement in: Reprints in Theory and Applications of Categories, no.5 (2004) pp.1-121 (pdf))

• William Lawvere,The Category of Categories as a Foundation for Mathematics, pp. 1-20 in: John W. Gray,Fibred and Cofibred Categories, in: S. Eilenberg, D. K. Harrison, S. MacLane, H. Röhrl (eds.):Proceedings of the Conference on Categorical Algebra - La Jolla 1965, Springer (1966) [doi:10.1007/978-3-642-99902-4]

• Myles Tierney, Forcing Topologies and Classifying Toposes , pp.211-219 in Heller, Tierney (eds.), Algebra, Topology and Category Theory , Academic Press New York 1976.

---

1. Here and in the following $x,y$ are variables ranging over O, whereas the $f_1,f_2,\dots$ range over A; the contexts are assumed to be canonical i.e. consisting of all free distinct variables occurring in a sequent listed in order of first appearance. ↩

2. Apparently $Set[\mathbb{K}]$ made its first appearance in Johnstone’s 1974 Cambridge dissertation on “Internal category Theory” (cf. Tierney 1976). ↩