Yves Guiraud

Philippe Malbos

POLYGRAPHS OF FINITE DERIVATION TYPE

Keywords: higher-dimensional categories, higher-dimensional rewriting, finite derivation type, low-dimensional homotopy functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Craig Squier proved that, if a monoid can be presented by a finite convergent string rewriting system, then it satisfies the homological finiteness condition left-FP 3 . Using this result, he constructed finitely presentable monoids with a decidable word problem, but that cannot be presented by finite convergent rewriting systems. Later, he introduced the condition of finite derivation type, which is a homotopical finiteness property on the presentation complex associated to a monoid presentation. He showed that this condition is an invariant of finite presentations and he gave a constructive way to prove this finiteness property based on the computation of the critical branchings: being of finite derivation type is a necessary condition for a finitely presented monoid to admit a finite convergent presentation. This survey presents Squier's results in the contemporary language of polygraphs and higher-dimensional categories, with new proofs and relations between them.

INTRODUCTION

Given a monoid M, a generating set Σ 1 for M provides a way to represent the elements of M in the free monoid Σ ¦ 1 , i.e. as finite words written with the elements of Σ 1 . But, in general, an element of M has several representatives in Σ ¦ 1 . The word problem for M consists in finding a generating set Σ 1 and a procedure that can determine whether or not any two elements of Σ ¦ 1 represent the same element in the monoid M.

The word problem and convergent presentations. One way to solve the word problem is to exhibit a finite presentation Σ pΣ 1 , Σ 2 q of M, made of a generating set Σ 1 and a set Σ 2 of directed relations with a good computational property: convergence. Indeed, in rewriting theory, one studies presentations where the relations in Σ 2 are not seen as equalities between the words in Σ ¦ 1 , such as u v, but, instead, as rewriting rules that can only be applied in one direction, like u ñ v, thus simulating a non-reversible computational process reducing the word u into the word v.

In rewriting theory, such a presentation Σ of a monoid is called a string rewriting system or, historically, a semi-Thue system; in that case, the directed relations of Σ 2 are called rewriting rules. A presentation Σ is convergent if it has the two properties of ¡ termination, i.e. all the computations end eventually, and ¡ confluence, i.e. different computations on the same input lead to the same result.

The monoid presented by Σ is defined as the quotient, denoted by Σ, of the free monoid Σ ¦ 1 over Σ 1 by the congruence generated by Σ 2 . By extension, we say that Σ presents any monoid isomorphic to Σ.

A finite and convergent presentation Σ of a monoid M gives a solution to the word problem, called the normal-form procedure and defined as follows. Given an element u of the free monoid Σ ¦ 1 , convergence ensures that all the applications of (directed) relations to u, in every possible manner, will eventually produce a unique result: an element p u of Σ ¦ 1 where no relation applies anymore. The word p u is called the normal form of u. By construction, two elements u and v of Σ ¦ 1 represent the same element of M if, and only if, their normal forms are equal in Σ ¦

1 . Finiteness ensures that one can determine whether an element of Σ ¦ 1 is a normal form or not, by examining all the relations.

Rewriting and polygraphs. The notion of string rewriting system comes from combinatorial algebra. It was introduced by Axel Thue in 1914 in order to solve the word problem for finitely presented semigroups [START_REF] Thue | Probleme über Veränderungen von Zeichenreihen nach gegebenen Regeln[END_REF]. It is only in 1947 that the problem was shown to be undecidable, independently by Emil Post [START_REF] Post | Recursive unsolvability of a problem of Thue[END_REF] and Andrei Markov [START_REF] Markov | On the impossibility of certain algorithms in the theory of associative systems[END_REF][START_REF]On the impossibility of certain algorithms in the theory of associative systems. II[END_REF]. Then in 1943, Maxwell Newman gave a general setting, the abstract rewriting theory, to describe the properties of termination and confluence, and to show the first fundamental result of rewriting: Newman's lemma [START_REF] Newman | On theories with a combinatorial definition of "equivalence[END_REF]. Since then, rewriting theory has been mainly developed in theoretical computer science, producing numerous variants corresponding to different syntaxes of the formulas being transformed: string, terms, terms modulo, λ-terms, termgraphs, etc. Rewriting is also present in other computational formalisms such as Petri nets or logical systems.

More recently, higher-dimensional rewriting has unified several paradigms of rewriting. This approach is based on presentations by generators and relations of higher-dimensional categories, independently introduced by Albert Burroni and Ross Street under the respective names of polygraphs in [START_REF] Burroni | Higher-dimensional word problems with applications to equational logic[END_REF] and computads in [START_REF] Street | Limits indexed by category-valued 2-functors[END_REF][START_REF]The algebra of oriented simplexes[END_REF]. Those algebraic objects have been subsequently developed in rewriting theory, fixing the terminology to polygraph in that field [Mét03, Gui06, Laf07, Mét08, GM09, Mim10, GM11, GM12a, GM12b, GMM13, GGM].

The main useful property of polygraphs is to encapsulate, in the same globular object, an algebraic structure corresponding to the syntax of the terms and to the computations on the terms, together with a homotopical structure describing the properties of the computations. As a consequence, polygraphs provide a natural setting to formulate Squier's theory, based on the discovery of deep relations between the computational, the homological and the homotopical properties of presentations by generators and relations.

From computational to homological properties. The normal-form procedure proves that, if a monoid admits a finite convergent presentation, then it has a decidable word problem. The converse implication was still an open problem in the middle of the eighties:

Question. [Jan82, Jan85] Does every finitely presented monoid with a decidable word problem admit a finite convergent presentation?

In [START_REF] Kapur | A finite Thue system with decidable word problem and without equivalent finite canonical system[END_REF], Deepak Kapur and Paliath Narendran consider Artin's presentation of the monoid B 3 of positive braids on three strands xs, t | sts ñ tsty.

Kapur and Narendran proved that B 3 admits no finite convergent presentation on the two generators s and t. However, they also proved one gets a finite convergent presentation of B 3 by adjunction of a new generator a standing for the product st: d s, t, a § § ta α ùñ as, st β ùñ a, sas γ ùñ aa, saa δ ùñ aat h .

(1)

As a consequence, the word problem for B 3 is solvable. The result of Kapur and Narendran shows that the existence of a finite convergent presentation depends on the chosen generators. Thus, to provide the awaited negative answer to the open question, one would have to exhibit a monoid with a decidable word problem but with no finite convergent presentation for any possible set of generators: new methods had to be introduced. And, indeed, Craig Squier answered the question by linking the existence of a finite convergent presentation for a given monoid M to an invariant of the monoid: the homological type left-FP 3 . Here, invariant is to be taken in the sense that it is independent of the choice of a presentation of M and, in particular, of a generating set. A monoid M is of homological type left-FP 3 if there exists an exact sequence P 3 / / P 2 / / P 1 / / P 0 / / Z / / 0 of projective and finitely generated (left) ZM-modules, where Z denotes the trivial ZM-module. From a presentation Σ of a monoid M, one can build an exact sequence of free ZM-modules

ZMrΣ 2 s d 2 / / ZMrΣ 1 s d 1 / / ZM ε / / Z / / 0, (2)
where ZMrΣ k s is the free ZM-module over Σ k . In [START_REF] Squier | Word problems and a homological finiteness condition for monoids[END_REF], Squier proved that, when Σ is convergent, its critical branchings form a generating set of the kernel of d 2 , where a critical branching of Σ is a minimal

Introduction

overlapping application of two relations on the same word of Σ ¦ 1 . For example, the relations α : ta ñ as and β : st ñ a generate a critical branching pβa, sαq on sta: aa sta βa 9 ; sα 5 7 sas

The convergence of Σ ensures that every critical branching pf, gq is confluent, that is, it can be completed by rewriting sequences f I and g I as in

v f I ' u f @ < g 4 6 u I w g I W M (3)
For example, the presentation (1) of B 3 has four critical branchings, and all of them are confluent: Squier proved that the set Σ 3 of critical branchings of a convergent presentation Σ extends the exact sequence (2) by one step:

ZMrΣ 3 s d 3 / / ZMrΣ 2 s d 2 / / ZMrΣ 1 s d 1 / / ZM ε / / Z / / 0, (4)
where the boundary map d 3 is defined on the generic branching (3) by d 3 pf, gq rfs ¡ rgs rf I s ¡ rg I s, where r¤s satisfies

r u 1 α 1 v 1 ùñ ¤ ¤ ¤ u n α n v n ùñ s u 1 rα 1 s ¤ ¤ ¤ u n rα n s. 1. Introduction with ab α ùñ 1 , x i a β i ùñ atx i , x i t γ i ùñ tx i , x i b δ i ùñ bx i , x i y i ε i ùñ 1.
Each S k is a finitely generated monoid with a decidable word problem. But, for k ¥ 2, the monoid S k is not of homological type left-FP 3 and, as a consequence, it does not admit a finite convergent presentation. Thus, Squier gave a negative answer to the open question: there exist finitely generated monoids with a decidable word problem that do not admit a finite convergent presentation (for any possible finite set of generators).

Finite derivation type. Given a monoid M with a presentation Σ, Squier considers in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] the presentation complex of Σ, that is a cellular complex with one 0-cell, whose 1-cells are the elements of the free monoid Σ ¦ 1 and whose 2-cells are generated by the relations of Σ 2 . More precisely, the 2-cells of the presentation complex are constructed as follows. We denote by Σ ¡ 2 the set obtained by reversing the relations of Σ 2 :

Σ ¡ 2 2 v α ¡ ùñ u such that u α ùñ v is in Σ 2 @ .
There is a 2-cell in the presentation complex between each pair of words with shape wuw I and wvw

I such that Σ 2 b Σ ¡ 2 contains a relation u ñ v.
Then, Squier extends this 2-dimension complex with 3-cells filling all the squares formed by independent applications of relations, such as the following one,

where

u 1 ñ v 1 and u 2 ñ v 2 are in Σ 2 b Σ ¡ 2 :
wv 1 w I u 2 w P ( 0

wu 1 w I u 2 w P A = 3 5 wv 1 w I v 2 w P wu 1 w I v 2 w P F B
We will see that, in the 2-categorical formulation of this complex that we consider, this 3-cell corresponds to the so-called exchange relations.

A homotopy basis of Σ is a set Σ 3 of additional 3-cells that makes Squier's complex aspherical, i.e. such that every 2-dimensional sphere can be "filled" by the 3-cells of Σ 3 . The presentation Σ is of finite derivation type if it admits a finite homotopy basis. Squier proved that the finite derivation type property is an intrinsic property of the presented monoid: 4.2.3. Theorem [SOK94, Theorem 4.3] Let Σ and Ξ be two finite presentations of the same monoid. Then Σ has finite derivation type if and only if Ξ has finite derivation type.

The proof given by Squier is based on Tietze transformations. In these notes, we give another proof based on a homotopy bases transfer theorem, Theorem 4.2.2. As a consequence of Theorem 4.2.3, we can define the condition of finite derivation type for monoids independently of a considered presentation: a monoid is of finite derivation type if its finite presentations are of finite derivation type.

Introduction

From computational to homotopical properties. In [START_REF] Squier | A finiteness condition for rewriting systems[END_REF], Squier links the existence of a finite convergent presentation to the homotopical property of finite derivation type. He proves that, given a convergent presentation Σ, it is sufficient to consider one 3-cell filling the diagram (3) for each critical branching to get a homotopy basis of Σ. Such a set of 3-cells is called a family of generating confluences of Σ.

Theorem [SOK94, Theorem 5.2]

Let Σ be a convergent presentation of a monoid. Every family of generating confluences of Σ is a homotopy basis.

Moreover, if Σ is finite, the presentation Σ has finitely many critical branchings. 4.3.3. Theorem [SOK94, Theorem 5.3] If a monoid admits a finite convergent presentation, then it is of finite derivation type.

In [START_REF] Squier | A finiteness condition for rewriting systems[END_REF], Squier used Theorem 4.3.3 to give another proof that there exist finitely generated monoids with a decidable word problem that do not admit a finite convergent presentation. Moreover, he showed that the homological finiteness condition left-FP 3 is not sufficient for a finitely presented monoid with a decidable word problem to admit a finite convergent presentation. Indeed, the monoid S 1 given by the presentation d a, b, t, x, y § § ab ñ 1, xa ñ atx, xt ñ tx, xb ñ bx, xy ñ 1 h has a decidable word problem, admits a finite presentation and is of homological type left-FP 3 , yet it is not of a finite derivation type (and, thus, it does not admit a finite convergent presentation). This example is entirely developed in Section 6.1.

Refinements of Squier's conditions. Squier's homological and homotopical finiteness conditions are related: finite derivation type implies homological type left-FP 3 , as proved by several authors [START_REF] Cremanns | Finite derivation type implies the homological finiteness condition FP 3[END_REF][START_REF] Stephen | Low-dimensional homotopy theory for monoids[END_REF][START_REF] Lafont | A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier)[END_REF]. The converse implication is false in general, as already noted above with the monoid S 1 , but it is true in the special case of groups [START_REF]For groups the property of having finite derivation type is equivalent to the homological finiteness condition FP 3[END_REF]. Squier has proved in [START_REF] Squier | A finiteness condition for rewriting systems[END_REF] that the invariant homological type left-FP 3 is a necessary, but not sufficient condition for a monoid to admit a finite convergent presentation, the same question being still open for the homotopical invariant finite derivation type. After Squier, various refinements of both invariants have been explored, in the quest for a complete characterisation of the existence of finite convergent presentations of monoids.

In the homological direction, thanks to the notion of abelian resolution, one defines the more restrictive conditions homological type left-FP n , for every natural number n ¡ 3, and homological type left-FP V : a monoid M has homological type left-FP V if there exists a resolution of the trivial ZM-module by finitely generated and projective ZM-modules. In [START_REF] Kobayashi | Complete rewriting systems and homology of monoid algebras[END_REF], a notion of n-fold critical branching is used to complete the exact sequence (4) into a resolution, obtaining the following implication: if a monoid admits a finite convergent presentation, then it is of homological type left-FP V , the converse implication still being false in general. The same results are also known for associative algebras presented by a finite Gröbner basis [START_REF] Anick | On the homology of associative algebras[END_REF] and for groups [START_REF] Daniel | A monoid which is right FP 8 but not left FP 1[END_REF][START_REF] Brown | The geometry of rewriting systems: a proof of the Anick-Groves-Squier theorem, Algorithms and classification in combinatorial group theory[END_REF][START_REF] John | Rewriting systems and homology of groups, Groups -Canberra[END_REF]. One can obtain similar implications with the properties right-FP V and bi-FP V , defined with resolutions by right modules and bimodules, respec- tively. In [START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF], the authors give a construction of a resolution involving n-fold critical branchings and based on the notion of normalisation strategy.

In the homotopical direction, the condition finite derivation type has been refined into FDT 4 , a property about the existence of a finite presentation with a finite homotopy basis, itself satisfying a homotopical finiteness property [START_REF] Mcglashan | Pride, Finiteness conditions for rewriting systems[END_REF]. The condition FDT 4 is also necessary for a monoid to admit a finite convergent presentation and it is sufficient, but not necessary, for having the conditions homological type left/right/bi-FP 4 . Higher-dimensional finite derivation type properties, called FDT n , are defined in [START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF], as a generalisation in any dimension of Squier's finite derivation type. A monoid with a finite convergent presentation is FDT V and, for any n, the property FDT n implies the homological type FP n [START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF].

Organisation and prerequisites. In Section 2, we consider presentations of monoids (and, more generally, of categories) by 2-polygraphs, and we explain their main rewriting properties in Section 3. In Section 4, we introduce the property of finite derivation type for categories using the structure of 3polygraph and, in Section 4.3, we relate convergence and finite derivation type. This survey is rather self-contained, but wider categorical notions are covered in more detail by Mac Lane in [START_REF] Mac | Categories for the working mathematician[END_REF] and by Barr and Wells in [START_REF] Barr | Category theory for computing science[END_REF]. For notions of rewriting theory, one can refer to Baader and Nipkow [START_REF] Baader | Term rewriting and all that[END_REF], Terese [START_REF]Term rewriting systems[END_REF] and Book and Otto [START_REF] Book | String-rewriting systems[END_REF] for the special case of string rewriting. For extension of the finite derivation type property to higher-dimensional rewriting systems, we refer the reader to [START_REF] Guiraud | Higher-dimensional categories with finite derivation type[END_REF].

LOW-DIMENSIONAL CATEGORIES AND POLYGRAPHS

2.1. Categories and functors 2.1.1. Categories. A category (or 1-category) is a data C made of a set C 0 , whose elements are called the 0-cells of C, and, for all 0-cells x and y of C, of a set Cpx, yq, whose elements are called the 1-cells from x to y of C. Those sets are equipped with the following algebraic structure: ¡ for all 0-cells x, y and z of C, a map, called the composition (or 0-composition) of C, γ x,y,z : Cpx, yq ¢ Cpy, zq Ñ Cpx, zq, ¡ for every 0-cell x of C, a specified element 1 x of Cpx, xq, called the identity of x.

The following relations are required to hold, where we write u : x Ñ y to mean that u belongs to Cpx, yq:

¡ the composition is associative, i.e. for all 0-cells x, y, z and t and for all 1-cells u : x Ñ y, v : y Ñ z and w : z Ñ t of C , γ x,z,t pγ x,y,z pu, vq, wq γ x,y,t pu, γ y,z,t pv, wqq, ¡ the identities are local units for the composition, i.e. for all 0-cells x and y and for every 1-cell u : x Ñ y of C, γ x,x,y p1 x , uq u γ x,y,y pu, 1 y q. A groupoid is a category where every 1-cell has an inverse, that is, for every 1-cell u : x Ñ y, there exists a (necessarily unique) 1-cell u ¡ : y Ñ x such that γ x,y,x pu, u ¡ q 1 x and γ y,x,y pu ¡ , uq 1 y .

Low-dimensional categories and polygraphs

2.1.2. A globular point of view. A category C can also be seen as a graph

C 0 C 1 t 0 o o s 0 o o
where C 1 is the disjoint union of all the hom-sets Cpx, yq, and the maps s 0 and t 0 send a 1-cell u : x Ñ y to its source x and its target y, respectively. We usually simply write spuq and tpuq instead of s 0 puq and t 0 puq. The composition of C equips this graph with a partial function

0 : C 1 ¢ C 1 Ñ C 1
mapping a pair pu, vq of composable 1-cells (i.e. such that tpuq spvq) to u 0 v (we often simply write uv). By definition, the source and target of a composite 1-cell are given by spu 0 vq spuq and tpu 0 vq tpvq.

Moreover, the associativity axiom is written as pu 0 vq 0 w u 0 pv 0 wq.

The identities define an inclusion C 0 C 1 that maps each 0-cell x to the 1-cell 1 x . By definition, the source and target of an identity 1-cell are sp1 x q x and tp1 x q x.

Finally, the unit axioms become

1 x 0 u u u 0 1 y .
This globular definition of categories is equivalent to the original definition given in 2.1.1.

2.1.3. Functors. Let C and D be categories. A functor F : C Ñ D is a data made of a map F 0 : C 0 Ñ D 0 and, for all 0-cells x and y of C, a map F x,y : Cpx, yq Ñ DpFpxq, Fpyqq, such that the following relations are satisfied:

¡ for all 0-cells x, y and z and all 1-cells u : x Ñ y and v : y Ñ z of C, F x,z pu 0 vq F x,y puq 0 F y,z pvq, ¡ for every 0-cell x of C, F x,x p1 x q 1 Fpxq . We often just write Fpxq for F 0 pxq and Fpuq for F x,y puq. A functor F is an isomorphism if the map F 0 and each map F x,y is a bijection. We denote by Id C the identity functor on C. Morphisms of monoids are exactly the functors between the corresponding categories with one 0-cell.

The word problem

2.2.1. 1-polygraphs. A 1-polygraph is a graph Σ, i.e. a diagram of sets and maps

Σ 0 Σ 1 . t 0 o o s 0 o o
The elements of Σ 0 and Σ 1 are called the 0-cells and the 1-cells of Σ, respectively. If there is no confusion, we just write Σ pΣ 0 , Σ 1 q. A 1-polygraph is finite if it has finitely many 0-cells and 1-cells.

Free categories.

If Σ is a 1-polygraph, the free category over Σ is the category denoted by Σ ¦ and defined as follows:

¡ the 0-cells of Σ ¦ are the ones of Σ, ¡ the 1-cells of Σ ¦ from x to y are the finite paths of Σ, i.e. the finite sequences

x u 1 ÝÑ x 1 u 2 ÝÑ x 2 u 3 ÝÑ ¤ ¤ ¤ u n¡1 ÝÑ x n¡1 u n ÝÑ y of 1-cells of Σ,
¡ the composition is given by concatenation, ¡ the identities are the empty paths.

If Σ has only one 0-cell, then the 1-cells of the free category Σ ¦ form the free monoid over the set Σ 1 .

2.2.3. Generating 1-polygraph. Let C be a category. A 1-polygraph Σ generates C if there exists a functor π : Σ ¦ C that is the identity on 0-cells and such that, for all 0-cells x and y of C, the map π x,y : Σ ¦ px, yq Cpx, yq is surjective. We usually consider that π is implicitly specified for a given generating 1-polygraph Σ and, if u is a 1-cell of Σ ¦ , we just write u instead of πpuq. A category is finitely generated if it admits a finite generating 1-polygraph (in particular, the category must have finitely many 0-cells).

2.2.4. The word problem for categories. Let C be a category. The word problem for C is the problem of finding a generating 1-polygraph Σ for C together with an algorithm that decides, for any two 1-cells u and v of Σ ¦ , whether or not u v holds in C (that is, whether or not the 1-cells u and v represent the same 1-cell of C). We note that, to have u v, it is necessary for u and v to be parallel, i.e. they must have the same source and the same target. The word problem is undecidable in general for a given category C, even if it is finitely generated. However, a finite convergent presentation of C, see 3.1.7, provides a solution to the word problem for C.

Presentations of categories

2.3.1. Spheres and cellular extensions of categories. A 1-sphere of a category C is a pair γ pu, vq of parallel 1-cells of C, that is, with the same source and the same target; such a 1-sphere is denoted by γ : u ñ v. The 1-cell u is the source of γ and v is its target. A cellular extension of C is a set Γ equipped with a map from Γ to the set of 1-spheres of C.

Congruences.

A congruence on a category C is an equivalence relation on the parallel 1-cells ¡ the 0-cells of C{Γ are the ones of C, ¡ for all 0-cells x and y of C, the hom-set C{Γ px, yq is the quotient of Cpx, yq by the restriction of Γ .

of C that is compatible with the composition of C, that is, for all 1-cells x w / / y u ! ! v = = z w I / / t of C such that u v,
We denote by π Γ : C C{Γ the canonical projection. When the context is clear, we just write π for π Γ and u for the image through π of a 1-cell u of C.

2-polygraphs.

A 2-polygraph is a triple Σ pΣ 0 , Σ 1 , Σ 2 q made of a 1-polygraph pΣ 0 , Σ 1 q, often simply denoted by Σ 1 , and a cellular extension Σ 2 of the free category Σ ¦

1 . In other terms, a 2-polygraph Σ is a 2-graph Σ 0 Σ ¦ 1 t 0 o o s 0 o o Σ 2 t 1 o o s 1 o o
whose 0-cells and 1-cells form a free category. The elements of Σ k are called the k-cells of Σ and Σ is finite if it has finitely many cells in every dimension.

Presentations of categories.

If Σ is a 2-polygraph, the category presented by Σ is the category denoted by Σ and defined by ¡ adjunction or elimination of a generating 1-cell x and of a generating 2-cell α : u ñ x, where u is a 1-cell of the free category over Σ 1 z txu, ¡ adjunction or elimination of a generating 2-cell α : u ñ v such that u Σ 2 ztαu v.

Σ Σ ¦ 1 {Σ 2 . If C is a category, a presentation of C is a 2-polygraph Σ such that C is isomorphic to Σ. In that case,

Two-dimensional categories

2.4.1. 2-categories. A 2-category is a data C made of a set C 0 , whose elements are called the 0-cells of C, and, for all 0-cells x and y of C, a category Cpx, yq, whose 0-cells and 1-cells are respectively called the 1-cells and the 2-cells from x to y of C. This data is equipped with the following algebraic structure:

¡ for all 0-cells x, y and z of C, a functor γ x,y,z : Cpx, yq ¢ Cpy, zq Ñ Cpx, zq, ¡ for every 0-cell x of C, a specified 0-cell 1 x of the category Cpx, xq.

The following relations are required to hold: ¡ the composition is associative, i.e. for all 0-cells x, y, z and t of C, γ x,z,t ¥ pγ x,y,z ¢ Id Cpz,tq q γ x,y,t ¥ pId Cpx,yq ¢γ y,z,t q, ¡ the identities are local units for the composition, i.e. for all 0-cells x and y of C, γ x,x,y ¥ p1 x ¢ Id Cpx,yq q Id Cpx,yq γ x,y,y ¥ pId Cpx,yq ¢1 y q.

This definition of 2-categories is usually stated as follows: a 2-category is a category enriched in categories. A p2, 1q-category is a 2-category whose 2-cells are invertible for the 1-composition: in other terms, it is a 2-category whose hom-categories are groupoids.

The globular point of view.

A 2-category can, equivalently, be defined as a 2-graph

C 0 C 1 t 0 o o s 0 o o C 2 t 1 o o s 1 o o
equipped with an additional algebraic structure. The definition of 2-graph requires that the source and target maps satisfy the globular relations:

s 0 ¥ s 1 s 0 ¥ t 1 and t 0 ¥ s 1 t 0 ¥ t 1 .
The 2-graph is equipped with two compositions, the 0-composition 0 and the 1-composition 1 , respectively defined on 0-composable 1-cells and 2-cells, and on 1-composable 2-cells. We also have an inclusion of C 0 into C 1 given by the identities of the 2-category, and an inclusion of C 1 into C 2 induced by the identities of the hom-categories. In details, we have the following operations:

¡ for all 1-cells x u ÝÑ y v ÝÑ z, a 0-composite 1-cell x u 0 v ÝÑ z, ¡ for all 2-cells x u u I @ @ f Õ y v v I B B g Õ z , a 0-composite 2-cell x u 0 v u I 0 v I ? ? f 0 g Õ z , ¡ for all 2-cells x u v / / w D D f Õ g Õ y , a 1-composite 2-cell x u w > > f 1 g Õ y ,
¡ for every 0-cell x, an identity 1-cell x 1 x ÝÑ x, ¡ for every 1-cell x u ÝÑ y, an identity 2-cell u 1 u ùñ u.

The following relations hold:

¡ for all 1-cells x u ÝÑ y v ÝÑ z w ÝÑ t, pu 0 vq 0 w u 0 pv 0 wq, ¡ for every 1-cell x u ÝÑ y, 1 x 0 u u u 0 1 y , ¡ for all 1-cells x u ÝÑ y v ÝÑ z, 1 u 0 v 1 u 0 1 v , ¡ for all 2-cells u f ùñ v g ùñ w h ùñ x, pf 1 gq 1 h f 1 pg 1 hq, ¡ for all 2-cells x u u I @ @ f Õ y v v I B B g Õ z w w I B B h Õ t , pf 0 gq 0 h f 0 pg 0 hq, ¡ for every 2-cell x u v @ @ f Õ y , 1 x 0 f f f 0 1 y , ¡ for every 2-cell u f ùñ v, 1 u 1 f f f 1 1 v , ¡ for all 2-cells x u u I / / u P B B f Õ f I Õ y v v I / / v P C C g Õ g I Õ z
, pf 1 f I q 0 pg 1 g I q pf 0 gq 1 pf I 0 g I q.

The last relation is usually called the exchange relation or the interchange law for the compositions 0 and 1 . This globular definition of 2-categories is equivalent to the enriched one. In particular, the 0-composition of 2-cells with identity 2-cells defines the whiskering operations ¡ for all cells x w / / y u v @ @ f Õ z , the left whiskering x w 0 u w 0 v ? ?

w 0 f Õ z , ¡ for all cells x u v ? ? f Õ y w / / z , the right whiskering x u 0 w v 0 w ? ? f 0 w Õ z ,
that satisfy the following relations, implied by the exchange and associativity relations:

¡ for all cells x u / / y v v I / / v P D D f Õ f I Õ z , u 0 pf 1 f I q pu 0 fq 1 pu 0 f I q, ¡ for all cells x u u I / / u P C C f Õ f I Õ y v / / z , pf 1 f I q 0 v pf 0 vq 1 pf I 0 vq, ¡ for all cells x u / / y v / / z w w I A A f Õ t , pu 0 vq 0 f u 0 pv 0 fq, ¡ for all cells x u / / y v v I @ @ f Õ z w / / t , pu 0 fq 0 w u 0 pf 0 wq, ¡ for all cells x u u I ? ? f Õ y v / / z w / / t , pf 0 vq 0 w f 0 pv 0 wq,
As for categories, we usually omit the 0 notation. For 2-cells, we write s and t instead of s 1 and t 1 .

Low-dimensional categories and polygraphs

2.4.3. Free 2-categories. Let Σ be a 2-polygraph. The free 2-category over Σ is denoted by Σ ¦ and defined as follows:

¡ the 0-cells of Σ ¦ are the ones of Σ, ¡ for all 0-cells x and y of Σ, the hom-category Σ ¦ px, yq is presented by the 2-polygraph whose 0-cells are the 1-cells from x to y of Σ ¦ , whose 1-cells are the

x w / / y u ! ! v = = α Õ z w I / / t with α : u ñ v in Σ 2 and w and w I in Σ ¦ 1 ,
with one 2-cell with source αwv 1 u I wβ and target uwβ 1 αwv I , for all α : u ñ u I and

β : v ñ v I in Σ 2 and w in Σ ¦ 1 ,
¡ for all 0-cells x, y and z of Σ the composition functor is given by the concatenation on 1-cells and, on 2-cells, by

u 1 α 1 u I 1 1 ¤ ¤ ¤ 1 u m α m u I m ¨0 v 1 β 1 v I 1 1 ¤ ¤ ¤ 1 v n β n v I n ¨ u 1 α 1 u I 1 v 1 spβ 1 qv I 1 1 ¤ ¤ ¤ 1 u m α m u I m v 1 spβ 1 qv I 1 1 u m tpα m qu I m v 1 β 1 v I 1 1 ¤ ¤ ¤ 1 u m tpα m qu I m v n β n v I n ,
¡ for every 0-cell x of Σ, the identity 1-cell 1 x is the one of Σ ¦ 1 .

By definition of the 2-category Σ ¦ , for all 1-cells u and v of Σ ¦ , we have u v in the quotient category Σ if, and only if, there exists a zigzag sequence of 2-cells of Σ ¦ between them:

u f 1 7 9 u 1 v 1 g 1 e y f 2 7 9 u 2 p¤ ¤ ¤ q e y 7 9 u n¡1 v n¡1 g n¡1 e y f n 7 9 u n v. g n e y
2.4.4. Free p2, 1q-categories. If Σ is a 2-polygraph, the free p2, 1q-category over Σ is denoted by Σ t and is defined as the 2-category whose 0-cells are the ones of Σ and, for all 0-cells x and y, the homcategory Σ t px, yq is given as the quotient

Σ t px, yq Σ b Σ ¡ q ¦ px, yq v InvpΣ 2 q,
where:

¡ the 2-polygraph Σ ¡ is obtained from Σ by reversing its 2-cells, ¡ the cellular extension InvpΣ 2 q contains the following two relations for every 2-cell α of Σ and all possible 1-cells u and v of Σ ¦ such that spuq x and tpvq y: uαv 1 uα ¡ v 1 uspαqv and uα ¡ v 1 uαv 1 utpαqv .

By definition of the p2, 1q-category Σ t , for all 1-cells u and v of Σ ¦ , we have u v in the quotient category Σ if, and only if, there exists a 2-cell f : u ñ v in the p2, 1q-category Σ t .

REWRITING PROPERTIES OF 2-POLYGRAPHS

Convergent presentations of categories

Let us fix a 2-polygraph Σ.

3.1.1. Rewriting and normal forms. A rewriting step of Σ is a 2-cell of the free 2-category Σ ¦ with shape

x w / / y u ! ! v = = ϕ Õ z w I / / t
where ϕ : u ñ v is a 2-cell of Σ and w and w I are 1-cells of Σ ¦ . A rewriting sequence of Σ is a finite or infinite sequence u 1 f 1 7 9 u 2 f 2 7 9 p¤ ¤ ¤ q f n¡1 7 9 u n f n 7 9 p¤ ¤ ¤ q of rewriting steps. If Σ has a rewriting sequence from u to v, we say that u rewrites into v. Let us note that every 2-cell f of Σ ¦ decomposes into a finite rewriting sequence of Σ, this decomposition being unique up to exchange relations. A 1-cell u of Σ ¦ is a normal form if Σ has no rewriting step with source u, and a normal form of u is a 1-cell v of Σ ¦ that is a normal form and such that u rewrites into v.

3.1.2. Termination. We say that Σ terminates if it has no infinite rewriting sequence. In that case, every 1-cell of Σ ¦ has at least one normal form and noetherian induction allows definitions and proofs of properties of 1-cells of Σ ¦ by induction on the size of the 2-cells leading to normal forms. A termination order on Σ is an order relation ¤ on parallel 1-cells of Σ ¦ such that the following properties are satisfied: ¡ the composition of 1-cells of Σ ¦ is strictly monotone in both arguments, ¡ every decreasing family pu n q nN of parallel 1-cells of Σ ¦ is stationary, ¡ for every 2-cell α of Σ, the strict inequality spαq ¡ tpαq holds.

As a direct consequence of the definition, if Σ admits a termination order, then Σ terminates. A useful example of termination order is the left degree-wise lexicographic order (or deglex for short) generated by a given order on the 1-cells of Σ. It is defined by the following strict inequalities, where the x i s and y j s are 1-cells of Σ:

x 1 ¤ ¤ ¤ x p y 1 ¤ ¤ ¤ y q , if p q, x 1 ¤ ¤ ¤ x k¡1 x k ¤ ¤ ¤ x p x 1 ¤ ¤ ¤ x k¡1 y k ¤ ¤ ¤ y p , if x k y k .
The deglex order is total if, and only if, the original order on 1-cells of Σ is total.

3.1.3. Branchings. A branching of Σ is a pair pf, gq of 2-cells of Σ ¦ 2 with a common source, as in v u f 8 : g 5 7 w

Rewriting properties of 2-polygraphs

The 1-cell u is the source of this branching and the pair pv, wq is its target. We do not distinguish the branchings pf, gq and pg, Local branchings are compared by "inclusion", i.e. by the order ¤ generated by the relations pf, gq ¤ ufv, ugvq

given for any local branching pf, gq and any possible 1-cells u and v of Σ ¦

1 . An overlapping local branching that is minimal for the order ¤ is called a critical branching (or a critical pair). The terms "aspherical" and "Peiffer" come from the corresponding notions for spherical diagrams in Cayley complexes associated to presentations of groups, [LS01], while "critical" is used in rewriting theory, [START_REF] Book | String-rewriting systems[END_REF][START_REF] Baader | Term rewriting and all that[END_REF].

3.1.4. Confluence. A branching v u f 8 : g 5 7 w
is confluent if there exist 2-cells f I and g I in Σ ¦ 2 , as in the following diagram:

v f I $ , u f 9 ; g 5 7 u I w g I S I
We say that Σ is confluent (resp. locally confluent) if all of its branchings (resp. local branchings) are confluent. If Σ is confluent, every 1-cell of Σ ¦ has at most one normal form.

Convergent presentations of categories

3.1.5. Lemma. A 2-polygraph is locally confluent if, and only if, all its critical branchings are confluent.

Proof. Every aspherical branching is confluent:

v 1 v ( u f 8 : f 6 8 v v 1 v S I
We also have confluence of every Peiffer local branching:

u I v u I g % - uv fv @ < ug 4 6 u I v I uv I fv I P F
We note that, in the aspherical and Peiffer cases, the 2-cells f I and g I can be chosen in such a way that

f 1 f I g 1 g I holds.
Finally, in the case of an overlapping but not minimal local branching pf, gq, there exist factorisations f uhv and g ukv with The following result, also called the diamond lemma, is implied by Theorem 4.3.2.

3.1.6. Theorem (Newman's lemma [New42, Theorem 3]). For terminating 2-polygraphs, local confluence and confluence are equivalent properties.

3.1.7. Convergent polygraphs. We say that Σ is convergent if it terminates and it is confluent. Such a Σ is called a convergent presentation of Σ, and of any category that is isomorphic to Σ. In that case, every 1-cell u of Σ ¦ 1 has a unique normal form, denoted by p u, so that we have u v in Σ if, and only if, p u p v holds in Σ ¦

1 . This defines a section Σ Σ ¦ 1 of the canonical projection Σ ¦ 1 Σ, mapping a 1-cell u of Σ to the unique normal form of its representative 1-cells in Σ ¦ , still denoted by p u. As a consequence, a finite and convergent 2-polygraph Σ yields a decision procedure for the word problem of the category Σ it presents: the normal-form procedure, which takes, as input, two 1-cells u 3. Rewriting properties of 2-polygraphs and v of Σ ¦ , and decides whether u v holds in Σ or not. For that, the procedure computes the respective normal forms p u and p v of u and v. Finiteness is used to test whether a given 1-cell u is a normal form or not, by examination of all the relations and their possible applications on u. Then, the equality u v holds in Σ if, and only if, the equality p u p v holds in Σ ¦ . If the procedure stops, it returns the 2-polygraph Σ. Otherwise, it builds an increasing sequence of 2polygraphs, whose limit is denoted by Σ. Note that the resulting 2-polygraph may depend on the order 3.3. Normalisation strategies of examination of the critical branchings. Also, if the starting 2-polygraph Σ is already convergent, then the Knuth-Bendix completion of Σ is Σ. By construction, the 2-polygraph Σ is convergent and, since all the operations performed by the procedure are Tietze transformations, it is Tietze-equivalent to Σ:

Transformations of 2-polygraphs

Theorem ([KB70]

). Any Knuth-Bendix completion Σ of a 2-polygraph Σ, equipped with a total termination order, is a convergent presentation of the category Σ. Moreover, the 2-polygraph Σ is finite if, and only if, the 2-polygraph Σ is finite and the Knuth-Bendix completion procedure halts.

Métivier-Squier reduction.

A 2-polygraph Σ is reduced if, for every 2-cell α : u ñ v of Σ, we have that u is a normal form for Σ 2 z tαu and that v is a normal form for Σ 2 . Given a convergent 2-polygraph Σ, the Métivier-Squier reduction of Σ is the 2-polygraph obtained by the procedure that successively performs the following operations:

1. The procedure replaces every generating 2-cell α : u ñ v by α : u ñ p u: u of Σ ¦ such that πpp uq u. In general, we cannot assume that the chosen section is functorial, i.e. that x uv p up v holds in Σ ¦ . However, we assume that p 1 x 1 x holds for every 0-cell x of C. Given a 1-cell u of Σ ¦ , we simply write p u for p u. Such a section being fixed, a normalisation strategy for Σ is a map

u α 7 9 v Õ p u Þ ÝÑ u α ( 0 v Õ p u 2. Next, if
σ : Σ ¦ 1 Ñ Σ ¦ 2 that sends every 1-cell u of Σ ¦ to a 2-cell u σ u ùñ p u of Σ t , such that σ p u 1 p u holds for every 1-cell u of Σ ¦ .
3.3.2. Left and right normalisation strategies. Let Σ be a 2-polygraph, with a chosen section. A normalisation strategy σ for Σ is a left one (resp. a right one) if it also satisfies

σ uv ¤ v σ p uv Õ ¤ u , , p u B B σ u # x uv 2 2 ¤ resp. σ uv ¤ v p v * * σ v { σ up v Õ ¤ u 4 4 x uv 2 2 ¤ ¨.
The 2-polygraph Σ always admits left and right normalisation strategies. For example, in the left case, let us arbitrarily choose a 2-cell σ ua : ua ñ x ua in Σ t , for every 1-cell u of Σ ¦ and every 1-cell a of Σ, such that p u u and ua is defined, with x ua $ ua. Then we extend σ into a left normalisation strategy for Σ by putting σ u 1 u if p u u (which implies σ 1x 1 1x ), and σ u σ v a 1 σ p va if p u $ u and u va with v in Σ ¦ and a in Σ.

Leftmost and rightmost normalisation strategies.

If Σ is a reduced 2-polygraph, then, for every 1-cell u of Σ ¦ , the set of rewriting steps with source u can be ordered from left to right: for two rewriting steps f vαv I and g wβw I with source u, we have f g if the length of v is strictly smaller than the length of w. If Σ is finite, then the order is total and the set of rewriting steps of source u is finite. Hence, this set contains a smallest element λ u and a greatest element ρ u , respectively called the leftmost and the rightmost rewriting steps on u. If, moreover, the 2-polygraph Σ terminates, the iteration of λ (resp. ρ) yields a normalisation strategy σ called the leftmost (resp. rightmost) normalisation strategy of Σ: σ u λ u 1 σ tpλuq presp. σ u ρ u 1 σ tpρuq q.

We prove, by noetherian induction, that the leftmost (resp. rightmost) normalisation strategy of Σ is a left (resp. right) normalisation strategy. The leftmost and rightmost normalisation strategies give a way to make constructive some of the results we present here. For example, they provide a deterministic choice of a confluence diagram v σpvq A congruence on a 2-category C is an equivalence relation on the parallel 2-cells of C that is compatible with the two compositions of C, that is, for all cells

x w / / y # # ; ; E E z w I / / t h Õ f Õ g Õ k Õ
of C such that f g, we have w 0 ph 1 f 1 kq 0 w I w 0 ph 1 g 1 kq 0 w I .

If Γ is a cellular extension of C, the congruence generated by Γ is denoted by Γ and defined as the smallest congruence such that, if Γ contains a 3-cell γ : f g, then f Γ g. The quotient 2-category of a 2-category C by a congruence relation is the 2-category, denoted by C{ , whose 0-cells and 1-cells are those of C and whose 2-cells are the equivalence classes of 2-cells of C modulo the congruence .

A homotopy basis of C is a cellular extension Γ of C such that, for every parallel 2-cells f and g of C, we have f Γ g, that is, the equality f g holds in the quotient 2-category C{ Γ . For instance, the set of 2-spheres of C forms a homotopy basis.

4.1.2. p3, 1q-polygraphs and coherent presentations. A p3, 1q-polygraph is a pair Σ pΣ 2 , Σ 3 q made of a 2-polygraph Σ 2 and a cellular extension Σ 3 of the free p2, 1q-category Σ t 2 over Σ 2 , as summarised in

Σ 0 Σ ¦ 1 t 0 o o s 0 o o Σ t 2 t 1 o o s 1 o o Σ 3 t 2 o o s 2 o o If C is a category, a coherent presentation of C is a p3, 1q-polygraph Σ pΣ 2 , Σ 3 q such that Σ 2 is a presentation of C and Σ 3 is a homotopy basis of Σ t 2 .
4.1.3. Finite derivation type. A 2-polygraph Σ is of finite derivation type if it is finite and if the p2, 1qcategory Σ t admits a finite homotopy basis. A category C is of finite derivation type if it admits a finite coherent presentation.

3-categories.

The definition of 3-category is adapted from the one of 2-category by replacement of the hom-categories and the composition functors by hom-2-categories and composition 2-functors. In particular, in a 3-category, the 3-cells can be composed in three different ways:

¡ by 0 , along their 0-dimensional boundary:

x u u I A A y f Õ f I Õ A 7 9 v v I A A z g Õ g I Õ B 7 9 Þ ÝÑ x uv u I v I > > z fg Õ f I g I Õ AB 7 9
¡ by 1 , along their 1-dimensional boundary:

x u v / / w B B y f Õ f I Õ g Õ g I Õ A 7 9 B 7 9 Þ ÝÑ x u w @ @ y f 1 g Õ f I 1 g I Õ A 1 B 7 9
¡ by 2 , along their 2-dimensional boundary:

x u v > > y f Õ g Õ h Õ A 7 9 B 7 9 Þ ÝÑ x u v > > y f Õ h Õ A 2 B 7 9
A p3, 1q-category is a 3-category whose 2-cells are invertible for the composition 1 and whose 3-cells are invertible for the composition 2 . This implies that 3-cells are also invertible for the composition 1 . 4.1.5. Free p3, 1q-categories. Given a p3, 1q-polygraph Σ, the free p3, 1q-category over Σ is denoted by Σ t and defined as follows:

¡ its underlying 2-category is the free p2, 1q-category Σ t 2 , ¡ its 3-cells are all the formal compositions by 0 , 1 and 2 of 3-cells of Σ, of their inverses and of identities of 2-cells, up to associativity, identity, exchange and inverse relations.

In particular, we get that Σ 3 is a homotopy basis of Σ t 2 if, and only if, for every pair pf, gq of parallel 2-cells of Σ t 2 , there exists a 3-cell A : f g in Σ t .

The homotopy basis transfer theorem

The objective of this section is to prove Theorem 4.2.3: given two finite presentations of the same category, both are of finite derivation type or neither is. Towards this goal, we prove Theorem 4.2.2, that allows transfers of homotopy bases between presentations of the same category. 4.2.1. Lemma. Let C be a category and let Σ and Ξ be presentations of C. There exist 2-functors F : Σ t Ñ Ξ t and G : Ξ t Ñ Σ t and, for every 1-cells u of Σ t and v of Ξ t , there exist 2-cells σ u : GFpuq ñ u and τ v : FGpvq ñ v in Σ t and Ξ t , such that the following conditions are satisfied:

¡ the 2-functors F and G induce the identity through the canonical projections onto C:

Σ t π Σ / / / / F C Id C Ξ t π Ξ / / / / C Σ t π Σ / / / / C Ξ t π Ξ / / / / G O O C Id C O O
¡ the 2-cells σ u and τ v are functorial in u and v: σ 1x 1 1x , τ 1y 1 1y , σ uu I σ u σ u I and τ vv I τ v τ v I.

Proof. Let us define F, the case of G being symmetric. On a 0-cell x of Σ, we take Fpxq x. If a : x Ñ y is a 1-cell of Σ, we choose, in an arbitrary way, a 1-cell Fpaq : x Ñ y in Ξ t such that π Ξ Fpaq π Σ paq.

Then, we extend F to every 1-cell of Σ t by functoriality. Let α : u ñ u I be a 2-cell of Σ. Since Σ is a presentation of C, we have π Σ puq π Σ pu I q, so that π Ξ Fpuq π Ξ Fpu I q holds. Using the fact that Ξ is a presentation of C, we arbitrarily choose a 2-cell Fpαq : Fpuq ñ Fpu I q in Ξ t . Then, we extend F to every 2-cell of Σ t by functoriality. Now, let us define σ, the case of τ being symmetric. Let a be a 1-cell of Σ. By construction of F and G, we have:

π Σ GFpaq π Ξ Fpaq π Σ paq.
Since Σ is a presentation of C, there exists a 2-cell σ a : GFpaq ñ a in Σ t . We extend σ to every 1-cell u of Σ t by functoriality.

Theorem.

Let C be a category, let Σ and Ξ be two presentations of C and let F, G and τ be chosen as in Lemma 4.2.1. If Γ is a homotopy basis of Σ t , then ∆ FpΓ q b τ Ξ is a homotopy basis of Ξ t , where: for every 2-cell α : u ñ v of Ξ.

Proof. Let us define, for every 2-cell f of Ξ t , a 3-cell τ f of ∆ t with shape

FGpvq τ v $ , τ f Õ FGpuq FGpfq A = τ u 5 7 v u f I E
We extend the notation τ α in a functorial way, according to the formulas τ 1u 1 τu , τ fg τ f τ g ,

τ f 1 g FGpwq τ w % - τ g Õ FGpvq FGpgq A = τ v 0 2 τ f Õ w FGpuq FGpfq A = τ u 6 8 v g P F u f I E and τ f ¡ u f % - τ ¡ f Õ FGpvq FGpfq ¡ 7 9 FGpuq τ u 9 ; FGpfq 3 5 v f ¡ 7 9 u FGpvq τ v P F
One checks that the 3-cells τ f are well-defined, i.e. that their definition is compatible with the relations on 2-cells of Ξ t , such as the exchange relation:

τ fg 1 hk τ pf 1 hqpg 1 kq .

The homotopy basis transfer theorem

Now, let us consider parallel 2-cells f, g : u ñ v of Ξ t . The 2-cells Gpfq and Gpgq of Σ t are parallel so that, since Γ is a homotopy basis of Σ t , there exists a 3-cell

Gpuq

Gpfq

& .

Gpgq

H D A Õ Gpvq in Γ t . An application of F to A gives the 3-cell FGpuq FGpfq & . FGpgq H D FpAq Õ FGpvq of Ξ t , which
, by definition of ∆ and functoriality of F, is in ∆ t . Using the 3-cells FpAq, τ f and τ g , we get the following 3-cell from f to g in ∆ t :

u f ( τ ¡ u 7 9 g T J FGpuq FGpfq # + FGpgq Q G FGpvq τ v 7 9 v τ ¡ u 1 τ ¡ f Õ FpAq Õ τ ¡ u 1 τ g Õ
This concludes the proof that ∆ FpΓ q b τ Ξ is a homotopy basis of the p2, 1q-category Ξ t .

We deduce from Theorem 4.2.2 the following result.

Theorem ([SOK94, Theorem 4.3]).

Let Σ and Ξ be finite presentations of the same category. Then Σ is of finite derivation type if, and only if, Ξ is of finite derivation type.

The following proposition is useful to prove that a presentation admits no finite homotopy basis.

Proposition.

Let Σ be a 2-polygraph and let Γ be a homotopy basis of Σ t . If Σ admits a finite homotopy basis, then there exists a finite subset of Γ that is a homotopy basis of Σ t .

Proof. Let ∆ be a finite homotopy basis of Σ and let δ be a 3-cell of ∆. Since Γ is a homotopy basis of Σ, there exists a 3-cell A δ in Γ t with boundary pspδq, tpδqq. This induces a 3-functor F : ∆ t Ñ Γ t that is the identity on Σ and such that Fpδq A δ for every 3-cell δ of ∆. Let Γ ∆ be the subset of Γ that contains all the generating 3-cells that appear in the 3-cells A δ , for every δ in ∆. Since ∆ is finite and each A δ contains finitely many 3-cells of Γ , we have that Γ ∆ is finite. Finally, let us consider a 2-sphere pf, gq of Σ t . By hypothesis, there exists a 3-cell A in ∆ t with boundary pf, gq. By application of F, one gets a 3-cell FpAq in Γ t whose boundary is pf, gq. Moreover, the 3-cell FpAq is a composite of cells A δ : hence, the 3-cell FpAq is in Γ t ∆ . As a consequence, one gets f Γ ∆ g, so that Γ ∆ is a finite homotopy basis of Σ t , which concludes the proof.

Squier completion for convergent presentations

Squier completion provides a way to extend a convergent presentation of a category C into a coherent presentation of C. for every critical branching pf, gq of Σ. We note that, if Σ is confluent, it always admits a family of generating confluences. However, such a family is not necessarily unique, since the 3-cell can be directed in the reverse way and, for a given branching pf, gq, we can have several possible 2-cells f I and g I with the required shape. Normalisation strategies provide a deterministic way to construct a family of generating confluences, see [START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF]4.3.2].

For a convergent 2-polygraph Σ, Squier completion of Σ is the p3, 1q-polygraph denoted by SpΣq and defined by SpΣq pΣ, Γ q, where Γ is a chosen family of generating confluences of Σ. By the following result, if Σ is a convergent presentation of a category C, then Squier completion SpΣq is a coherent presentation of C.

Theorem ([SOK94, Theorem 5.2]).

Let Σ be a convergent 2-polygraph. Every family of generating confluences of Σ is a homotopy basis of Σ t .

Proof. We fix a family of generating confluences of Σ and consider the corresponding Squier completion SpΣq. We proceed in three steps.

Step 1. We prove that, for every local branching pf, gq : u ñ pv, wq of Σ, there exist 2-cells f I : v ñ u I and g I : w ñ u I in Σ ¦ and a 3-cell A : f 1 f I g 1 g I in SpΣq t , as in the following diagram:

v f I $ , A Õ u f 9 ; g 5 7 u I w g I R H
As we have seen in the study of confluence of local branchings, in the case of an aspherical or Peiffer branching, we can choose f I and g I such that f 1 f I g 1 g I : an identity 3-cell is enough to link them. Moreover, if we have an overlapping branching pf, gq that is not critical, we have pf, gq puhv, ukvq with ph, kq critical. We consider the 3-cell α : h 1 h I k 1 k I of SpΣq corresponding to the critical branching ph, kq and we conclude that the following 2-cells f I and g I and 3-cell A satisfy the required conditions:

f I uh I v g I uk I v A uαv.
Step 2. We prove that, for every parallel 2-cells f and g of Σ ¦ whose common target is a normal form, there exists a 3-cell from f to g in SpΣq t . We proceed by noetherian induction on the common source u of f and g, using the termination of Σ. Let us assume that u is a normal form: then, by definition, both 2-cells f and g must be equal to the identity of u, so that 1 1u : 1 u 1 u is a 3-cell of SpΣq t from f to g. Now, let us fix a 1-cell u of Σ ¦ with the following property: for every 1-cell v of Σ ¦ such that u rewrites into v in one step, and for every parallel 2-cells f, g : v ñ p v p u of Σ ¦ , there exists a 3-cell from f to g in SpΣq t . Let us consider parallel 2-cells f, g : u ñ p u and let us prove the result by progressively constructing the following composite 3-cell from f to g in SpΣq t :

u 1 f I 1 ! ) f 2 % - A Õ u f $ g X N f 1 G C g 1 ' / u I h 7 9 p u v 1 g I 1 S I g 2 I E B Õ C Õ
Since u is not a normal form, we can decompose f f 1 1 f 2 and g g 1 1 g 2 so that f 1 and g 1 are rewriting steps. They form a local branching pf 1 , g 1 q and we build the 2-cells f I 1 and g I 1 of Σ ¦ together with the 3-cell A of SpΣq t , as in the first part of the proof. Then, we consider a 2-cell h : u I ñ p u in Σ ¦ , that must exist by confluence of Σ and since p u is a normal form. We apply the induction hypothesis to the parallel 2-cells f 2 and f I 1 1 h in order to get B and, symmetrically, to the parallel 2-cells g I 1 1 h and g 2 to get C.

Step 3. We prove that every 2-sphere of Σ t is the boundary of a 3-cell of SpΣq t . First, let us consider a 2-cell f : u ñ v in Σ ¦ . Using the confluence of Σ, we choose 2-cells σ u : u ñ p u and

σ v : v ñ p v p u in Σ ¦ .
By construction, the 2-cells f 1 σ v and σ u are parallel and their common target p u is a normal form.

Thus, there exists a 3-cell in SpΣq t from f 1 σ v to σ u or, equivalently, a 3-cell σ f from f to σ u 1 σ ¡ ¡ for all 1-cells u : x Ñ y, v : y Ñ z and w : z Ñ t of C, one 3-cell

x uv p w γ uv,w & . p up v p w γ u,v p w @ < p uγ v,w 4 6 z uvw p u x vw γ u,vw P F α u,v,w Õ ¡ for every 1-cell u : x Ñ y of C, two 3-cells p 1 x p u γ 1x,u " p u ι x p u F B p u λ u Õ p u p 1 y γ u,1y " p u p uι y G C p u ρ u

Õ

Let us prove that Std 3 pCq is, indeed, a coherent presentation of C. The standard presentation Std 2 pCq is not terminating: indeed, for every 0-cell x of C, the 2-cell ι x creates infinite rewriting sequences

1 x ñ p 1 x ñ p 1 x p 1 x ñ p 1 x p 1 x p 1 x ñ ¤ ¤ ¤
However, we get a convergent presentation of C by reversing all the 2-cells ι x into ι ¡

x . Indeed, for termination, we consider the size of the 1-cells (the number of generators they contain) and we check that each 2-cell γ u,v has source of size 2 and target of size 1, while each 2-cell ι ¡

x has source of size 1 and target of size 0. As a consequence, for every non-identity 2-cell f : u ñ v of the free 2-category, the size of u is strictly greater than the size of v. For confluence, we study the critical branchings, divided into three families: ¡ for all 1-cells u : x Ñ y, v : y Ñ z and w : z Ñ t of C, one critical branching pγ u,v p w, p uγ v,w q, giving the 3-cell Indeed, the 3-sphere ω proves that the boundary of B is also the boundary of a 3-cell of the p3, 1qcategory pSp Σqz tBuq t . This elimination mechanism, based on the study of the triple critical branchings of Σ is part of the homotopical reduction procedure introduced in [GGM]. This construction coherently eliminates pairs of redundant cells of a coherent presentation. On this particular example, it yields that the p2, 1q-category Σ t admits an empty homotopy basis, i.e. that the p3, 1q-polygraph pΣ, rq is a coherent presentation of the monoid M.

A HOMOLOGICAL FINITENESS CONDITION

5.1. Monoids of finite homological type 5.1.1. Resolutions. Let M be a monoid. We denote by ZM the ring generated by M, that is, the free abelian group over M, equipped with the canonical extension of the product of M:

uM λ u u ¨ vM λ v v ¨ u ,vM λ u λ v uv wM u vw λ u λ v w.
Given a (left) ZM-module M, a resolution of M is an exact sequence of ZM-modules

p¤ ¤ ¤ q / / M n d n / / M n¡1 / / p¤ ¤ ¤ q / / M 2 d 2 / / M 1 d 1 / / M 0 d 0 / / M / / 0
that is, a sequence pM n q nN of ZM-modules, together with a sequence pd n q nN of morphisms of ZMmodules, called the boundary maps, such that d 0 is surjective and im d n 1 ker d n holds for every natural number n. In particular, the sequence pM n , d n q nN is a (chain) complex of ZMmodules, that is, we have the inclusion im d n 1 ker d n or, equivalently, the relation d n d n 1 0 holds for every natural number n. Such a resolution is called projective (resp. free) if all the modules M n are projective (resp. free). Given a natural number n, a partial resolution of length n of M is defined in a similar way but with a bounded sequence pM k q 0¤k¤n of ZM-modules.

5.1.2. Contracting homotopies. Given a complex of ZM-modules p¤ ¤ ¤ q

/ / M n 1 d n 1 / / M n d n / / M n¡1 / / p¤ ¤ ¤ q / / M 1 d 1 / / M 0 d 0 / / M / / 0
a method to prove that such a complex is a resolution of M is to construct a contracting homotopy, that is a sequence of morphisms of Z-modules p¤ ¤ ¤ q

M n 1 o o M n i n 1 o o M n¡1 i n o o p¤ ¤ ¤ q o o M 1 o o M 0 i 1 o o M i 0 o o
such that d 0 i 0 Id M and, for every n, we have

d n 1 i n 1 i n d n Id Mn .
Indeed, in that case, we have that d 0 is surjective. Moreover, for every natural number n and every x in ker d n , the equality d n 1 i n 1 pxq x holds, proving that x is in im d n 1 , so that ker d n im d n 1

holds. As a consequence, the considered complex is a resolution of M.

Homological type left-FP

n . If M is a monoid, the trivial ZM-module is the abelian group Z equipped with the trivial action un n, for every u in M and n in Z. A monoid M is of homological type left-FP n , for a natural number n, if there exists a partial resolution of length n of the trivial ZMmodule Z by projective, finitely generated ZM-modules:

P n d n / / P n¡1 d n¡1 / / p¤ ¤ ¤ q d 2 / / P 1 d 1 / / P 0 d 0 / / Z / / 0.
A monoid M is of homological type left-FP V if there exists a resolution of Z by projective, finitely generated ZM-modules.

5.1.4. Lemma. Let M be a monoid and let n be a natural number. The following assertions are equivalent:

Monoids of homological type left-FP 2

i) The monoid M is of homological type left-FP n .

ii) There exists a free, finitely generated partial resolution of the trivial ZM-module Z of length n are exact sequences of ZM-modules, with each P k and P I k finitely generated and projective, then the ZM-module Q is finitely generated if, and only if, the ZM-module Q I is finitely generated.

Monoids of homological type left-FP 2

5.2.1. Presentations and partial resolutions of length 2. Let M be a monoid and let Σ be a presentation of M. Let us define a partial resolution of length 2 of Z by free ZM-modules

ZMrΣ 2 s d 2 / / ZMrΣ 1 s d 1 / / ZM ε / / Z / / 0.
The ZM-modules ZMrΣ 1 s and ZMrΣ 2 s are the free ZM-modules over Σ 1 and Σ 2 , respectively: they contain the formal sums of elements denoted by urxs, where u is an element of M and x is a 1-cell of Σ or a 2-cell of Σ. Let us note that ZM is isomorphic to the free ZM-module over the singleton Σ 0 . The boundary maps are defined, on generators, by

ZM ε ÝÑ Z u Þ ÝÑ 1 ZMrΣ 1 s d 1 ÝÑ ZM rxs Þ ÝÑ x ¡ 1 ZMrΣ 2 s d 2 ÝÑ ZMrΣ 1 s rαs Þ ÝÑ rspαqs ¡ rtpαqs
The maps ε and d 2 are respectively called the augmentation map and the Reidemester-Fox Jacobian of Σ.

In the definition of d 2 , the bracket r¤s is extended to the 1-cells of Σ t thanks to the relation r1s 0 and ruvs rus urvs, for all 1-cells u and v of Σ.

Proposition.

Let M be a monoid and let Σ be a presentation of M. The sequence of ZM-modules ZMrΣ 2 s d2 / / ZMrΣ 1 s d1 / / ZM ε / / Z / / 0 is a partial free resolution of length 2 of Z.

Proof. We first note that the sequence is a chain complex. Indeed, the augmentation map is surjective by definition. Moreover, we have εd 1 rxs εpxq ¡ εp1q 1 ¡ 1 0, for every 1-cell x of Σ. In order to check that d 1 d 2 0, we first prove, by induction on the length, that we have d 1 rus u ¡1 for every 1-cell u of Σ t . For the unit, we have d 1 r1s d 1 p0q 0 and 1 ¡1 0.

Then, for a composite 1-cell uv such that the result holds for both u and v, we get

d 1 ruvs d 1 rus ud 1 rvs u ¡ 1 uv ¡ u uv ¡ 1.
As a consequence, we have d 1 d 2 rαs d 1 rspαqs ¡ d 1 rtpαqs spαq ¡ tpαq 0, for every 2-cell α of Σ, where the last equality comes from spαq tpαq, that holds since Σ is a presentation of M.

The rest of the proof consists in defining contracting homotopies i 0 , i 1 , i 2 :

ZMrΣ 2 s d 2 / / ZMrΣ 1 s d 1 / / i 2 o o ZM ε / / i 1 o o Z i 0 o o
We choose a representative p u in Σ ¦ From Proposition 5.2.2, we deduce the following result: 5.2.3. Theorem. The following properties hold. i) Every monoid is of homological type left-FP 0 .

ii) Every finitely generated monoid is of homological type left-FP 1 .

iii) Every finitely presented monoid is of homological type left-FP 2 . The monoid M is finitely generated and, thus, it is of homological type left-FP 1 . However, for every natural number n, we have d 2 rα n 1 s rat n 2 s ¡ rct n 1 s, rat n 1 s at n 1 rts ¡ rct n s ¡ ct n rts, d 2 rα n s pat n 1 ¡ ct n qrts. The monoid M is of homological type left-FP 1 , but not left-FP 2 . This is proved by showing that ker d 1 is not finitely generated as a ZM-module, which is tedious by direct computation in this case. Another way to conclude is to extend the partial resolution of Proposition 5.2.2 by one dimension: it will then be sufficient to compute im d 3 , which is trivial in this case because Σ has no critical branching, so that ker d 2 0 and, as a consequence, ker d 1 is isomorphic to ZMrΣ 2 s. Convergent presentations provide a method to obtain such a length-three partial resolution.

5.3. Squier's homological theorem 5.3.1. Coherent presentations and partial resolutions of length 3. Let M be a monoid and let Σ be a coherent presentation of M. Let us extend the partial resolution of 5.2.2 into the resolution of length 3

ZMrΣ 3 s d 3 / / ZMrΣ 2 s d 2 / / ZMrΣ 1 s d 1 / / ZM ε / / Z / / 0,
where the ZM-module ZMrΣ 3 s is the free ZM-module over Σ 3 , formed by the linear combination of elements urγs, with u in M and γ a 3-cell of Σ. The boundary map d 3 is defined, for every 3-cell γ of Σ, by d 3 rγs rs 2 pγqs ¡ rt 2 pγqs. The bracket r¤s is extended to 3-cells of Σ t thanks to the relations ruAvs urAs, rA 1 Bs rAs rBs, rA 2 Bs rAs rBs, for all 1-cells u and v and 3-cells A and B of Σ t such that the composites are defined. In particular, the latter relation implies r1 f s 0 for every 2-cell f of Σ t . We check, by induction on the size, that d 3 rAs rs 2 pAqs ¡ rt 2 pAqs holds for every 3-cell A of Σ t .

Proposition.

Let M be a monoid and let Σ be a coherent presentation of M. The sequence of ZM-modules

ZMrΣ 3 s d 3 / / ZMrΣ 2 s d 2 / / ZMrΣ 1 s d 1 / / ZM ε / / Z / / 0
is a partial free resolution of length 3 of Z.

Proof. We proceed with the same notations as the ones of the proof of Proposition 5.2.2, with the extra hypothesis that σ is a left normalisation strategy for Σ. This implies that i 2 purvsq rσpp uvqs holds for all u in M and v in Σ ¦ 1 , by induction on the length of v.

We have d 2 d 3 0 because s 1 s 2 s 1 t 2 and t 1 s 2 t 1 t 2 . Then, we define the following morphism of Z-modules ZMrΣ 2 s i 3 ÝÑ ZMrΣ 3 s urαs Þ ÝÑ rσpp uαqs where σpp uαq is a 3-cell of Σ t with the following shape, with v spαq and w tpαq: 5.3.3. Remark. The proof of Proposition 5.3.2 uses the fact that Σ 3 is a homotopy basis to produce, for every 2-cell α of Σ and every u in M, a 3-cell σpp uαq with the required shape. The hypothesis on Σ 3 could thus be modified to only require the existence of such a 3-cell in Σ t : however, it is proved in [START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF] that this implies that Σ 3 is a homotopy basis. With the leftmost normalisation strategy σ, we get, writing the 2-cell µ as a string diagram :

σpaq 1 a σpaaq σpaaaq µa 1 µ .

The presentation has exactly one critical branching, whose corresponding generating confluence can be written in the two equivalent ways .

The ZM-module ker d 2 is generated by

d 3 $ $ ¡ s $ $ ¡ $ ¡ $ a $ ¡ $ .
5.3.7. Resolutions from convergent presentations. In [START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF], the results presented here are generalised to produce a free resolution

p¤ ¤ ¤ q d n 1 / / ZMrΣ n s d n / / ZMrΣ n¡1 s d n¡1 / / p¤ ¤ ¤ q d 2 / / ZMrΣ 1 s d 1 / / ZMrΣ 0 s ε / / Z / / 0
of the trivial ZM-module Z from a convergent presentation of a monoid M. For k ¥ 4, the ZM-module ZMrΣ k s is defined as the free ZM-module over a family Σ k of k-cells obtained from the pk ¡ 1q-fold 6. Squier's example and variant critical branchings. For example, the 4-cell

7 9 % - I E 2 4 B >
is the only element of Σ 4 in the case of the monoid of Example 5.3.6. A related resolution is obtained in [START_REF] Kobayashi | Complete rewriting systems and homology of monoid algebras[END_REF] using antichains instead of k-fold critical branchings.

SQUIER'S EXAMPLE AND VARIANT

Squier's example

In [START_REF] Squier | Word problems and a homological finiteness condition for monoids[END_REF], Squier defines, for every k ¥ 1, the monoid S k presented by d a, b, t, x 1 , . . . , x k , y 1 , . . . , y k § § pα n q nN , pβ i q 1¤i¤k , pγ i q 1¤i¤k , pδ i q 1¤i¤k , pε i q 1¤i¤k h with

at n b α n ùñ 1, x i a β i ùñ atx i , x i t γ i ùñ tx i , x i b δ i ùñ bx i , x i y i ε i ùñ 1.
In [START_REF] Squier | A finiteness condition for rewriting systems[END_REF], Squier proves the following properties for S 1 . With similar arguments, the result extends to every monoid S k , for k ¥ 1. In what follows, we denote by γ n : xt n ñ t n x the 2-cell of Sq ¦ defined by induction on n as follows:

γ 0 1 x and γ n 1 γt n 1 tγ n . For every n, we write f n : xat b ñ at n 1 bx the 2-cell of Sq ¦ defined as the following composite:

xat n b
βt n b 7 9 atxt n b atγ n b 7 9 at n 1 xb at n 1 δ 7 9 at n 1 bx.

We note that f n contains no 2-cell α k .

6.2.1. Proposition. The monoid S 1 admits the finite presentation Sq xa, b, t, x, y | α 0 , β, γ, δ, εy.

Proof. For every natural number n, we consider the following 2-sphere of Sq t : (5) Thus, the 2-cell α n 1 is parallel to the composite 2-cell at n 1 bε ¡ 1 f ¡ n y 1 xα n y 1 ε.

Since f n contains no α k , this proves the result by induction on n.

6.2.2. Proposition. The 2-polygraph Sq is convergent and Squier completion of Sq contains a 3-cell A n with shape

at n 1 bx α n 1 x " * xat n b f n C ? xα n @ < A n Õ x
for every natural number n.

Proof. Let us prove that Sq terminates. For that, we build a termination order based on derivations, similar to the method of [GM09, Theorem 4.2.1] for 3-polygraphs. We associate, to every 1-cell u of Sq ¦ , two maps u ¦ : N Ñ N and fpuq : N Ñ N as follows. First, we define them on the 1-cells of Sq:

x ¦ pnq n 1, a ¦ pnq b ¦ pnq t ¦ pnq y ¦ pnq n, fpaqpnq 3 n , fpbqpnq fpyqpnq 2 n , fptqpnq fpxqpnq 0.

Then, we extend the mappings to every 1-cell of Sq ¦ thanks to the following relations:

1 ¦ pnq n, puvq ¦ pnq v ¦ pu ¦ pnqq, fp1qpnq 0, fpuvqpnq fpuqpnq fpvqpu ¦ pnqq. We compare parallel 1-cells of Sq ¦ by the order generated by u v if u ¦ ¤ v ¦ and fpuq fpvq. The defining relations of p¤q ¦ and f imply that the composition of 1-cells of Sq ¦ is strictly monotone in both arguments. The natural order on N implies that every decreasing family of parallel 1-cells of Sq ¦ is stationary. To get a termination order, hence the termination of Sq, there remains to check that u ¡ v for every 2-cell u ñ v of Sq. Indeed, we check that the following (in)equalities are satisfied: pat k bq ¦ pnq n 1 ¦ pnq, pxaq ¦ pnq n 1 patxq ¦ pnq, pxtq ¦ pnq n 1 ptxq ¦ pnq, pxbq ¦ pnq n 1 pbxq ¦ pnq, pxyq ¦ pnq n 1 ¡ n 1 ¦ pnq, and fpat k bqpnq 3 n 2 n ¡ 0 fp1qpnq, fpxaqpnq 3 n 1 ¡ 2 n 3 n fpatxqpnq, fpxtqpnq 2 n 1 ¡ 2 n fptxqpnq, fpxbqpnq 2 n 1 ¡ 2 n fpbxqpnq, fpxyqpnq 2 n 1 ¡ 0 fp1qpnq.

Let us prove that Sq is confluent and compute Squier completion of Sq. The 2-polygraph Sq has exactly one critical branching pβt n b, xα n q for every natural number n, and each of those critical branchings is confluent, yielding the 3-cell A n . We conclude thanks to Theorem 4.3.2.

6.2.3. Proposition. The monoid S 1 has a decidable word problem.

Proof. The convergent presentation Sq of S 1 is infinite, so that the normal-form procedure cannot be applied. However, the sources of the 2-cells α n are exactly the elements of the regular language at ¦ b.

This implies that the sources of the 2-cells of Sq form a regular language over the finite set ta, b, t, x, yu:

by [OKK98, Proposition 3.6], this implies that the word problem of S 1 is decidable.

In order to show that S 1 is not of finite derivation type, by Theorem 4.2.3, it is sufficient to check that the finite presentation Sq of S 1 given in Proposition 6.2.1 admits no finite homotopy basis. We denote by π : Sq t ÝÑ Sq t the projection that sends the 2-cells β, γ, δ and ε to themselves and whose value on α n is given by induction on n, thanks to (6), i.e.

πpα 0 q α and πpα n 1 q g ¡ n 1 xπpα n qy 1 ε where g n f n y 1 at n 1 bε.

By application of the homotopy basis transfer theorem 4.2.2 to Sq and Sq, with F the canonical inclusion of Sq t into Sq t , with G π and with τ mapping each 1-cell u of Sq t to 1 u , we obtain 6.2.4. Lemma. The monoid S 1 admits the coherent presentation xa, b, t, x, y | α 0 , β, γ, δ, ε | p r

A n q nN y where r A n is the 3-cell xπpα n q @ < r A n

Õ

x

Let us now deduce that S 1 is not of finite derivation type. A direct proof is given in [Squ87, Theorem 6.7], see also [START_REF] Lafont | A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier)[END_REF]§6]. However, we can use an argument coming from the dimension above, to explicit as 4-cells the relations between the 3-cells. We choose this proof to incite the reader to continue the exploration of the higher dimensions of rewriting, e.g. with [START_REF] Métayer | Resolutions by polygraphs[END_REF][START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF]. Precisely, we use the fact that the triple critical branchings (the minimum overlaps of three rewriting steps) of a reduced convergent 2-polygraph Σ induce a homotopy basis of Squier completion SpΣq: all the parallel 3-cells of SpΣq t are equal up to the 4-cells generated by the triple critical branchings [START_REF]Higher-dimensional normalisation strategies for acyclicity[END_REF]Proposition 4.4.4]. This implies 6.2.5. Proposition. Let Σ be a reduced convergent 2-polygraph with no triple critical branching. Then all the parallel 3-cells of the free p3, 1q-category SpΣq t are equal.

We can now conclude with 6.2.6. Proposition. The monoid S 1 is not of finite derivation type.

Proof. We note that the 3-cell A n y 1 ε of SpSqq t has the 2-sphere (5) as boundary: As a consequence, for every natural number n, the 3-cell g ¡ n 1 A n y 1 ε has source α n 1 and target g ¡ n 1 xα n y 1 ε. We define the 3-cell B n of SpSqq t by induction on n as B 0 1 α 0 and B n 1 g ¡ n 1 A n y 1 ε ¨2 B n so that B n has source α n and target πpα n q, by definition of π. As a consequence, the 3-cell r A n , when seen as a 3-cell of SpSqq t through the canonical inclusion, is parallel to the following composite 3-cell:

at n 1 bx πpα n 1 qx Õ α n 1 x ' / B ¡ n 1 x x xat n b f n C ? xα n 7 9 xπpα n q R H A n Õ xB n Õ x (7)
We observe that the convergent 3-polygraph is reduced and has no critical triple branching. Thus, as a consequence of Proposition 6.2.5, all the parallel 3-cells of SpSqq t are equal. This implies that r

A n is equal to the composite (7). Expanding the definition of B n 1 , we get:

r A n f n 1 B ¡ n x ¨2 f n 1 g ¡ n x 1 A ¡ n yx 1 εx ¨2 A n 2 xB n . (8)
Now, let us assume that Sq admits a finite homotopy basis. By Proposition 4.2.4, there exists a natural number n such that the 3-cells r A 0 , . . . , r A n form a homotopy basis of Sq t . In particular, the 3-cell r

A n 1 is parallel to a composite W of the 3-cells r A 0 , . . . , r

A n , hence it is equal to W in Sq t .

Thus, on the one hand, by application of (8) to each of r A 0 , . . . , r A n , and by definition of B 0 , . . . , B n , we get that r

A n 1 is a composite of the 3-cells A 0 , . . . , A n . But, on the other hand, the relation (8) tells us that r

A n 1 is equal to a composite r A n 1 C 2 ph 1 A ¡ n 1 yx 1 kq 2 A n 1 2 D (9

)
where the 3-cells C and D contain A 0 , . . . , A n only.

To prove that this leads to a contradiction, let us consider the free right ZS 1 -module ZS 1 rΓs over the homotopy basis Γ tA n , n Nu. We define a map r¤s : SpSqq t ÝÑ ZS 1 rΓs 6.3. A variant of Squier's example thanks to the relations ruAvs rAsv, rA 1 Bs rAs rBs, rA 2 Bs rAs rBs, for all 1-cells u and v and 3-cells A and B of SpSqq t such that the composites are defined. From (9), we deduce that r r A n 1 s rCs ¡ rA n 1 syx rA n 1 s rDs (10) holds in ZS 1 rΓs. Since the 3-cell r A n 1 is a composite of the 3-cells A 0 , . . . , A n , we have that r r A n 1 s is a linear combination of rA 0 s, . . . , rA n s. Since the right ZS 1 -module ZS 1 rΓs is free, it follows from (10) that yx 1 holds in S 1 . However, the 1-cells yx and 1 are distinct normal forms of the convergent presentation Sq of S 1 . This means that yx is distinct from 1 in S 1 and, thus, leads to a contradiction, so that we conclude that Sq t does not admit a finite homotopy basis.

Finally, by Theorem 4.3.3, we get: 6.2.7. Corollary. The monoid S 1 admits no finite convergent presentation. Moreover, the 2-polygraph | LP has no triple critical branching. In a similar way to the case of Squier's monoid S 1 , we get that the (finitely generated, with a decidable word problem) monoid M is not of finite derivation type: we prove that the 3-cells B n induce a projection π of | LP t onto LP t , so that the family pπpA n qq nN is an infinite homotopy basis of LP t . Then we prove that no finite subfamily of pπpA n qq nN can be a homotopy basis of LP t .

A variant of Squier's example

¡

  fq. A branching pf, gq is local if f and g are rewriting steps. Local branchings belong to one of the following three families: ¡ aspherical branchings, for a rewriting step u f ùñ vPeiffer branchings, for rewriting steps u f ùñ u I and v g ùñ v I : u I v uv fv @ < ug 4 6 uv I ¡ overlapping branchings are the remaining local branchings.

  a critical branching of Σ. Moreover, if the branching ph, kq is confluent, then so is pf, gq:

3. 2

 2 .1. Knuth-Bendix completion. Let Σ be a terminating 2-polygraph, equipped with a total termination order ¤. A Knuth-Bendix completion of Σ is a 2-polygraph Σ obtained by the following process. We start with Σ equal to Σ and with B equal to the set of critical branchings of Σ. If B is empty, then the procedure stops. Otherwise, it picks a branching in B and it performs the following operations: 1. It computes 2-cells f I : v ñ p v and g I : w ñ p w of Σ¦ , where p v and p w are normal forms for v and w, respectively, as in the following diagram: tests which (in)equality p v p w or p v ¡ p w or p v p w holds, corresponding to the following three situations, respectively: If p v $ p w, the procedure adds the dotted 2-cell α of the corresponding situation to Σ and all the new critical branchings created by α to B.3. It removes pf, gq from B and restarts from the beginning.

  the resulting 2-polygraph contains parallel generating 2-cells, the procedure removes all but one: , the procedure removes every generating 2-cell α with source vspβqv I , where β is another generating 2By construction, we get the following result, originally obtained by Métivier for term rewriting and by Squier for string rewriting: 3.2.4. Theorem ([Mét83], [Squ87, Theorem 2.4]). Every (finite) convergent 2-polygraph is Tietzeequivalent to a (finite) reduced convergent 2-polygraph.

  1. Normalisation strategies. Let Σ be a 2-polygraph and let C denote the category presented by Σ. We consider a section C Σ ¦ 1 of the canonical projection π : Σ ¦ 1 C, i.e. we choose, for every 3. Rewriting properties of 2-polygraphs 1-cell u of C, a 1-cell p

  pf, gq of Σ.4. FINITE DERIVATION TYPE4.1. Coherent presentations of categories 4.1.1. Cellular extensions and homotopy bases of 2-categories. Let C be a 2-category. A 2-sphere of C is a pair γ pf, gq of parallel 2-cells of C, i.e. with spfq spgq and tpfq tpgq. We call f the source of γ and g its target and we denote such a 2-sphere by γ : f g. A cellular extension of the 2-category C is a set Γ equipped with a map from Γ to the set of 2-spheres of C.

¡Fpvq

  the cellular extension FpΓ q contains one 3for every 3-cell γ : f g of Γ ,¡ the cellular extension τ Ξ contains one 3

  4.3.1. Squier completion. For Σ a 2-polygraph, a family of generating confluences of Σ is a cellular extension of Σ t that contains exactly one 3

ÕÕÕ

  where α and β are 2-cells of Σ and where p u, p w and p v are non-identity normal forms. Let us note that αp v is the leftmost reduction step of p u p wp v and that p uβ is its rightmost reduction step. In particular, we have σpp u p wp vq αp v 1 σpu I p vq.We define Σ 3 as the cellular extension of Σ t made of one 3-cell with the following shape, for every critical branching b pαp v, p uβq of Σ: 5. Example. The standard presentation of a category C is the 2-polygraph Std 2 pCq defined as follows. The 0-cells and 1-cells of Std 2 pCq are the ones of C, with p u denoting a 1-cell u of C when seen as a 1-cell of Std 2 pCq. The 2-polygraph Std 2 pCq contains a 2for all 1-cells u : x Ñ y and v : y Ñ z of C, and a 2for every 0-cell x of C. The standard coherent presentation of C is the p3, 1q-polygraph denoted by Std 3 pCq and obtained by extension of Std 2 pCq with the homotopy basis made of the following 3cells:

¡u.yyyyy

  for every 1-cell u : x Ñ y of C, two critical branchings pγ 1x,u , ι ¡x p uq and pγ u,1y , Since considering the 2-cells ι x or ι ¡ x as generators does not change the generated p2, 1q-category, we get that those three families of 3-cells form a homotopy basis of Std 2 pCq. We replace λ I u by λ u ι x p u 1 λ u and ρ I u by ρ u p uι y 1 ρ u to get the result. 4.3.6. Example. Let us consider the monoid M presented by the 2We prove that Σ terminates with the deglex order generated by x y. The 2-polygraph Σ has one, non confluent critical branching pαyx, xyαq. Knuth-Bendix completion Σ of Σ is obtained by adjunction of the following 2-cell β : yyyx ñ xyyy: completion Sp Σq extends Σ with the following two 3-cells:In fact, the 3-cell A is sufficient to get a homotopy basis of Σ, as witnessed by the following 3-sphere of the p3, 1q-category Sp Σq t :

  5.2.4. Examples. Let us consider the monoid M presented by the 2-polygraph Σ d a, c, t § § at n 1 α n ùñ ct n , n N h .

Õ

  Let us note that such a 3-cell necessarily exists in Σ t because Σ 3 is a homotopy basis of Σ t . Then we have, on the one hand, i 2 d 2 purαsq i 2 purvs ¡ urwsq rσpp uvqs ¡ rσpp uwqs and, on the other hand, d 3 i 3 purαsq rp uα 1 σpp uwqs ¡ rσpp uvqs, urαs rσpp uwqs ¡ rσpp uvqs.Hence d 3 i 3 i 2 d 2 Id ZMrΣ 2 s , concluding the proof.

Õ

  5.3.8. Other homological finiteness conditions. In the definition 5.1.3 of homological type left-FP n for a monoid M, the replacement of left modules by right modules, bimodules or natural systems gives the definitions of the homological types right-FP n , bi-FP n and FP n , for every 0 ¤ n ¤ V. We refer the reader to [GM12b, Section 5.2] for the relations between these different finiteness conditions. In particular, for n 3, all of these homotopical conditions are consequences of the finite derivation type property. The proof is similar to the one for the left-FP 3 property in Section 5.3: for example, in the case of the right-FP 3 property, we consider right modules and, to get the contracting homotopy, we construct a right normalisation strategy σ by defining a 3-cell σpαp uq with shape for any generating 2-cell α : v ñ w and u in the monoid.

..d I ac n b β I c n b D @ d I α n 1 3 ac n 1 d

 1 Let us consider the monoid M presented by the following 2-polygraph from [LP91, Laf95]: LP d a, b, c, d, d I § § ab α 0 ùñ a, da β ùñ ac, d I a γ ùñ ac h The monoid M has similar properties to Squier's example: it admits a finite presentation, it has a decidable word problem, yet it is not of finite derivation type and, as a consequence, it does not admit a finite convergent presentation. To prove these facts, the 2-polygraph LP is completed, by Knuth-Bendix procedure, into the infinite convergent 2-polygraph | LP d a, b, c, d, d I § § pac n b α n ùñ ac n q nN , da β ùñ ac, d I a β I ùñ ac h Squier completion of | LP has two infinite families of 3-cells: I ac n β I c n S I

  The equality at n 1 ct n holds in M by definition, yielding d 2 rα n 1 s d 2 rα n s. As a consequence, the ZM-module ker d 2 is generated by the elements rα n s ¡ rα 0 s. Since the ZM-module ker d 1 is equal to im d 2 , hence isomorphic to ZMrΣ 2 s{ ker d 2 , it follows that ker d 1 is generated by rα 0 s only, so that, by Lemma 5.1.4, the monoid M is of homological type left-FP 2 . This can also be obtained by simply observing that M admits the finite presentation xa, c, t | α 0 y.

	Now, let us consider the monoid M presented by the 2-polygraph
	Σ	d	a, b, t	§ § at n b	α n ùñ 1 , n N

h

.

  Let M be a finitely presented monoid. If M is of finite derivation type, then it is of homological type left-FP 3 .

	From Proposition 5.3.2, we deduce
	5.3.4. Theorem ([CO94, Theorem 3.2], [Laf95, Theorem 3], [Pri95]). By Theorem 4.3.3, this implies
	5.3.5. Theorem ([Squ87, Theorem 4.1]). If a monoid admits a finite convergent presentation, then it is
	of homological type left-FP 3 .
	5.3.6. Example. Let us consider the monoid M with the convergent presentation
	xa | aa µ ùñ ay.

  6.1.1. Theorem ([SOK94, Theorem 6.7, Corollary 6.8]). For every k ¥ 1, the monoid S k satisfies the For k ¥ 2, the monoid S k is not of finite homological type left-FP 3 and, as a consequence, it does not admit a finite convergent presentation. Proposition 6.1.2 does not hold for S 1 . Indeed, this monoid is of homological type left-FP V ,[Squ87, Example 4.5]. This proves that, if finite derivation type implies left-FP 3 , the reverse implication does not hold for general monoids. However, in the special case of groups, the property of having finite derivation type is equivalent to the homological finiteness condition left-FP 3[START_REF]For groups the property of having finite derivation type is equivalent to the homological finiteness condition FP 3[END_REF]. The latter result is based on the Brown-Huebschmann isomorphism between homotopical and homological syzygies[START_REF] Brown | Identities among relations, Low-dimensional topology[END_REF].Let us prove the result in the case of the monoid S 1 , with the following infinite presentation:

	following properties:
	i) it is finitely presented,
	ii) it has a decidable word problem,
	iii) it is not of finite derivation type,
	iv) it admits no finite convergent presentation.
	In [Squ87], Squier had already proved
	6.1.2. Proposition ([Squ87, Example 4.5.]). Sq xa, b, t, x, y | pα n q nN , β, γ, δ, εy
	with	at n b	α n ùñ 1, xa β ùñ atx, xt γ ùñ tx, xb δ ùñ bx, xy ε ùñ 1.

6.2. Proof of Theorem 6.1.1

Monoids (resp. groups) correspond exactly to categories (resp. groupoids) with only one 0-cell.

for every element u of M, with p 1 x 1 x for every 0-cell x of Σ, and we fix a normalisation strategy σ for Σ. Then we define the morphisms of Z-modules i 0 , i 1 and i

by their values on generic elements i 0 p1q 1, i 1 puq rp us, i 2 purxsq rσpp uxqs, where the bracket r¤s is extended to every 2-cell of Σ t thanks to the relations r1 u s 0, rufvs urfs and rf 1 gs rfs rgs, for all 1-cells u and v and 2-cells f and g of Σ t such that the composites ufv and f 1 g are defined.First, we have εi 0 Id Z . Next, for every u in M, we have i 0 εpuq 1 and d 1 i 1 puq d 1 rp us u ¡ 1. Thus d 1 i 1 i 0 ε Id ZM . Finally, we have, on the one hand, i 1 d 1 purxsq i 1 pux ¡ uq rx uxs ¡ rp us and, on the other hand, d 2 i 2 purxsq d 2 rσpp uxqs rp uxs ¡ rx uxs urxs rp us ¡ rx uxs. For this equality, we check that d 2 rfs rspfqs ¡ rtpfqs holds for every 2-cell f of Σ t by induction on the size of f. Hence we have d 2 i 2 i 1 d 1 Id ZMrΣ 1 s , thus concluding the proof.

in SpΣq t , as in the following diagram:

Moreover, the p3, 1q-category SpΣq t contains a 3-cell σ f ¡ from f ¡ to σ v 1 σ ¡ u , given as the following composite:

Now, let us consider a general 2-cell f : u ñ v of Σ t . By construction of Σ t , the 2-cell f can be decomposed (in general in a non-unique way) into a zigzag

where each f i and g i is a 2-cell of Σ ¦ . We define σ f as the following composite 3-cell of SpΣq t , with source f and target σ u 1 σ ¡ v :

We proceed similarly for any other 2-cell g : u ñ v of Σ t , to get a 3-cell σ g from g to σ u 1 σ ¡ v in SpΣq t .

Thus, the composite σ f 2 σ ¡ g is a 3-cell of SpΣq t from f to g, concluding the proof.

Theorem 4.3.2 is extended to higher-dimensional polygraphs in [GM09, Proposition 4.3.4]. In the special case of presentations of monoids, we recover the original result of Squier.