Coherent confluence modulo relations and double groupoids (Q2136121): Difference between revisions

The authors of the paper under review consider strict globular \(n\)-categories. A \textit{coherent presentation} of an \(n\)-category is a description by generators, relations, and relations between the relations [\textit{S. Gaussent} et al., Compos. Math. 151, No. 5, 957--998 (2015; Zbl 1398.20069)]. Solvers of specific problems for \(n\)-categories would like to be able to compute all pairs of relations that are equal for a given presentation, making only some of them explicit and able to generate all other pairs of equal relations. Confluent and terminating rewriting systems generate coherent presentations, whose relations among relations are defined by confluence diagrams of critical branchings. The paper introduces a procedure to compute coherent presentations when the rewrite relations are defined modulo a set of axioms. The authors' results on coherence are formulated using the structure of \(n\)-categories enriched in double groupoids, whose horizontal cells represent path rewriting, the vertical cells represent congruence generated by axioms, and the square cells represent coherence cells induced by diagrams of confluence modulo. The authors illustrate their constructions on rewriting systems modulo commutation relations in commutative monoids, isotopy relations in pivotal monoidal categories, and inverse relations in groups. From the text: ``In Section 2, we introduce notations and terminology on higher-dimen\-si\-o\-nal globular \(n\)-categories and globular \(n\)-polygraphs. We refer the reader to [\textit{Y. Guiraud} and \textit{P. Malbos}, Theory Appl. Categ. 22, 420--478 (2009; Zbl 1190.18002)] for a deeper presentation on rewriting properties of \(n\)-polygraphs. We also recall from [\textit{C. Ehresmann}, Ann. Sci. Éc. Norm. Supér., III. Sér. 80, 349--426 (1963; Zbl 0128.02002)] the notions of double categories and of double groupoids. In Section 3 we define the notions of double polygraphs and dipolygraphs, giving double coherent presentations of globular \(n\)-categories. Following [\textit{R. Dawson} and \textit{R. Paré}, J. Pure Appl. Algebra 168, No. 1, 19--34 (2002; Zbl 1008.18007)], we construct the free \(n\)-category enriched in double groupoids generated by a double \((n+2)\)-polygraph, in which our coherence results will be formulated. Finally, we explain how to deduce a globular coherent presentation from a double coherent presentation. As examples, we make explicit the notion of coherent presentation in the cases of groups, commutative monoids and pivotal categories. Section 4 is devoted to the study of rewriting properties of polygraphs defined modulo relations. We formulate the notions of termination, confluence, local confluence and confluence modulo for these polygraphs. Following [\textit{L. Bachmair} and \textit{N. Dershowitz}, Theor. Comput. Sci. 67, No. 2--3, 173--201 (1989; Zbl 0686.68021)], we give a completion procedure in terms of critical branchings for confluence modulo of the polygraph modulo \((\mathtt{R},\mathtt{E},_{\mathtt{E}}\mathtt{R})\). In Section 5, we develop the notion of coherent confluence modulo and we prove a coherent version of Newman's lemma and critical branching lemma for polygraphs modulo. In Section 6, we define the notion of coherent completion modulo, and we show how to compute a double coherent presentation of an \(n\)-category by coherent completion. Section 7 shows how to deduce a globular coherent presentation for an \(n\)-category from a double coherent presentation generated by a polygraph modulo. Finally, we apply our constructions in the situation of commutative monoids, pivotal monoidal categories modulo isotopy relations, and groups modulo inverse relations.''