Higher categories as globular algebras
In this section, we recall and extend the setting for globular algebraic higher categories introduced by Batanin in [Bat98a]. In this setting, a particular theory of :-categories is a monad on the category of :-globular sets. Most globular higher categories that one usually encounters t in this setting: strict :-categories, bicategories, precategories (de ned later in this chapter), Gray categories, etc. From this unifying viewpoint, several notions and constructions can be de ned once for all theories, like the notion of :-polygraph and the associated free :-category construction as we will see in the next section. Moreover, a notion of :-category de ned in this setting canonically induces notions of 0-, . . . , „: 1”-categories with associated truncation and inclusion functors between the di erent dimensions. Among the broad class of theories of higher categories that are captured by this setting, one can distinguish the theories that are associated with a truncable monad. Such theories are better behaved in some aspects and more closely match the idea that one can have of higher categories. Indeed, the general setting of Batanin allows de ning notions of higher categories with unusual operations. This can be problematic since these operations can induce too much interaction between cells of di erent dimensions, so that for example the construction of free instances can not be done dimensionwise. This motivates the consideration of truncable monads, that do not allow this kind of operations.
The setting of Batanin o ers a nice abstraction of the di erent higher category theories. How-ever, the textbook de nitions of the di erent higher categories are generally not given by a monad. Instead, notions of :-categories are usually de ned by sets of operations (identities, compositions) that satisfy several equations. Moreover, the de nitions of several natural operations, like the truncation and inclusion functors, are usually additional boilerplate that is not explicitly derived from general constructions. It is quite simple to show that an equational de nition of higher categories induces a monad, but to give an explicit description of this monad in order to apply the general results and constructions of Batanin’s setting can be quite tedious. Thus, there is a gap between Batanin’s abstract viewpoint on higher categories and actual de nitions, and it deserves to be lled.
The plan for this section is as follows. First, we recall the de nitions of an algebra over a monad and the associated Eilenberg-Moore category, using some abstract reformulations for these objects coming from the formal theory of monads of Street [Str72] (Section 1.2.1). Then, we recall the de nition of globular sets and some operations on these objects (Section 1.2.2). Next, we recall Batanin’s setting of higher categories as globular algebras, i.e., the Eilenberg-Moore categories derived from a monad on globular sets (Section 1.2.3). We show how a monad on :-globular set induces globular algebras from dimension 0 to : and de ne truncation and inclusion functors between the di erent dimensions. We moreover introduce a criterion that enables to relate actual de nitions of higher categories to the ones obtained with this setting without having to explicitly describe the underlying monads (Theorem 184.108.40.206). Finally, we recall from [Bat98a] the notion of truncable monad and give several additional properties that they have over general monads on globular sets (Section 1.2.4). We moreover introduce a criterion to recognize that the underlying monads of globular algebras are truncable, without having to explicitly describe those monads (Theorem 220.127.116.11).
Algebras over a monad
In this section, we recall the de nition of an algebra over a monad, together with the associated notion of Eilenberg-Moore category, taking the formal perspective introduced by Street [Str72]. We moreover recall the related notions of monadicity and of monad morphism.
18.104.22.168 — Algebras. Given a monad „) [ ‘” on a category C, a ) -algebra is the data of an object – 2 C together with a morphism : ) – ! – such that [- = id- and ‘- = ) „ ”.
A morphism between two algebras „- ” and „- 0 0” is the data of a morphism 5 : – ! – 0 of C satisfying
= 0 )„5”.
We write C) for the category of ) -algebras, also called Eilenberg-Moore category of ) . There is a canonical forgetful functor U):C) !C which maps the ) -algebra „- ” to – . This functor has a canonical left adjoint F):C!C) which maps – 2 C to the ) -algebra „) – ‘-associated counit, denoted n) , is such that n) „- ”, such that the unit of F) a U) is [, and the ” = for a given ) -algebra „- ”. The monad induced by F) a U) is then exactly „) [ ‘”.
In order to study functors of the form D ! C) , it is useful to introduce an abstract char-acterization for such functors, which is a specialization in CAT of the general description of Eilenberg-Moore objects given by Street in his formal theory of monads [Str72]. To give some intuition, note that ) -algebra can be equivalently described as a functor : 1 ! C together with a natural transformation U : ) ) such that U „[ ” = id and U „‘ ” = U „) U”
This correspondence extends to more general functors to C) in the form of the following property, that can be derived from [Str72, Theorem 1]:
Theorem 22.214.171.124. Given a category D, the operation which maps a functor : D ! C) to the pairs „U) U) n) ” induces a natural bijective correspondence between the functors D ! C) and the pairs „ U” where : D ! C is a functor and U : ) ) is a natural transformation such that U „[ ” = id and U „‘ ” = U „) U”.
In fact, the correspondence of [Str72, Theorem 1] relies on a 2-adjunction, so that it extends to natural transformations as well:
Theorem 126.96.36.199. Given a category D and functors 0 : D ! C) , the operation which maps a natural transformation V : ) 0 to U) V induces a bijective correspondence between the natural transformation ) 0 and the natural transformations ¯: U) ) U) 0 such that V „U) n) ” = „U) n) 0” „) V”
188.8.131.52 — Monadicity. Let „) [ ‘” be a monad on a category C. Given a category D and an adjunction F a U : D ! C such that the monad induced by this adjunction is exactly „) [ ‘”, recall that there is a canonical functor H : D ! C) , called comparison functor, derived from this adjunction (c.f. [Mac13, Theorem VI.3.1]). This functor can also be de ned in the setting of Street using Theorem 184.108.40.206: Theorem 220.127.116.11 ([Str72, Theorem 3]). There is a unique functor H : D ! C) such that U) H = U and U) n) H = Un where n is the counit of F a U. The functor H moreover satis es that F) = H F and n) H = Hn.
A functor ¯ : ¯ ¯ is said monadic when it has a right adjoint ¯ : ¯ ¯ such that the U D!C ¯ ¯ F C!D ¯ ¯) ¯ comparison functor H :D!C is an equivalence of categories, where „) [¯ ‘¯” is the monad ¯ ¯ induced by the adjunction F a U. Monadic functors can be characterized by Beck’s monadicity theorem that we introduce later (c.f. Theorem 18.104.22.168).
Proposition 22.214.171.124. For : 2 N[ f=g, the category Alg: is locally nitely presentable. In particular, it is complete and cocomplete. Moreover, the functor U: preserves and creates directed colimits, and creates limits.
Proof. The category Alg: is locally nitely presentable as a consequence of Proposition 126.96.36.199 since Glob: is locally nitely presentable by Remark 188.8.131.52. The functor U: preserves directed colimits by Proposition 184.108.40.206. Moreover, since U: re ects isomorphisms and Alg: is cocomplete, U: creates directed colimits. Finally, it is well-known that the forgetful functor associated to an Eilenberg-Moore category creates limits (see [Bor94b, Proposition 4.3.1] for example).
We can usually derive monads from equational de nitions of higher categories as illustrated by the following examples.
Example 220.127.116.11. Since 1-globular sets are graphs, the nitary forgetful functor Cat ! Gph de ned in Example 18.104.22.168 induces a nitary monad „) [ ‘ ” on Glob1. This monad maps a 1-globular set seen as a graph to the underlying 1-globular set of the category of paths on . Using Beck’s monadicity theorem (Theorem 22.214.171.124), one can verify that the functor Cat ! Gph is monadic, so that Alg1 ’ Cat. Moreover, the monad „) 0 [0 ‘0” is essentially the identity monad on Glob0, and thus Alg0 ’ Set. More generally, we will see in Section 1.4.1 that the monads of strict :-categories for : 2 N are derived from the monad of strict l-categories.
Example 126.96.36.199. We de ne a notion of weird 2-category as follows: a weird 2-category is a 2-globular set equipped with an operation :2 2!0.
Note that we do not require the composability of the arguments of , and we do not enforce any axiom on . A morphism between two weird 2-categories is then a morphism between the underlying 2-globular sets that is compatible with . The category Weird of weird 2-categories and their morphisms is essentially algebraic, and the functor which maps a weird 2-category to its underlying 2-globular set is induced by an essentially algebraic theory morphism, so that it is a right adjoint and nitary by Theorem 188.8.131.52. From the adjunction, we derive a nitary monad „) [ ‘” on Glob2, and, given – 2 Glob2, we have that „) – ”0 ’ -0 t „-2 -2” „) – ”1 ’ -1 „) – ”2 ’ -2 so that, for Alg2 derived from the monad ) , Alg2 ’ Weird. Moreover, the monads „) 0 [0 ‘0” and „) 1 [1 ‘1” are essentially the identity monads on Glob0 and Glob1 respectively, so that the associated notions of weird 0- and 1-categories are simply 0- and 1-globular sets.
The last example moreover illustrates the unusual operations that notions of higher categories de ned in the setting of Batanin can have. It is also an example of a monad on globular sets which is not truncable (c.f. Example 184.108.40.206).
Remark 220.127.116.11. In the above de nition, we require that the monad „) [ ‘” is nitary in order to prove later the existence of several free constructions on the :-categories. This is not too restrictive, since it includes all the monads of algebraic globular higher categories that have operations with nite arities, i.e., most theories of algebraic globular higher categories.
Truncation and inclusion functors. We now introduce truncation and inclusion functors between the categories Alg: together with some of their properties. Let = 2 N [ fl g and „) [ ‘” be a nitary monad on Glob=. Given : ; 2 N= [ f=g with : ; and a ) ;
Table of contents :
Topics of this thesis
1 Higher categories
1.1 Finite presentability
1.1.2 Essentially algebraic theories
1.2 Higher categories as globular algebras
1.2.1 Algebras over a monad
1.2.2 Globular sets
1.2.3 Globular algebras
1.2.4 Truncable globular monads
1.3 Free higher categories on generators
1.3.1 Pullbacks in CAT
1.3.2 Cellular extensions
1.4 Strict categories and precategories
1.4.1 Strict categories
1.4.3 Categories as precategories
1.5 Higher categories as enriched categories
1.5.2 The funny tensor product
1.5.3 Enriched denition of precategories
2 The word problem on strict categories
2.1 Measures on polygraphs
2.1.1 =-globular groups and =-groups
2.1.2 Measures on polygraphs
2.1.3 Elementary properties of free categories
2.2 Free categories through categorical actions
2.2.1 Categorical actions
2.2.2 Contexts and contexts classes
2.2.3 Free action on a cellular extension
2.2.4 Free ¹=¸1º-categories on =-categorical actions
2.2.5 Another description of free categories on cellular extensio
2.3 Computable free extensions
2.3.1 Computability with encodings
2.3.2 Computable free cellular extensions
2.3.3 The case of polygraphs
2.4 Word problem on polygraphs
2.4.1 Terms and word problem
2.4.2 Solution to the word problem on nite polygraphs
2.4.3 Solution to the word problem on general polygraphs
2.4.4 An implementation in OCaml
2.5 Non-existence of some measure on polygraphs
2.5.1 Plexes and polyplexes
2.5.2 Inexistence of the measure
3 Pasting diagrams
3.1 The formalisms of pasting diagrams
3.1.2 Parity complexes
3.1.3 Pasting schemes
3.1.4 Augmented directed complexes
3.1.5 Torsion-free complexes
3.2 The category of cells
3.2.1 Movement properties
3.2.2 Gluing sets on cells
3.2.3 Cell¹%º is an l-category
3.3 The freeness property
3.3.1 Cell decompositions
3.3.2 Freeness of decompositions of length one
3.3.3 Freeness of general decompositions
3.4 Relating formalisms
3.4.1 Closed and maximal cells
3.4.2 Embedding parity complexes
3.4.3 Embedding pasting schemes
3.4.4 Embedding augmented directed complexes
3.4.5 Absence of other embeddings
4 Coherence for Gray categories
4.1 Precategories for computations and presentations
4.1.2 Free precategories
4.1.3 Presentations of precategories
4.2 Gray categories
4.2.1 The Gray tensor products
4.2.2 Gray categories
4.2.3 Gray presentations
4.2.4 Correctness of Gray presentations
4.3.1 Coherence in Gray categories
4.3.2 Rewriting on 3-prepolygraphs
4.3.4 Critical branchings
4.3.5 Finiteness of critical branchings
4.4.3 Frobenius pseudomonoid