Free precategories as presheaf categories

Simon Forest and Samuel Mimram

arXiv: 2211.16099v1 · PDF · 29 November 2022
Categories: math.CT
Licence: CC BY 4.0 The site shows the text.

Abstract

Precategories generalize both the notions of strict n-category and sesquicategory: their definition is essentially the same as the one of strict n-categories, excepting that we do not require the various interchange laws to hold. Those have been proposed as a framework in which one can express semi-strict definitions of weak higher categories: in dimension 3, Gray categories are an instance of them and have been shown to be equivalent to tricategories, and definitions of semi-strict tetracategories have been proposed, and used as the basis of proof assistants such as Globular. In this article, we are mostly interested in free precategories. Those can be presented by generators and relations, using an appropriate variation on the notion of polygraph (aka computad), and earlier works have shown that the theory of rewriting can be generalized to this setting, enjoying most of the fundamental constructions and properties which can be found in the traditional theory, contrarily to polygraphs for strict categories. We further study here why this is the case, by providing several results which show that precategories and their associated polygraphs bear properties which ensure that we have a good syntax for those. In particular, we show that the category of polygraphs for precategories form a presheaf category.

Items 45

Example

Example 1

GZ16

Given a 2-precategory C with two 2-cells \phi and \psi as in

\begin{tikzcd} x \ar[r,bend left=60,"f",""{auto=false,name=topl}] \ar[r,bend right=60,"{f'}"'{pos=0.52},""{auto=false,name=botl}] & y \ar[r,bend left=60,"g",""{auto=false,name=topr}] \ar[r,bend right=60,"{g'}"',""{auto=false,name=botr}] & z \ar[from=topl,to=botl,phantom,"\Downarrow\phi"] \ar[from=topr,to=botr,phantom,"\Downarrow\psi"] \end{tikzcd}

there are two ways to compose \phi and \psi together, given by

(\phi \mathbin{\ast}_0 g) \mathbin{\ast}_1 (f' \mathbin{\ast}_0 \psi) \quad\text{and}\quad (f \mathbin{\ast}_0 \psi) \mathbin{\ast}_1 (\phi \mathbin{\ast}_0 g')

that can be represented using string diagrams by

\expandafter\lets satexfigure0\endcsname\undefined \def0.9{0.9}\setkeys{satex}{} \IfFileExists{satex/wires-left-right.satix}{\input{satex/wires-left-right.satix}}{\@latex@error{No file wires-left-right.satix}.} \vcenter{ \hbox{\scalebox{0.9}{ s satexfigure0\endcsname }}} \quad\qquad\text{and}\qquad\quad \expandafter\lets satexfigure0\endcsname\undefined \def0.9{0.9}\setkeys{satex}{} \IfFileExists{satex/wires-right-left.satix}{\input{satex/wires-right-left.satix}}{\@latex@error{No file wires-right-left.satix}.} \vcenter{ \hbox{\scalebox{0.9}{ s satexfigure0\endcsname }}}

and these two composites are not expected to be equal in C. Moreover, by our definition of precategories, there is no such thing as a valid cell \phi \mathbin{\ast}_0 \psi, and the string diagram

\expandafter\lets satexfigure0\endcsname\undefined \def0.9{0.9}\setkeys{satex}{} \IfFileExists{satex/wires-mid-mid.satix}{\input{satex/wires-mid-mid.satix}}{\@latex@error{No file wires-mid-mid.satix}.} \vcenter{ \hbox{\scalebox{0.9}{ s satexfigure0\endcsname }}}

makes no sense in this setting.

Proposition

Proposition 2

U8DG

The category \mathbf{PCat}_{n} is locally finitely presentable, complete and cocomplete. Moreover, the functor \mathcal U_n is a right adjoint which preserves directed colimits.

Proposition

Proposition 3

CLVK

For every n \in \mathbb{N}\cup\{\omega\}, the functor \mathcal U_n is monadic.

Proposition

Proposition 4

9V6O

Given n \in \mathbb{N} \cup \{\omega\}, \mathbf{Pol}_{n} is a locally finitely presentable category. In particular, it is complete and cocomplete.

Theorem

Theorem 5

WB2Y

Given m \in \mathbb{N} and a polygraph \mathsf{P}\in\mathbf{Pol}_{\omega}, every m-cellof \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } can be written uniquely as

E_1[g_1] \mathbin{\ast}_{m-1} \cdots \mathbin{\ast}_{m-1} E_k[g_k]

for some unique g_1,\cdots,g_k \in \mathsf{P}_m and (m{-}1) E_1,\ldots,E_k of the corresponding types.

Used by Remark 6

Remark

Remark 6

SZD2

A consequence of the above theorem is that the embeddings \operatorname{e}_{i} \colon \mathsf{P}_i \rightarrow \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_i introduced earlier are injective. Thus, given g \in \mathsf{P}_i, we will often omit \operatorname{e}_{i} and write g for both the element of \mathsf{P}_i and the cell of \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_i.

Uses Theorem 5

Proposition

Proposition 7

RWPK

Let F\colon \mathsf{P} \rightarrow \mathsf{Q} \in \mathbf{Pol}_{\omega} be a morphism of polygraphs, k \in \mathbb{N}_{\le n} and u \in \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_k. The following hold:

when k > 0, there exists a cell u' \in \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_{k-1} such that u = \def#2{u'} \ifx#2\@empty \mathrm{id}^{k} \else \mathrm{id}^{k}_{u'} \fi if and only if there exists a cell \tilde u' \in \def-{-} \def#1{\mathsf{Q}} \def#2{(-)} \def#3{\mathsf{Q}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_{k-1} such that \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }(u) = \def#2{\tilde u'} \ifx#2\@empty \mathrm{id}^{k} \else \mathrm{id}^{k}_{\tilde u'} \fi,
there exists a generator g \in \mathsf{P}_k such that u = g if and only if there exists a generator \tilde g \in \mathsf{Q}_k such that \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }(u) = \tilde g.

Proposition

Proposition 8

L0VR

Given \mathsf{P} \in \mathbf{Pol}_{\omega} and u,v_1,v_2 \in \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } such that u \mathbin{\ast}_i v_1 = u \mathbin{\ast}_i v_2 for some i, then v_1 = v_2.

Remark

Remark 9

Q9I1

Note that such a property does not hold for polygraphs of strict categories. Indeed, considering the 2of strict precategories \mathsf{P} defined by

\begin{aligned} \mathsf{P}_0 &= \{x\} & \mathsf{P}_1 &= \{f \colon x \rightarrow x\} & \mathsf{P}_2 &= \{\alpha \colon \def#2{x} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{x} \fi \Rightarrow f\} , \end{aligned}

we have \alpha \mathbin{\ast}_0 \def#2{f} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{f} \fi \neq \def#2{f} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{f} \fi \mathbin{\ast}_0 \alpha while

\alpha \mathbin{\ast}_1(\alpha \mathbin{\ast}_0 \def#2{f} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{f} \fi ) = \alpha \mathbin{\ast}_0 \alpha = \alpha \mathbin{\ast}_1 ( \def#2{f} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{f} \fi \mathbin{\ast}_0 \alpha)

in the free strict 2-category\def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }. Graphically,

\begin{tikzcd} x \ar[rr,bend left=50,equals] \ar[rr,bend left=25,phantom,"\alpha\!\Downarrow"] \ar[r,bend left,equals]\ar[r,bend right,"f"']\ar[r,phantom,"\alpha\!\Downarrow"] &x\ar[r,"f"']&x \end{tikzcd} = \begin{tikzcd} x \ar[r,bend left,equals] \ar[r,phantom,"\alpha\!\Downarrow"] \ar[r,bend right,"f"'] & x \ar[r,bend left,equals] \ar[r,phantom,"\alpha\!\Downarrow"] \ar[r,bend right,"f"'] & x \end{tikzcd} = \begin{tikzcd} x \ar[rr,bend left=50,equals] \ar[rr,bend left=25,phantom,"\alpha\!\Downarrow"] \ar[r,"f"'] & x \ar[r,bend left,equals]\ar[r,bend right,"f"']\ar[r,phantom,"\alpha\!\Downarrow"] & x \end{tikzcd}

Proposition

Proposition 10

ASOE

Given n \in \mathbb{N} \cup \{\omega\} and an nprefunctor F\colon C \rightarrow D \in \mathbf{PCat}_{n}, if

F(u) = \def#2{v} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{v} \fi

for some k \in \mathbb{N}_{< n}, {u \in C_{k+1}}, and {v \in D_k}, then there exists a unique u' \in C_k such that

F(u') = v \qquad\text{and}\qquad u = \def#2{u'} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{u'} \fi \makebox[0pt][l]{.}

Proposition

Proposition 11

XQYH

Given m \in \mathbb{N} \cup \{\omega\} and a morphism F \colon \mathsf{P} \rightarrow \mathsf{Q} \in\mathbf{Pol}_{m}, the prefunctor \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }\colon \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }\rightarrow \def-{-} \def#1{\mathsf{Q}} \def#2{(-)} \def#3{\mathsf{Q}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } is Conduché.

Remark

Remark 12

JVSV

As a counter-example for the above property in the context of strict categories, consider the polygraphs \mathsf{P} and \mathsf{Q} defined by

\begin{aligned} \mathsf{P}_0 &= \{x\} & \mathsf{P}_1 &= \emptyset & \mathsf{P}_2 &= \{\alpha \colon \def#2{x} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{x} \fi \Rightarrow \def#2{x} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{x} \fi , \beta\colon \def#2{x} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{x} \fi \Rightarrow \def#2{x} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{x} \fi \} \\ \mathsf{Q}_0 &= \{y\} & \mathsf{Q}_1 &= \emptyset & \mathsf{Q}_2 &= \{\gamma \colon \def#2{y} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{y} \fi \Rightarrow \def#2{y} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{y} \fi \} \makebox[0pt][l]{.} \end{aligned}

We then have a morphism F \colon \mathsf{P} \rightarrow \mathsf{Q} sending \alpha and \beta to \gamma, and the associated prefunctor \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } sends both \alpha \mathbin{\ast}_0 \beta and \beta \mathbin{\ast}_0 \alpha to \gamma \mathbin{\ast}_0 \gamma.

Proposition

Proposition 13

LQL3

Given n \in \mathbb{N} \cup \{\omega\} and F \colon C \rightarrow D \in \mathbf{PCat}_{n}, the following are equivalent:

F is a monomorphism,
F_k is a monomorphism for every k\le n.

Proposition

Proposition 14

V5ZD

Given n \in \mathbb{N} \cup \{\omega\} and F \colon \mathsf{P} \rightarrow \mathsf{Q} \in \mathbf{Pol}_{n}, the following are equivalent:

F is a monomorphism,
F_k is a monomorphism for every k\le n,
\def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } is a monorphism in \mathbf{PCat}_{n}.

Example

Example 15

0ERU

Let C be a small category. \hat C has a canonical structure of concrete category, where \ifthenelse{\equal{-}{-}}{|{-}|}{|-|} \def#1{\hat C} \ifx#1\empty \else ^{\hat C} \fi is defined on preasheaves P \in \hat C by

\ifthenelse{\equal{P}{-}}{|{-}|}{|P|} \def#1{\hat C} \ifx#1\empty \else ^{\hat C} \fi = \bigsqcup_{c \in C_0} P(c)

and extended naturally to morphisms between presheaves.

Used by Example 18

Example

Example 16

ZAC3

The functor \def-{-} \def#1{-} \def#2{|{-}|} \def#3{|-|} \ifx-#1 #2 \else #3 \fi \colon \mathbf{Pol}_{\omega} \rightarrow \mathbf{Set} which maps \mathsf{P} \in \mathbf{Pol}_{\omega} to

\def-{-} \def#1{\mathsf{P}} \def#2{|{-}|} \def#3{|\mathsf{P}|} \ifx-#1 #2 \else #3 \fi = \bigsqcup_{k \in \mathbb{N}} \mathsf{P}_k

equips \mathbf{Pol}_{\omega} with a structure of concrete category.

Example

Example 17

DCMB

There is a functor \def-{-} \def#1{-} \def#2{|{-}|} \def#3{|-|} \ifx-#1 #2 \else #3 \fi \colon \mathbf{Cat}_{\omega} \rightarrow \mathbf{Set} which maps C\in\mathbf{Cat}_{\omega} to

\def-{-} \def#1{C} \def#2{|{-}|} \def#3{|C|} \ifx-#1 #2 \else #3 \fi =\bigsqcup_{k \in \mathbb{N}}C_k

By precomposition with the functor (-)^*:\mathbf{Pol}_{\omega}\rightarrow\mathbf{Cat}_{\omega}, we obtain a functor \def-{-} \def#1{ \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }} \def#2{|{-}|} \def#3{| \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }|} \ifx-#1 #2 \else #3 \fi \colon \mathbf{Pol}_{\omega} \rightarrow \mathbf{Set} which maps \mathsf{P} \in \mathbf{Pol}_{\omega} to

\def-{-} \def#1{ \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }} \def#2{|{-}|} \def#3{| \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }|} \ifx-#1 #2 \else #3 \fi = \bigsqcup_{k \in \mathbb{N}} \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_k

and also equips \mathbf{Pol}_{\omega} with a structure of concrete category.

Example

Example 18

XDX4

Let C be a small category and consider the canonical concrete category structure on \hat C given by Example 15. Given P\in\hat C and c\in C, we write \iota_c:P(c)\rightarrow\bigsqcup_{c\in C}P(c) for the canonical injection. The category \operatorname{Elt}(\hat C) has

as objects the pairs (P,\iota_c(x)) where P \in \hat C and x \in P(c), and
as morphisms from (P,\iota_c(x)) to (Q,\iota_d(y)) the natural transformations \alpha\colon P \Rightarrow Q such that c = d and \alpha_c(x) = y.

Given (P,\iota_c(x)) \in \operatorname{Elt}(\hat C), we have the following.

(P,\iota_c(x)) is principal when P is the smallest subpresheaf P' of P such that x \in P'(c). In particular, for all c \in C, (C(-,c),\iota_c( \def#2{c} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{c} \fi ))\in \operatorname{Elt}(\hat C) is principal.
(P,\iota_c(x)) is primitive when the natural transformation \theta\colon C(-,c) \rightarrow P which maps \def#2{c} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{c} \fi to x is an isomorphism.

Uses Example 15

Theorem

Theorem 19

S3NE

Let (\mathcal C, \ifthenelse{\equal{-}{-}}{|{-}|}{|-|} \def#1{\mathcal C} \ifx#1\empty \else ^{\mathcal C} \fi ) be a concrete category. \mathcal C is concretely equivalent to a presheaf category if and only if the following conditions are all satisfied:

\ifthenelse{\equal{-}{-}}{|{-}|}{|-|} \def#1{\mathcal C} \ifx#1\empty \else ^{\mathcal C} \fi reflects isomorphisms,
\mathcal C is cocomplete and \ifthenelse{\equal{-}{-}}{|{-}|}{|-|} \def#1{\mathcal C} \ifx#1\empty \else ^{\mathcal C} \fi preserves all small colimits,
the collection of isomorphism classes of primitive elements of \operatorname{Elt}(\mathcal C) is small,
for every element (X,x) \in \operatorname{Elt}(C), there is a morphism (U,u) \rightarrow (X,x) for some primitive element (U,u),
given two morphisms f,g\colon (U,u) \rightarrow (X,x) \in \operatorname{Elt}(\mathcal C) where (U,u) is primitive, we have f = g,
given two morphisms f\colon (U,u) \rightarrow (X,x) and g\colon (V,v) \rightarrow (X,x) of \operatorname{Elt}(\mathcal C) where both (U,u) and (V,v) are primitive, there is an isomorphism \theta\colon (U,u) \rightarrow (V,v) such that g \circ \theta = f.

Lemma

Lemma 20

0UE4

The function \def#1{} \ifx#1\empty \operatorname{supp} \else \operatorname{supp}^{} \fi is well-defined.

Lemma

Lemma 21

BIN5

Let n \in \mathbb{N} \cup \{\omega\} and F \colon \mathsf{P} \rightarrow \mathsf{Q} \in \mathbf{Pol}_{n}. Then, we have that \def#1{\mathsf{Q}} \ifx#1\empty \operatorname{supp} \else \operatorname{supp}^{\mathsf{Q}} \fi \circ \def-{-} \def#1{ \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }} \def#2{|{-}|} \def#3{| \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }|} \ifx-#1 #2 \else #3 \fi = \def-{-} \def#1{F} \def#2{|{-}|} \def#3{|F|} \ifx-#1 #2 \else #3 \fi \circ \def#1{\mathsf{P}} \ifx#1\empty \operatorname{supp} \else \operatorname{supp}^{\mathsf{P}} \fi.

Proposition

Proposition 22

V32S

Given n \in \mathbb{N} \cup \{\omega\}, an n \mathsf{P} and u \in \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }, there exist a finite n \tilde{P}, a monomorphism F\colon \tilde{P} \rightarrow \mathsf{P} and \tilde u \in \def-{-} \def#1{{\tilde{P}}} \def#2{(-)} \def#3{{\tilde{P}}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } such that \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }(\tilde u) = u and \def#1{} \ifx#1\empty \operatorname{supp} \else \operatorname{supp}^{} \fi (\tilde u) = \def-{-} \def#1{\tilde\mathsf{P}} \def#2{|{-}|} \def#3{|\tilde\mathsf{P}|} \ifx-#1 #2 \else #3 \fi.

Lemma

Lemma 23

PN18

Given a pair of parallel morphisms

\begin{tikzcd} \mathsf{P} \ar[r,shift left,"F"] \ar[r,shift right,"G"'] & \mathsf{Q} \end{tikzcd}

of \mathbf{Pol}_{\omega} such that \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }(u) = \def-{-} \def#1{G} \def#2{(-)} \def#3{G} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }(u) for some u \in \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }, we have F/u = G/u.

Lemma

Lemma 24

DYTR

An element (\mathsf{P},u) of \operatorname{Elt}(\mathbf{Pol}_{\omega}) (resp. \operatorname{Elt}(\mathbf{Pol}_{\omega}^*)) is principal if and only if \def#1{} \ifx#1\empty \operatorname{supp} \else \operatorname{supp}^{} \fi (u) = \def-{-} \def#1{\mathsf{P}} \def#2{|{-}|} \def#3{|\mathsf{P}|} \ifx-#1 #2 \else #3 \fi.

Lemma

Lemma 25

BQNP

Given a pair of parallel morphisms

\begin{tikzcd} (\mathsf{P},u) \ar[r,shift left,"F"] \ar[r,shift right,"G"'] & (\mathsf{Q},v) \end{tikzcd}

of \operatorname{Elt}(\mathbf{Pol}_{\omega}^*) where (\mathsf{P},u) is principal, then F = G.

Used by Remark 31, Remark 32

Lemma

Lemma 26

1LPK

Given an element (\mathsf{P},u) \in \operatorname{Elt}(\mathbf{Pol}_{\omega}^*), (\mathsf{P},u) is a polyplex if and only if (\mathsf{P}, \def#2{u} \ifx#2\@empty \mathrm{id}^{} \else \mathrm{id}^{}_{u} \fi ) is a polyplex.

Lemma

Lemma 27

09WW

Let (U,u) \in \operatorname{Elt}(\mathbf{Pol}_{\omega}^*). Then, the following are equivalent:

(U,u) is a polyplex and there exist \alpha \in U such that u = \alpha,
there exist polyplex liftings
G^\epsilon \colon (U^\epsilon,u^\epsilon) \rightarrow (U,\partial^{\epsilon}(u))
for \epsilon \in \{-,+\}, principal elements (S,s) and (T,t), and morphisms
\begin{aligned} F^{\epsilon-} \colon (S,s)&\rightarrow (U^\epsilon,\partial^-(u^\epsilon)) & F^{\epsilon+} \colon (T,t)&\rightarrow (U^\epsilon,\partial^+(u^\epsilon)) \end{aligned}
for \epsilon \in \{-,+\}, such that, considering the pushout
\begin{tikzcd}[column sep=20mm] S \sqcup T \ar[r,"{[F^{+-},F^{++}]}"] \ar[d,"{[F^{--},F^{-+}]}"'] & U^+ \ar[d,"\bar G^+",dotted] \\ U^- \ar[r,"\bar G^-"',dotted] & \partial U \end{tikzcd}
(U,u) is isomorphic to (\bar U,\bar \alpha), where \bar U is obtained from \partial U by adding a generator
\bar \alpha : \bar G^-(u^-) \rightarrow \bar G^+(u^+) \makebox[0pt][l]{.}

Lemma

Lemma 28

KRB6

Let (U,u) \in \operatorname{Elt}(\mathbf{Pol}_{\omega}^*), u_1 \in \def-{-} \def#1{U} \def#2{(-)} \def#3{U} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_k, u_2 \in \def-{-} \def#1{U} \def#2{(-)} \def#3{U} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_l for some k,l \in \mathbb{N}, with u_1 and u_2 are i-composablefor i = \min(k,l). Then, the following are equivalent:

(U,u) is a polyplex and u = u_1 \mathbin{\ast}_i u_2,
there exist a principal element (U',u') and polyplexes (U_1,u_1) and (U_2,u_2), and morphisms F_j \colon U'\rightarrow U_j \in \mathbf{Pol}_{\omega} and G_j \colon U_j \rightarrow U for j \in \{1,2\}, such that
\begin{tikzcd} U' \ar[d,"F_1"'] \ar[r,"F_2"] & U_2 \ar[d,"G_2"] \\ U_1 \ar[r,"G_1"'] & U \end{tikzcd}
is a pushout diagram in \mathbf{Pol}_{\omega}, \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_1(u') = \partial^+_i(u_1), \def-{-} \def#1{F} \def#2{(-)} \def#3{F} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_2(u') = \partial^-_i(u_2) and u = G_1(u_1) \mathbin{\ast}_i G_2(u_2).

Used by Remark 44

Proposition

Proposition 29

DLOE

Given an element (\mathsf{P},u)\in\operatorname{Elt}(\mathbf{Pol}_{\omega}^*), there exists a polyplex lifting

F \colon (U,\bar u) \rightarrow (\mathsf{P},u)

where (U,\bar u) is primitive.

Proposition

Proposition 30

SGBM

Given two morphisms L^1\colon (U^1,u_1) \rightarrow (\mathsf{P},u) and L^2\colon (U^2,u_2) \rightarrow (\mathsf{P},u) of \operatorname{Elt}(\mathbf{Pol}_{\omega}^*) where both (U^1,u_1) and (U^2,u_2) are primitive, there is an isomorphism \Theta\colon (U^1,u_1) \rightarrow (U^2,u_2) such that L^2 \circ \Theta = L^1.

Used by Remark 32

Remark

Remark 31

8HNN

A consequence of the existence and unicity properties above, together with Lemma 25, is that the functor \def-{-} \def#1{ \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }} \def#2{|{-}|} \def#3{| \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }|} \ifx-#1 #2 \else #3 \fi \colon \mathbf{Pol}_{\omega} \rightarrow \mathbf{Set} of Example 17 is familially representable [carboni1995connected], i.e.,can be expressed as a functor of the form

\bigsqcup_{i \in I} \operatorname{Hom}(U^i,-) \colon \mathbf{Pol}_{\omega} \rightarrow \mathbf{Set}\makebox[0pt][l]{.}

Here, I is a set of representatives (U^i,u^i) of all polyplexes (considered up to isomorphism of elements in \operatorname{Elt}(\mathbf{Pol}_{\omega}^*)) of any dimension. Those can for instance be enumerated by constructing one polyplex liftings for each cell of the free precategory on the terminal polygraph. A similar description holds for the functor \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_k, mapping a polygraph to the set of k-cellsof the associated free precategory: the family I is now a set of representatives for the polyplexes of dimension k up to isomorphism.

Uses Lemma 25

Remark

Remark 32

MQDN

A consequence of the canonicity of a polyplex liftings given by the above properties is that one can define a polyplex measure on the cells of free precategories. Let \mathsf{P} \in \mathbf{Pol}_{\omega}, and write \mathbb{Z}\mathsf{P} for the free \mathbb{Z}-module on \def-{-} \def#1{\mathsf{P}} \def#2{|{-}|} \def#3{|\mathsf{P}|} \ifx-#1 #2 \else #3 \fi. Given u \in \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }, one can define \operatorname{\delta} \def#1{\mathsf{P}} \ifx#1\empty \else ^{\mathsf{P}} \fi (u) as follows. Consider a polyplex lifting F \colon (V,v) \rightarrow (\mathsf{P},u) and define S_V \in \mathbb{Z} V by S_V = \sum_{g\in V} g. Then, one defines \operatorname{\delta} \def#1{\mathsf{P}} \ifx#1\empty \else ^{\mathsf{P}} \fi (u) as \mathbb{Z} F(S_V). The definition of \operatorname{\delta} \def#1{\mathsf{P}} \ifx#1\empty \else ^{\mathsf{P}} \fi (u) does not depend on the choice of (V,v) by Lemma 25, Proposition 30. The question of the existence of a similar measure for free strict categories was raised by Makkai in [makkai2005word]. Later, using the standard Eckmann–Hilton for strict categories, the non-existence of such a measure was proven [forest:tel-03155192, Proposition 2.5.2.13].

Uses Lemma 25, Proposition 30

Lemma

Lemma 33

7C77

The functor \mathcal{U} is fully faithful.

Proposition

Proposition 34

XJNE

Let (\mathsf{P},g) \in \operatorname{Elt}(\mathbf{Pol}_{\omega}). Then

(\mathsf{P},g) is principal if and only if \mathcal{U}(\mathsf{P},g) is principal,
(\mathsf{P},g) is a plex if and only if \mathcal{U}(\mathsf{P},g) is a polyplex.

Theorem

Theorem 35

YU1W

The category \mathbf{Pol}_{\omega} is a concrete presheaf category.

Used by Remark 36

Remark

Remark 36

T1RF

Following Makkai’s proof of [makkai2005word, Theorem 4], the base category of the presheaf category given by the above theorem is a small full subcategory of \mathbf{Pol}_{\omega}, whose objects are (the underlying polygraphs of) plexes, and such that every (underlying polygraph of a) plex is isomorphic to exactly one object of this subcategory. The objects of the latter can thus be easily enumerated, since they are in correspondence with the generators of the terminal polygraph \mathbf{1}, as plex liftings.

Uses Theorem 35

Remark

Remark 37

U5LW

Like the familial representability observed in Remark 31, the conditions ?, ?, ? proved above entails a familial representability for the functor \def-{-} \def#1{-} \def#2{|{-}|} \def#3{|-|} \ifx-#1 #2 \else #3 \fi of Example 16, which can be expressed as

\bigsqcup_{i\in I} \operatorname{Hom}(U^i,-) \colon \mathbf{Pol}_{\omega} \rightarrow \mathbf{Set} \makebox[0pt][l]{.}

Here, I is a set of representatives (U^i,g^i) of all plexes (considered up to isomorphism of \operatorname{Elt}(\mathbf{Pol}_{\omega})). By taking I to be a set of representatives of all plexes of dimension k for some k \in \mathbb{N}, one get a familial representability of the functor (-)_k \colon \mathbf{Pol}_{\omega} \rightarrow \mathbf{Set}.

Remark

Remark 38

QSE7

In [araujo2022computads], [araujo2022computads] relies on [dean2022computads, Proposition 5.14], which gives sufficient conditions for a category to be a presheaf category on a given full subcategory. The difference with [makkai2005word, Theorem 4] is that the latter is relative to a concrete presheaf structure, and is able to characterize the shape category as a full subcategory of primitive elements.

Proposition

Proposition 39

55YB

Given n \in \mathbb{N} \cup \{\omega\}, the functor \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } \colon \mathbf{Pol}_{n} \rightarrow \mathbf{PCat}_{n} preserves connected limits.

Theorem

Theorem 40

KIOV

Given n \in \mathbb{N} \cup \{\omega\}, the functor \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_\mathbf{1} \colon \mathbf{Pol}_{n} \rightarrow \def#1{n} \ifx#1\empty \mathbf{PCat}_{\omega} \else \mathbf{PCat}_{n} \fi / \def-{-} \def#1{\mathbf{1}} \def#2{(-)} \def#3{\mathbf{1}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } is a right adjoint. In other words, \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } is a parametric right adjoint.

Corollary

Corollary 41

KREP

Given n\in \mathbb{N} \cup \{\omega\}, C \in \mathbf{PCat}_{n} and \mathsf{P} \in \mathbf{Pol}_{n}, every F \colon C \rightarrow \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } \in \mathbf{PCat}_{n} admits a generic factorization.

Proposition

Proposition 42

H3C5

Given n \in \mathbb{N} and \mathsf{P} \in \mathbf{Pol}_{\omega}, writing u for the non-identity n-cell of D^n, a functor F \colon D^n \rightarrow \def-{-} \def#1{\mathsf{P}} \def#2{(-)} \def#3{\mathsf{P}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } is generic if and only if (\mathsf{P},F(u)) is a polyplex.

Used by Remark 44

Remark

Remark 43

H4BN

In a related manner, given n \in \mathbb{N} and v \in \def-{-} \def#1{\mathbf{1}} \def#2{(-)} \def#3{\mathbf{1}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_n, the image of D^n \xrightarrow{v} \def-{-} \def#1{\mathbf{1}} \def#2{(-)} \def#3{\mathbf{1}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }, seen as an object of \def#1{} \ifx#1\empty \mathbf{PCat}_{\omega} \else \mathbf{PCat}_{} \fi / \def-{-} \def#1{\mathbf{1}} \def#2{(-)} \def#3{\mathbf{1}} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }, by a left adjoint to \def-{-} \def#1{-} \def#2{(-)} \def#3{-} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi }_\mathbf{1} is the underlying polygraph of a polyplex lifting of v.

Remark

Remark 44

ECR2

The above generic factorization can be seen as a stronger version of Proposition 11. Indeed, given k,l > 0 and i = \min(k,l) - 1, there exists a polygraph \mathsf{D}^{k,l} such that \def-{-} \def#1{(\mathsf{D}^{k,l})} \def#2{(-)} \def#3{(\mathsf{D}^{k,l})} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } is the free \omega-precategorywith one k-cellu_1 and one l-cellu_2, such that \partial^+_i(u_1) = \partial^-_i(u_2). The construction of \mathsf{D}^{k,l} can be seen to induce a polyplex (\mathsf{D}^{k,l},u_1\mathbin{\ast}_i u_2) by Lemma 28. Writting n for \max(k,l) and F^{k,l} \colon D^n \rightarrow \def-{-} \def#1{(\mathsf{D}^{k,l})} \def#2{(-)} \def#3{(\mathsf{D}^{k,l})} \ifx-#1 #2 \else #3 \fi ^{* \def#1{} \ifx#1\empty \else , \fi } for the functor sending the non-trivial n-cellof D^n to u_1\mathbin{\ast}_i u_2, Proposition 11 amounts to observe that the F^{k,l}’s are generic by Proposition 42.

Uses Lemma 28, Proposition 42

Property

Property 45 (Weak division)

KLXS

Given an \omega-precategoryC and an equivalence u : x \rightarrow y \in C_1, for any 1-cellss,t : y \rightarrow z and for any 2-cell w : u \mathbin{\ast}_0 s \Rightarrow u \mathbin{\ast}_0 t,

there is a 2-cellv : s \Rightarrow t such that u \mathbin{\ast}_0 v \sim w,
\begin{tikzcd}[row sep=1ex] &y\ar[dr,bend left,"s"]\\ x\ar[ur,bend left,"u"]\ar[dr,bend right,"u"']\ar[rr,phantom,"w\Downarrow"]&&z\\ &y\ar[ur,bend right,"t"'] \end{tikzcd} \qquad\sim\qquad \begin{tikzcd} x\ar[r,"u"]&y\ar[r,bend left=50,"s"]\ar[r,bend right=50,"t"']\ar[r,phantom,"v\Downarrow"]&z \end{tikzcd}
for any 2-cellsv,v':s\Rightarrow t such that u\mathbin{\ast}_0v\sim w\sim u\mathbin{\ast}_0 v' we have v\sim v'.

Source and licence

The text on this page is from arXiv:2211.16099v1 by Simon Forest and Samuel Mimram, under the licence CC BY 4.0. The corpus made these changes: it read the items out of the LaTeX source, it expanded the macros of the paper, it put each proof after its statement, and it converted the text to HTML. The formulas are the TeX of the paper, and KaTeX renders them. A formula or a reference can look different from the PDF. The page is published under CC BY 4.0.

The record of each item is in analysis/objects/2211/2211.16099.jsonl.