# Strict refinement property of connected loop-free
categories

Aly-Bora Ulusoy, Emmanuel Haucourt

<figure><img src="image_1.png" /></figure>

## To cite this version:

Aly-Bora Ulusoy, Emmanuel Haucourt. Strict refinement property of connected loop-free categories. 2024. hal-04482394

HAL Id: hal-04482394

https://hal.science/hal-04482394

Preprint submitted on 31 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Strict refinement property of connected loop-free categories

Aly-Bora Ulusoy¹ and Emmanuel Haucourt¹

¹Cosynus, École Polytechnique, Palaiseau, 91120, France.

Contributing authors: aly-bora.ulusoy@polytechnique.edu; haucourt@lix.polytechnique.fr;

## Abstract

In this paper we study the strict refinement property for connected partial orders also known as Hashimoto's Theorem. This property implies that any isomorphism between products of irreducible structures is determined is uniquely determined as a product of isomorphisms between the factors. This refinement implies a sort of smallest possible decomposition for such structures. After a brief recall of the necessary notion we prove that Hashimoto's theorem can be extended to connected loop-free categories, i.e. categories with no non-trivial morphisms endomorphisms. A special case of such categories is the category of connected components, for concurrent programs without loops.

**Keywords:** loop-free categories, refinement property, concurrent programs

**MSC Classification:** 06A06

Connected posets (i.e. those in which for all elements $x$ and $y$ we have a sequence $x = z_0, z_1, \dots, z_n = y$ such that $z_i$ and $z_{i-1}$ are comparable for every $i \in \{1, \dots, n\}$) satisfy the strict refinement property [1]: if the following isomorphism holds in the category of posets (Pos)

$$ \prod_{\alpha \in A} X_{\alpha} \cong \prod_{\beta \in B} Y_{\beta} $$

then we have a family of posets $\{Z_{\alpha,\beta} | \alpha \in A; \beta \in B\}$ such that the following isomorphisms hold for every $\alpha \in A$ and every $\beta \in B$.

$$ X_{\alpha} \cong \prod_{b \in B} Z_{\alpha, b} \quad \text{and} \quad Y_{\beta} \cong \prod_{a \in A} Z_{a, \beta} $$
A (small) category is said to be loop-free when any two of its morphisms whose composite is an endomorphism are identities. The category of loop-free categories (LFCat), which is a full subcategory of the category of small categories (Cat), contains Pos as a full subcategory. The embedding Pos ↪ → LFCat has a left adjoint obtained by identifying any two arrows with the same source and the same target. The purpose of this article is to prove that connected loop-free categories also satisfy the strict refinement property:

**Theorem A.** Given a connected loop-free category $\mathcal{C}$, for any two decompositions $\Psi_A : \mathcal{C} \to \coprod_{\alpha \in A} X_\alpha$ and $\Psi_B : \mathcal{C} \to \coprod_{\beta \in B} Y_\beta$, there exists a family of loop-free categories $Z_{\alpha,\beta}$ with $\alpha \in A$ and $\beta \in B$, and for every $\alpha \in A$ and $\beta \in B$, decompositions

$$a_{\alpha} : X_{\alpha} \to \coprod_{\beta \in B} Z_{\alpha, \beta} \quad \text{and} \quad b_{\beta} : Y_{\beta} \to \coprod_{\alpha \in A} Z_{\alpha, \beta}$$

such that the following diagram commutes:

<figure><img src="image_3.png" /></figure>

where $\gamma : \coprod_{\alpha \in A} \coprod_{\beta \in B} Z_{\alpha, \beta} \to \coprod_{\beta \in B} \coprod_{\alpha \in A} Z_{\alpha, \beta}$ is the natural isomorphism sending $((z_{\alpha,\beta})_{\beta \in B})_{\alpha \in A}$ to $((z_{\alpha,\beta})_{\alpha \in A})_{\beta \in B}$.

The structure of our proof diverges from Hashimoto's original paper [2] and instead follows more closely the presentation found in [1, Chapter 10] which has the added advantage of also constructing the elements of the refinement.

Beyond its pure theoretical interest, this problem is related to the study of programs made of several sequential processes running in parallel [3] (in the sequel we just write 'program'). The geometric model $[[P]]$ of a program $P$ is locally ordered [4, Corollary 6.1], so each of its points has a neighborhood whose fundamental category [5, 4.37, p.73] is loop-free. The crucial facts are:

1. the functor $\pi_1 : \mathbf{C} \to \mathbf{Cat}$, which assigns to every object of $\mathbf{C}$ its fundamental category, preserves finite products, and

2. two programs $P$ and $Q$ do not interact with each other when we have $[[P|Q]] \cong [[P]] \times [[Q]]$ (in $\mathbf{C}$) [4, Theorem 6.2].
Hence splitting a program *P* into subprograms that are executed independently of each other is somewhat related to writing the loop-free categories $\vec{\pi}_1(V)$ as finite product, for *V* partially ordered open subspace of $\llbracket P \rrbracket$. We expect that these local decompositions actually induce a global decomposition of $\vec{\pi}_1(\llbracket P \rrbracket)$; our hope is based on the van Kampen theorem [5, 4.52, p.80].

# 1 Definitions

Given an object *X* of a category *C*, we write *id*<sub>*X*</sub> for the identity morphism on *X*. We generally omit the subscript when clear from the context. Given a morphism *f*: *X* → *Y*, we write $\vec{f} = *X$ (resp. $\underline{f} = *Y$) for its *source* (resp. *target*).

**Definition 1.** A morphism $f: x \to y$ in a category $C$ is said to be *without return* when the hom-set $C(y, x)$ is empty. Otherwise, we say that $f$ *admits a return*. A category $C$ is said to be *loop-free* when all its morphisms, except identities, are without return. We write **LFCat** for the category of all small loop-free categories.

**Definition 2.** In **LFCat**, consider a family $\{f_\alpha : X_\alpha \to Y_\alpha\}_{\alpha \in A}$ of morphisms. The product map $f: \prod_{\alpha \in A} X_\alpha \to \prod_{\alpha \in A} Y_\alpha$ is the unique morphism such that $\pi_\alpha f = f_\alpha$ for every $\alpha \in A$.

For the rest of the chapter we will often write $f = (f_\alpha)_{\alpha \in A}$ for the product map of the family $\{f_\alpha : X_\alpha \to Y_\alpha\}_{\alpha \in A}$. For binary products, we write $(f,g)$ the product map of $f$ and $g$.

**Definition 3.** A *fence* is a family $(f_i)_{1 \le i \le n}$ of morphisms of *C* such that:

* $\underline{f_{2i}} = \underline{f_{2i+1}}$ and $\overline{f_{2i-1}} = \overline{f_{2i}}$

* or $\overline{f_{2i}} = \underline{f_{2i+1}}$ and $\underline{f_{2i-1}} = \underline{f_{2i}}$

The *length* of a fence $(f_i)_{1 \le i \le n}$ is its cardinal $n$.

**Definition 4.** Two morphisms $f$ and $g$ of a category $C$ are said to be *connected* if there exists a fence $(f_i)_{i \in [1, n]}$ such that $f = f_1$ and $g = f_n$. A category $C$ is said to be *connected* if all its morphisms are connected.

**Definition 5.** A (*product*) *decomposition* of a loop-free category *C* is an isomorphism $\Psi$ from *C* to a product $\prod_{\alpha \in A} X_\alpha$ of loop-free categories $X_\alpha$ for $\alpha \in A$.

Note that if $C$ is non-empty, connected, and loop-free, then so are the categories $X_\alpha$.

# 2 Hashimoto’s theorem for loop-free categories

Hashimoto’s Theorem [2] states that every connected partial order has the strict refinement property; in this article, we generalize this result to all connected loop-free categories in Theorem A.

As previously stated, we will follow the proof from [1], generalizing the key lemmas to the case of connected loop-free categories. We will first give a rough idea of the different steps of the proofs, before introducing the details and technical lemmas necessary for the proof in Section 3.
To prove Theorem A we will need to find the decompositions $(a_\alpha)_{\alpha \in A}$ and $(b_\beta)_{\beta \in B}$ of Eq. (1). For this we will first define some notions, that will be used in the presentation of the proof.

**Definition 6.** Given an element $s$ of a set product $\prod_{i \in I} S_i$, an index $j \in I$, and an element $x_j \in S_j$, we define $(s, x_j, j)_{i \in I}$ as the element of $\prod_{i \in I} S_i$ obtained by substituting $x_j$ to $s_j$ in $s$; in other words:

$$ (s, x_j, j)_i = \begin{cases} x_j & \text{if } i = j \\ s_i & \text{otherwise.} \end{cases} $$

**Definition 7.** Given an object $s$ of a loop-free category $\prod_{\alpha \in A} X_\alpha$, and an index $\lambda \in A$, the $\lambda$-section at $s$ is the functor from $X_\lambda$ to $\prod_{\alpha \in A} X_\alpha$ defined by

$$ \begin{cases} x_\lambda \mapsto (s, x_\lambda, \lambda) & \text{if } x_\lambda \text{ is an object} \\ f_\lambda \mapsto (\mathrm{id}_s, f_\lambda, \lambda) & \text{if } f_\lambda \text{ is a morphism} \end{cases} $$

We denote by $\Xi_\lambda^s : X_\lambda \cong X_\lambda^s$ the isomorphism induced by the $\lambda$-section at $s$ on its image. We denote by $\Phi_\lambda^s$ the restriction of $\Phi$ to $X_\lambda^s$ for every functor $\Phi$ defined over $\prod_{\alpha \in A} X_\alpha$.

**Definition 8.** Given an isomorphism $\Phi: \prod_{\alpha \in A} X_\alpha \to \prod_{\beta \in B} Y_\beta$, indexes $\lambda \in A$, $\mu \in B$, and an object $s \in \prod_{\alpha \in A} X_\alpha$, we define

$$ X_\lambda^\mu := \pi_\lambda \Phi^{-1} \Xi_\mu^{\Phi(s)} (Y_\mu) \quad \text{and} \quad Y_\mu^\lambda := \pi_\mu \Phi \Xi_\lambda^s (X_\lambda) $$

with $\pi_\lambda: \prod_{\alpha \in A} X_\alpha \to X_\lambda$ and $\pi_\mu: \prod_{\beta \in A} X_\beta \to X_\mu$ the projections.

As we will see, the refinement (but not its existence) $Z_{\alpha,\beta}$ (with $\alpha \in A$ and $\beta \in B$) depends on an object $s \in \prod_{\alpha \in A} X_\alpha$ that we arbitrarily fix now if the product is non-empty. In [1], which proves the strict refinement property for connected posets, the isomorphisms $(a_\alpha)_{\alpha \in A}$ and $(b_\beta)_{\beta \in B}$ of Diagram 1 are obtained by decomposing the expected isomorphisms into smaller morphisms, obtained with the notation introduced above, which gives the Diagram 2 below.
<figure><img src="image_4.png" /></figure>

The first part of the proof is to prove that all the introduced morphisms, are in fact isomorphisms and to prove that they are indeed product maps of isomorphisms. That is to say that we have $\Psi_2 = \prod_{\alpha \in A} a_\alpha$ and $\Psi_1 = \prod_{\beta \in B} b_\beta$ with

$$a_{\alpha} = (\pi_{\alpha} \Phi^{-1} \Xi_{\beta}^{\Phi^{(s)}} \pi_{\beta} \Phi \Xi_{\alpha}^{s})_{\beta \in B} \quad \text{and} \quad b_{\beta} = \Phi^{-1} \Xi_{\beta}^{\Phi^{(s)}}$$

Most of the proofs rely heavily on the following proposition, which allows us to restrain the coordinates of composite images.

**Lemma 8.** Let $\Phi: \mathcal{P} \times \mathcal{Q} \to \mathcal{U} \times \mathcal{V}$ an isomorphism of connected loop-free categories. Let $(u, v)$ and $(u', v')$ two morphisms of $\mathcal{U} \times \mathcal{V}$ and $p$ a morphism of $\mathcal{P}$. Then $\pi_{\mathcal{P}}\Phi^{-1}(u, v) = \pi_{\mathcal{P}}\Phi^{-1}(u', v') = p$ implies $\pi_{\mathcal{P}}\Phi^{-1}(u, v') = p$.

Then, once this has been achieved, we need to prove that the diagram commutes to conclude the proof. To do this, we will first prove the commutation on a restriction of the diagram, by replacing for each $\alpha \in A$ the starting category $X_\alpha$ by the subcategory $X_\alpha^\mu$ as in Definition 8, for an arbitrary $\mu \in \beta$, giving us the diagram below.

<figure><img src="image_5.png" /></figure>

Then using the following Lemma 10, the commutation is extended along a given $\lambda \in A$.
Proof. If $f \circ g = \text{id}$, then both $f$ and $g$ have a return; it follows that both are identities because $C$ is loop-free. □

**Lemma 5.** Given an isomorphism of small, loop-free categories $\Phi: C_1 \times C_2 \to D_1 \times D_2$ and an object $X$ of $C_1$, for all morphisms $(f, g)$ of $D_1 \times D_2$ such that $\pi_1 \Phi^{-1}(f, g) = \text{id}_X$, we have:

$$ \pi_1 \Phi^{-1}(f, \text{id}_g) = \pi_1 \Phi^{-1}(f, \text{id}_g) = \pi_1 \Phi^{-1}(\text{id}_f, g) = \pi_1 \Phi^{-1}(\text{id}_f, g) = \text{id}_X. $$

*Proof.* By definition of the product, the following diagram on the left commutes:

<figure><img src="image_6.png" /></figure>

The category $\mathcal{P}$ is loop-free, thus by applying Lemma 4 we have

$$ \pi_1 \Phi^{-1}(\text{id}_f, g) = \pi_1 \Phi^{-1}(f, \text{id}_g) = \text{id} $$

We prove in the same way that $\pi_1 \Phi^{-1}(\text{id}_f, g) = \pi_1 \Phi^{-1}(f, \text{id}_g) = \text{id}$. □

## 3.2 Technical lemmas

The proof of Hashimoto's theorem in [1] makes extensive use of the Proposition 6 and Proposition 7, which we will respectively extend to connected elements of LFCat in Lemma 8 and Lemma 10. As we have changed the formulation to make the proofs easier to follow, we give them here and refer to the original work for the proof.

These lemmas are at the core of the proof and are where the hypothesis that we are using loop-free and connected categories really comes into play, so it is important to keep them in mind.

**Proposition 6.** Given $\Phi: P \times Q \to U \times V$ an isomorphism of connected posets and $p \in P$,

$$ \pi_P \Phi^{-1}(u, v) = \pi_P \Phi^{-1}(u', v') = p \text{ implies } \pi_P \Phi^{-1}(u, v') = p $$

*Proof.* [1, Lemma 10.4.5]. □

**Proposition 7.** Given $\Phi: P \times Q \to U \times V$ an isomorphism of connected posets, if there exists $p \in P$ such that $\pi_U \Phi(p, q) = \pi_U \Phi(p, q')$, then for each $p' \in P$,

$$ \pi_U \Phi(p', q) = \pi_U \Phi(p', q') $$

*Proof.* [1, Lemma 10.4.8] □

In the two following proofs, as the objects in the commutative diagrams are of no importance, we have omitted them, replacing them by • when not necessary.
**Lemma 8.** Let $\Phi: \mathcal{P} \times \mathcal{Q} \to \mathcal{U} \times \mathcal{V}$ an isomorphism of connected loop-free categories. Let $(u, v)$ and $(u', v')$ two morphisms of $\mathcal{U} \times \mathcal{V}$ and $p$ a morphism of $\mathcal{P}$. Then $\pi_{\mathcal{P}}\Phi^{-1}(u, v) = \pi_{\mathcal{P}}\Phi^{-1}(u', v') = p$ implies $\pi_{\mathcal{P}}\Phi^{-1}(u, v') = p$.

*Proof.* Given $p, q, q'$ such that $\Phi(p, q) = (u, v)$ and $\Phi(p, q') = (u', v')$. Let us prove that $\pi_{\mathcal{P}}\Phi^{-1}(u, v') = p$. We proceed by induction on the length of the fence between $q$ and $q'$.

* A fence of length 2 implies $q = q'$ or $\bar{q} = \bar{q}'$. First, let us suppose $q = q'$, the other case being solved dually.
Let us prove that $\pi_{\mathcal{P}}\Phi^{-1}(u, v') = p$.
First, let us define

$$ \Phi(p, \mathrm{id}_q) := (u^*, v^*) \qquad \Phi(\mathrm{id}_{\bar{p}}, q) := (u_q, v_q) \qquad \Phi(\mathrm{id}_{\bar{p}}, q') := (u'_q, v'_q) \quad (5) $$

such that:

$$ u = u_q \circ u^* $$

$$ u' = u'_q \circ u^* $$

$$ v = v_q \circ v^* $$

$$ v' = v'_q \circ v^* $$

By the ??, the following diagram commutes:

<figure><img src="image_7.png" /></figure>

Following the outer arrows, we get

$$ (u, v') = (u_q, v'_q) \circ (u^*, v^*) $$

By Eq. (5), $\pi_{\mathcal{P}}\Phi^{-1}(u^*, v^*) = p$. We are thus left to prove $\pi_{\mathcal{P}}\Phi^{-1}(u_q, v'_q) = \mathrm{id}$. By construction $v_q = v'_q = \bar{v}^*$ such that by functoriality:

$$ \pi_{\mathcal{P}}\Phi^{-1}(u_q, v'_q) = \pi_{\mathcal{P}}\Phi^{-1}(u_q, v'_q) $$
$$ 
\begin{aligned}
&= \pi_P \Phi^{-1}(\underline{u_q}, \underline{v_q}) \\
&= \underline{\pi_P \Phi^{-1}(u_q, v_q)} \\
\underline{\pi_P \Phi^{-1}(u_q, v'_q)} &= \bar{p}
\end{aligned}
$$

By Proposition 3, $\Phi: \mathrm{Obj}(\mathcal{P}) \times \mathrm{Obj}(\mathcal{Q}) \to \mathrm{Obj}(\mathcal{U}) \times \mathrm{Obj}(\mathcal{V})$ is an order-preserving isomorphism of connected posets and such that $\pi_P \Phi^{-1}(\underline{u_q}, \underline{v_q}) = \pi_P \Phi^{-1}(\bar{u'_q}, \bar{v'_q}) = \bar{p}$. Hence,

$$ 
\begin{array}{l}
\bar{p} = \pi_P \Phi^{-1}(\underline{u_q}, \underline{v'_q}) \\
\bar{p} = \underline{\pi_P \Phi^{-1}(u_q, v'_q)}
\end{array}
\qquad \begin{array}{l}
\text{Proposition 6} \\
\text{by functoriality}
\end{array}
$$

Thus, $\pi_P \Phi^{-1}(u_q, v'_q) \in \mathcal{P}(\bar{p}, \bar{p})$, with $\mathcal{P}$ loop-free. This implies $\pi_P \Phi^{-1}(u_q, v'_q) = \mathrm{id}_{\bar{p}}$, such that

$$ 
\begin{aligned}
\pi_P \Phi^{-1}(u, v') &= \pi_P \Phi^{-1}(u_q, v'_q) \circ \pi_P \Phi^{-1}(u^*, v^*) \\
\pi_P \Phi^{-1}(u, v') &= p
\end{aligned}
$$

$$ 
\begin{array}{l}
\bullet \text{ Now let us suppose a fence } \xrightarrow{q'} \xleftarrow{r} \xrightarrow{q} \text{ of length } n=3 \text{ between } q \text{ and } q'. \text{ Let} \\
(u, v) := \Phi(p, q) \qquad (x, y) := \Phi(p, r) \qquad (u', v') := \Phi(p, q') \qquad (6)
\end{array}
$$

such that $\Phi$ sends the commutative diagram on top to the one below.

<figure><img src="image_8.png" /></figure>

<figure><img src="image_9.png" /></figure>

We are going to use the same method as before, working on each 2-fence inside the 3-fence above. For that we'll decompose $(u, v')$ using the Diagram 7. By the ??, the following diagram commutes:
<figure><img src="image_10.png" /></figure>

such that

$$ (u, v') = (u_q, \mathrm{id}_{\bar{v}'}) \circ (u^*, y^*) \circ (\mathrm{id}_{\underline{u^*}}, v'_q) \quad \text{By following the outer arrows} $$

$$ (u, v') = (u_q, \mathrm{id}_{\bar{v}_r}) \circ (u^*, y^*) \circ (\mathrm{id}_{\underline{u'_r}}, v'_q) \quad \text{By the Diagram 7} $$

- Working on the 2-fence $\xleftarrow{q} \xrightarrow{r}$, let us prove $\pi_P \Phi^{-1}(u_q, \mathrm{id}_{\bar{v}_r}) = \mathrm{id}$

By Eq. (6) we have $\pi_P \Phi^{-1}(u, v) = \pi_P \Phi^{-1}(x, y) = p$. Thus, as proved for 2-fences above

$$ \begin{align*} p &= \pi_P \Phi^{-1}(u, y) \\ &= \pi_P \Phi^{-1}((u_q, v_r) \circ (u^*, v^*)) \qquad \text{Diagram 7} \\ &= \pi_P \Phi^{-1}(u_q, v_r) \circ \pi_P \Phi^{-1}(u^*, v^*) \qquad \text{Functoriality} \\ p &= \pi_P \Phi^{-1}(u_q, v_r) \circ p \qquad \text{Diagram 7} \end{align*} $$

By loop-free property of $\mathcal{P}$, $\pi_P \Phi^{-1}(u_q, v_r) = \mathrm{id}_{\bar{p}}$. Which implies by Lemma 5,

$$ \pi_P \Phi^{-1}(u_q, \mathrm{id}_{\bar{v}_r}) = \mathrm{id}_{\bar{p}} $$

Similarly, $\pi_P \Phi^{-1}(\mathrm{id}_{\underline{u'_r}}, v'_q) = \mathrm{id}_{\underline{p}}$. Hence

$$ \begin{align*} \pi_P \Phi^{-1}(u, v') &= \pi_P \Phi^{-1}(u_q, \mathrm{id}_{\bar{v}_r}) \circ \pi_P \Phi^{-1}(u^*, y^*) \circ \pi_P \Phi^{-1}(\mathrm{id}_{\underline{u'_r}}, v'_q) \\ &= \mathrm{id}_{\bar{p}} \circ \pi_P \Phi^{-1}(u^*, y^*) \circ \mathrm{id}_{\underline{p}} \\ \pi_P \Phi^{-1}(u, v') &= \pi_P \Phi^{-1}(u^*, y^*) \end{align*} $$

- Let us prove now $\pi_P \Phi^{-1}(u^*, y^*) = p$. By commutativity of both projections the central square:

$$ \begin{align*} (x, y) &= (u_r \circ u^*, y^* \circ v'_r) \\ &= (u_r, \mathrm{id}_{\bar{u}^*}) \circ (u^*, y^*) \circ (\mathrm{id}_{\underline{u}^*}, v'_r) \\ (x, y) &= (u_r, \mathrm{id}_{\underline{v}_r}) \circ (u^*, y^*) \circ (\mathrm{id}_{\underline{u}'_r}, v'_r) \end{align*} $$
As $\pi_P\Phi^{-1}(u_r, v_r) = \text{id}_{\overline{p}}$, by Lemma 5, $\pi_P\Phi^{-1}(u_r, \text{id}_{\overline{v_r}}) = \text{id}_{\overline{p}}$. Similarly, we have $\pi_P\Phi^{-1}(\text{id}_{u'}, \text{id}_{v'}) = \text{id}_{\overline{p}}$. Thus

$$p = \pi_P\Phi^{-1}(x, y) = \pi_P\Phi^{-1}(u^*, y^*)$$

Such that

$$\pi_P\Phi^{-1}(u, v') = p$$

* Now let us suppose that the property holds for all fences of length $1 \le k < n$, with $n > 3$. Let us suppose given $q, q'$, connected by a fence $(q_i)_{1 \le i \le n}$. We define $(u_i, v_i) := \Phi(p, q_i)$, for each $1 \le i \le n$ and

$$(u, v) := (u_1, v_1) = \Phi(p, q_1) = \Phi(p, q)$$

$$(u', v') := (u_n, v_n) = \Phi(p, q_n) = \Phi(p, q')$$

By definition, $((p, q_i))_{1 \le i \le n-1}$ and $((p, q_i))_{2 \le i \le n}$ are fences of length $n-1$ respectively connecting $(p, q_1)$, $(p, q_{n-1})$ and $(p, q_2)$, $(p, q_n)$. By definition of $(u_i, v_i)$ we have,

$$p = \pi_P\Phi^{-1}(u_1, v_1) = \pi_P\Phi^{-1}(u_{n-1}, v_{n-1})$$

$$p = \pi_P\Phi^{-1}(u_2, v_2) = \pi_P\Phi^{-1}(u_n, v_n)$$

Thus, by induction hypothesis, this implies

$$p = \pi_P\Phi^{-1}(u_1, v_{n-1}) \qquad p = \pi_P\Phi^{-1}(u_2, v_n) \qquad (8)$$

Now we suppose $\overline{q_1} = \overline{q_2}$ ($\overline{q_1} = \overline{q_2}$ can be treated dually). We'll have to proceed differently depending on the symmetry of the fence.

- If $\overline{q_{n-1}} = \overline{q_n}$, by functoriality of $\Phi$, $\overline{u_{n-1}}, \overline{v_{n-1}} = \overline{u_n}, \overline{v_n}$, such that $\overline{u_2}, \overline{v_n} = \overline{u_1}, \overline{v_{n-1}}$. This implies that $(u_1, v_{n-1})$ and $(u_2, v_n)$ are connected by a fence of length 2. Thus, $\pi_Q\Phi^{-1}(u_1, v_{n-1})$ and $\pi_Q\Phi^{-1}(u_2, v_n)$ are connected by a fence of length 2. By Eq. (8), we have $p = \pi_P\Phi^{-1}(u_2, v_n) = \pi_P\Phi^{-1}(u_1, v_{n-1})$. We can then apply our induction hypothesis, such that

$$p = \pi_P\Phi^{-1}(u_1, v_n)$$

$$p = \pi_P\Phi^{-1}(u, v')$$

Which concludes this case.

- If $\overline{q_{n-1}} = \overline{q_n}$, by functoriality of $\Phi$, $\overline{u_{n-1}}, \overline{v_{n-1}} = \overline{u_n}, \overline{v_n}$. Thus, if we define $\overline{q_{2,n}} = \pi_Q\Phi^{-1}(u_2, v_n)$ and $\overline{q_{1,n-1}} = \pi_Q\Phi^{-1}(u_1, v_{n-1})$, we get the following fences:
<figure><img src="image_11.png" /></figure>

Thus, $q_{2,n}$ et $q_{1,n-1}$ are connected by a fence of length 3. We can apply our induction case for $k=3$ with the fence $(p, q_{1,n-1})$, $(p, \pi_Q \Phi^{-1}(u_1, v_n))$, $(p, q_{2,n})$. Indeed, we have $\Phi(p, q_{1,n-1}) = (u_1, v_{n-1})$ and $\Phi(p, q_{2,n}) = (u_2, v_n)$ (Eq. (8)). Thus, we get

$$ \pi_P \Phi^{-1}(u_1, v_n) = p $$

Thus, $\pi_P \Phi^{-1}(u, v) = \pi_P \Phi^{-1}(u', v') = p$ implies $\pi_P \Phi^{-1}(u, v') = p$, proving the induction step. $\square$

This Lemma 8 is not restricted to binary product and easily extends to arbitrary products as shown in the following lemma.

**Corollary 9.** Let $\Phi: \coprod_{\alpha \in A} X_{\alpha} \to \coprod_{\beta \in B} Y_{\beta}$ an isomorphism of connected categories. Let $f^i = (f_{\alpha}^i)_{\alpha \in A}$ a morphism of $\coprod_{\alpha \in A} X_{\alpha}$ for $i = 1, 2$. Then for all $\lambda \in A$ and all $\mu \in B$ such that $\pi_{\lambda} f^1 = \pi_{\lambda} f^2$

$$ \pi_{\lambda} \Phi^{-1}(\Phi(f^1), \Phi(f^2)_{\mu}, \mu) = \pi_{\lambda} f^1 = \pi_{\lambda} f^2 $$

*Proof.* This follows directly from Lemma 8 by defining:

$$ P := X_{\lambda} \qquad Q := \coprod_{\alpha \in A, \alpha \neq \lambda} X_{\alpha} \qquad U := Y_{\beta} \qquad V := \coprod_{\beta \in B, \mu \neq \beta} Y_{\beta} $$

and by defining

$$ (p, q) := \delta_{\lambda}^{-1}(f^1) \qquad (p, q') := \delta_{\lambda}^{-1}(f^2) $$

$$ (u, v) := \delta_{\mu}^{-1} \Phi(f^1) \qquad (u', v') := \delta_{\mu}^{-1} \Phi(f^2) $$

With $\delta_{\lambda}$ and $\delta_{\mu}$ the natural isomorphisms:

$$ \delta_{\lambda}: X_{\lambda} \times \coprod_{\alpha \in A, \alpha \neq \lambda} X_{\alpha} \to \coprod_{\alpha \in A} X_{\alpha} \qquad \delta_{\beta}: Y_{\mu} \times \coprod_{\beta \in B, \mu \neq \beta} Y_{\beta} \to \coprod_{\beta \in B} Y_{\beta} $$

We get an isomorphisms $\Psi = \delta_{\beta}^{-1} \circ \Phi \circ \delta_{\lambda}: P \times Q \to U \times V$. Such that $f_{\lambda}^{i} = \pi_{P} \Psi^{-1}(u, v')$ for $i = 1, 2$. $\square$

**Lemma 10.** Let $\Phi: \mathcal{P} \times \mathcal{Q} \to \mathcal{U} \times \mathcal{V}$ be an isomorphism of connected loop-free categories. Let $\mathcal{Q}'$ a connected subcategory of $\mathcal{Q}$. Let $p$ a morphism of $\mathcal{P}$. Then $\pi_U \Phi(p, q) = \pi_U \Phi(p, q')$ for all $q, q' \in \mathcal{Q}'$ implies, for all $p' \in \mathcal{P}$, $\pi_U \Phi(p', q) = \pi_U \Phi(p', q')$ for all $q, q' \in \mathcal{Q}'$.
Proof. Let $p$ a morphism of $\mathcal{P}$ Let $Q'$ a connected sub-category of $Q$, such that for all morphisms $q, q'$ in $Q'$, $\pi_U\Phi(p, q) = \pi_U\Phi(p, q')$. Let us prove that for all $p'$ morphism of $\mathcal{P}$, $\pi_U\Phi(p', q') = \pi_U\Phi(p', q)$ by induction on the length $n$ of a given fence connecting $q, q'$.

* $n = 1$. Trivial.

* $n = 2$. $\pi_U\Phi(p, q) = \pi_U\Phi(p, q')$ for all morphisms $q, q'$ in $Q'$ implies

$$ 
\begin{array}{l@{\qquad}l}
\underline{\pi_U\Phi(p, q)} = \underline{\pi_U\Phi(p, q')} & \\
\underline{\pi_U\Phi(\underline{p}, \underline{q})} = \underline{\pi_U\Phi(\underline{p}, \underline{q}')} & \text{for all } q, q' \in \operatorname{Mor}(Q) \\
\underline{\pi_U\Phi(\underline{p}, Q)} = \underline{\pi_U\Phi(\underline{p}, Q')} & \text{for all } Q, Q' \in \operatorname{Obj}(Q)
\end{array}
$$

By Proposition 3 $\Phi|_{\operatorname{Obj}(Q)}$ is an isomorphism between $\operatorname{Obj}(\mathcal{P}) \times \operatorname{Obj}(Q)$ and $\operatorname{Obj}(\mathcal{U}) \times \operatorname{Obj}(\mathcal{V})$. By Proposition 7

$$ \text{for all } Q, Q' \in \operatorname{Obj}(Q), \pi_U\Phi(\underline{p'}, Q) = \pi_U\Phi(\underline{p'}, Q') \quad (9) $$

Thus for $q \in \operatorname{Mor}(Q')$ we have

$$ 
\begin{align*}
\underline{\pi_U\Phi(\mathrm{id}_{\underline{p'}}, q)} &= \underline{\pi_U\Phi(\underline{p'}, q)} \\
&= \underline{\pi_U\Phi(\underline{p'}, \bar{q})} & \text{By Eq. (9)} \\
&= \underline{\pi_U\Phi(\mathrm{id}_{\underline{p'}}, \bar{q})} \\
\underline{\pi_U\Phi(\mathrm{id}_{\underline{p'}}, q)} &= \underline{\pi_U\Phi(\mathrm{id}_{\underline{p'}}, q)}
\end{align*}
$$

As $Q'$ is loop-free, this implies $\pi_U\Phi(\mathrm{id}_{\underline{p'}}, q) = \mathrm{id}$. Similarly, $\pi_U\Phi(\mathrm{id}_{\underline{p'}}, q') = \mathrm{id}$.

Let us suppose that $\bar{q} = \bar{q'}$, the other case being dual. By the above argument, the following diagrams commute

<figure><img src="image_12.png" /></figure>

Therefore, $\pi_U\Phi(p', q') = \pi_U\Phi(p', \mathrm{id}_{\bar{q}}) = \pi_U\Phi(p', q)$.

* Now suppose a fence $(q = q_0, q_1, \dots, q_n = q')$ and the property true for all integers strictly smaller than $n$. Then there is a $n-1$-fence $(q_1, \dots, q_n)$ and a 1-fence $(q_0, q_1)$. By induction hypothesis, $\pi_U\Phi(p', q_n) = \pi_U\Phi(p', q_1) = \pi_U\Phi(p', q_0)$.

$Q'$ is connected so for all $p' \in \mathcal{P}$, for all $q, q' \in Q'$, $\pi_U\Phi(p', q') = \pi_U\Phi(p', q')$. $\square$
# 4 Proof of Theorem A

For the remainder of section, we will consider that $\Phi$ is an isomorphism of connected loop-free categories, $(X_\alpha)_{\alpha \in A}$ and $(Y_\beta)_{\beta \in B}$ families of connected loop-free categories.

As stated before, we will first prove that all the morphisms of the Diagram 2 are isomorphisms.

**Lemma 11.** Given a category $X = \coprod_{\alpha \in A} X_\alpha$, $\lambda \in A$, $s$ a morphism of $X$ and $\Xi_\lambda^s$ as defined in Definition 7, then

$$ \pi_\lambda \circ \Xi_\lambda^s = \mathrm{id}_{X_\lambda} $$

We say that $\Xi_\lambda^s$ is a section of the canonical projection $\pi_\lambda: \coprod_{\alpha \in A} X_\alpha \to X_\lambda$. Furthermore, $\Xi_\lambda^s$ is a full and faithful functor

*Proof.* Let $f \in \coprod_{\alpha \in A} X_\alpha((s, x_\lambda, \lambda), (s, y_\lambda, \lambda))$. Then $X_\alpha$ loop-free implies, $\pi_\alpha f = \mathrm{id}_{s_\alpha}$ if $\alpha \neq \lambda$ and $\pi_\lambda f := f_\lambda \in X_\lambda(x_\lambda, y_\lambda)$. Such that $f = \Xi_\lambda^s(f_\lambda)$. This proves that $\Xi_\lambda^s$ is full. Furthermore, it is clearly faithful. □

**Corollary 12.** Given a category $X = \coprod_{\alpha \in A} X_\alpha$, $\lambda \in A$, $s$ a morphism of $X$ then $X_\lambda^s = \Xi_\lambda^s(X)$ is a connected, loop-free full sub-category of $X$ isomorphic to $X_\lambda$. Furthermore

$$ \pi_\lambda \circ \Xi_\lambda^s = \mathrm{id}_{X_\lambda} \qquad \Xi_\lambda^s \circ \pi_\lambda|_{X_\lambda^s} = \mathrm{id}_{X_\lambda^s} $$

One last proposition that we will need from [1] is the fact that for any $\lambda \in A$, $s_\lambda$ object of $X_\lambda$, the object part of the functor $\Phi|_{X_\lambda^s}: X_\lambda^s \to \coprod_{\beta \in B} Y_\beta^\lambda$ is an isomorphism of the underlying objects of the category.

**Proposition 13.** [1, Lemma 10.4.7]

Let $\Phi: \coprod_{\alpha \in A} X_\alpha \to \coprod_{\beta \in B} Y_\beta$ be an isomorphism of connected posets. Let $s \in \coprod_{\alpha \in A} X_\alpha$ and $\lambda \in A$ and $X_\lambda^s$ be as in Lemma 11. Let $Y_\beta^\lambda = \pi_\beta \Phi[X_\lambda^s]$, then

$$ \Phi|_{X_\lambda^s}: X_\lambda^s \to \coprod_{\beta \in B} Y_\beta^\lambda $$

is an isomorphism of posets.

This proposition also translates to an isomorphism of connected categories.

**Proposition 14.** Let $\Phi: \coprod_{\alpha \in A} X_\alpha \to \coprod_{\beta \in B} Y_\beta$ be an isomorphism of connected loop-free categories. Let $s \in \coprod_{\alpha \in A} X_\alpha$ and $\lambda \in A$ and $X_\lambda^s$ be as in Lemma 11. Let $Y_\beta^\lambda = \pi_\beta \Phi[X_\lambda^s]$, then

$$ \Phi|_{X_\lambda^s}: X_\lambda^s \to \coprod_{\beta \in B} Y_\beta^\lambda $$

is an isomorphism of connected loop-free categories.

*Proof.* Let us show that $\Phi|_{X_\lambda^s}: X_\lambda^s \to \coprod_{\beta \in B} Y_\beta^\lambda$ is essentially surjective. By Proposition 3, $\Phi_{\mathrm{Obj}|X_\lambda^s}$ is an isomorphism of posets. Thus, by Proposition 13,

$$ \Phi_{\mathrm{Obj}}[X_\lambda^s] = \coprod_{\beta \in B} \pi_\beta \Phi_{\mathrm{Obj}}[\mathrm{Obj}(X_\lambda^s)] $$
$$
= \prod_{\beta \in B} \mathrm{Obj}(\pi_{\beta} \Phi[X_{\lambda}^{s}])
$$
$$
\Phi_{\mathrm{Obj}}[X_{\lambda}^{s}] = \mathrm{Obj}(\prod_{\beta \in B} \pi_{\beta} \Phi[X_{\lambda}^{s}])
$$

Thus $\Phi|_{X_\lambda^s}$ is essentially surjective. Furthermore, $\Phi|_{X_\lambda^s}$ is full and faithful as the restric-
tion of a full and faithful functor to a full subcategory (Lemma 11 and Corollary 12).
Thus, $\Phi|_{X_\lambda^s}$ is a fully faithful and essentially surjective functor, thus an isomorphism
in LFCat
$\square$

**Proposition 15.** Let $\Phi: \prod_{\alpha \in A} X_{\alpha} \to \prod_{\beta \in B} Y_{\beta}$ an isomorphism of connected loop-free categories. Fix $\alpha \in A$ and $\beta \in B$. With

$$
Y_{\beta}^{\alpha} := \pi_{\beta} \Phi[X_{\alpha}^{s}] \qquad X_{\alpha}^{\beta} := \pi_{\alpha} \Phi^{-1}[Y_{\beta}^{\Phi(s)}]
$$

The two following morphisms are inverse of each other

$$
\pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} : Y_{\beta}^{\alpha} \to X_{\alpha}^{\beta} \qquad \pi_{\beta} \circ \Phi \circ \Xi_{\alpha}^{s} : X_{\alpha}^{\beta} \to Y_{\beta}^{\alpha}
$$

Proof. Let us prove that

$$
\pi_{\beta} \Phi \circ \Xi_{\alpha}^{s} \pi_{\alpha} \circ \Phi^{-1} \Xi_{\beta}^{\Phi(s)} |_{Y_{\beta}^{\alpha}} : Y_{\beta}^{\alpha} \to Y_{\beta}^{\alpha} \text{ is the identity.}
$$

First let us remark that $\pi_\beta \Phi \circ \Phi^{-1} \Xi_\beta^{\Phi(s)} = \mathrm{id}_{Y_\beta^\alpha}$ and $\Xi_\alpha^s \pi_\alpha |_{X_\alpha^s} = \mathrm{id}_{X_\alpha^s}$ (Corollary 12).
But this contraction can only be made if we prove that $\Phi^{-1} \Xi_\beta^{\Phi(s)}$ sends $Y_\beta^\alpha$ to a
subcategory of $X_\alpha^s$. As $\pi_\beta \Phi \Xi_\alpha^s : X_\alpha \to Y_\beta^\alpha$ is full and essentially surjective by Propo-
sition 14, it is equivalent to proving that $\Phi^{-1} \Xi_\beta^{\Phi(s)} \pi_\beta \Phi \Xi_\alpha^s$ sends $X_\alpha$ to a subcategory
of $X_\alpha^s$

Let $f_{\alpha} \in X_{\alpha}$ and $\lambda \in A, \lambda \neq \alpha$. By definition, $\pi_{\lambda} \mathrm{id}_{s} = \pi_{\lambda} \Xi_{\alpha}^{s} f$. Thus, by Corollary 9,

$$
\pi_{\lambda} \Phi^{-1}(\Phi(\mathrm{id}_{s}), \Phi(\Xi_{\alpha}^{s} f)_{\beta}, \beta) = \pi_{\lambda} \mathrm{id}_{s} \\
\text{i.e.} \qquad \pi_{\lambda} \Phi^{-1} \Xi_{\beta}^{\Phi(s)} \pi_{\beta} \Phi \Xi_{\alpha}^{s} f = \pi_{\lambda} \mathrm{id}_{s}
$$

Thus, $\Phi^{-1}\Xi_{\beta}^{\Phi(s)}\pi_{\beta}\Phi\Xi_{\alpha}^{s}$ sends $X_{\alpha}$ to a subcategory of $X_{\alpha}^{s}$. Such that,

$$
\begin{align*}
\pi_{\beta} \Phi \circ \Xi_{\alpha}^{s} \pi_{\alpha} \circ \Phi^{-1} \Xi_{\beta}^{\Phi(s)} |_{Y_{\beta}^{\alpha}}
&= \pi_{\beta} \Phi \circ \underbrace{\Xi_{\alpha}^{s} \pi_{\alpha}}_{=\mathrm{id}_{X_{\alpha}^{s}}} \circ \underbrace{\Phi^{-1} \Xi_{\beta}^{\Phi(s)} |_{Y_{\beta}^{\alpha}}}_{\text{maps to } X_{\alpha}^{s}} \\
&= \pi_{\beta} \circ \Phi \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} |_{Y_{\beta}^{\alpha}} \\
&= \pi_{\beta} \Xi_{\beta}^{\Phi(s)} |_{Y_{\beta}^{\alpha}}
\end{align*}
$$
$$ \pi_{\beta}\Phi \circ \Xi_{\alpha}^{s}\pi_{\alpha} \circ \Phi^{-1}\Xi_{\beta}^{\Phi(s)}|_{Y_{\beta}^{\alpha}} = \mathrm{id}_{Y_{\beta}^{\alpha}} $$

Corollary 12

$$ \text{Similarly, } \pi_{\alpha}\Phi^{-1}\Xi_{\beta}^{\Phi(s)} \circ \pi_{\beta}\Phi\Xi_{\alpha}^{s}|_{X_{\alpha}^{\beta}} = \mathrm{id}_{X_{\alpha}^{\beta}} $$

□

With this we have all we need to build the isomorphism $\Psi_1 = (b_\beta)_{\beta \in B} : \prod_{\beta \in B} Y_\beta \to \prod_{\alpha \in A, \beta \in B} X_\alpha^\beta$ and $\Psi_2 = (a_\alpha)_{\alpha \in A} : \prod_{\alpha \in A} X_\alpha \to \prod_{\alpha \in A, \beta \in B} X_\alpha^\beta$ from ??, i.e. all the morphisms in Diagram 2 are isomorphisms.

**Proposition 16.** With the previous notations and with

$$ \Psi_1 = \left( \prod_{\beta \in B} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \qquad \Psi_2 = \prod_{\alpha \in A} \left( \prod_{\beta \in B} \left( \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi \circ \Xi_{\alpha}^{s} \right) $$

$\Psi \circ \Phi$ and $\Psi_2$ are isomorphisms of connected loop-free categories. Furthermore, for all $\alpha \in A$, $\beta \in B$, $\pi_\beta \Psi_1$ and $\pi_\alpha \Psi_2$ are isomorphisms.

*Proof.* • $\Psi_1$ is an isomorphism. Indeed, by Corollary 12 $\Xi_{\beta}^{\Phi(s)} : Y_{\beta} \to Y_{\beta}^{\Phi(s)}$ is an isomorphism. By 14, so is $\Phi^{-1} : Y_{\beta}^{\Phi(s)} \to \prod_{\alpha \in A} X_{\alpha}^{\beta}$. Thus, as products of isomorphism, all arrows in the following diagram are isomorphisms.

$$ \prod_{\beta \in B} Y_{\beta} \xrightarrow{\prod_{\beta \in B} \Xi_{\beta}^{\Phi(s)}} \prod_{\beta \in B} Y_{\beta}^{\Phi(s)} \xrightarrow{\prod_{\beta \in B} \Phi^{-1}} \prod_{\beta \in B} \prod_{\alpha \in A} X_{\alpha}^{\beta} $$

• Let us prove that $\Psi_2$ is an isomorphism. Indeed, by Corollary 12, resp. Proposition 14 resp. 15, the following functors are all isomorphisms:

$$ X_{\alpha} \xrightarrow{\Xi_{\alpha}^{s}} X_{\alpha}^{s} \xrightarrow{\Phi} \prod_{\beta \in B} Y_{\beta} \xrightarrow{\prod_{\beta \in B} \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)}} \prod_{\beta \in B} X_{\alpha}^{\beta} $$

It follows that $\Psi_2 = \prod_{\lambda \in A} \left( \prod_{\beta \in B} \left( \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi \circ \Xi_{\alpha}^{s} \right)$ is an isomorphism by composition and product of isomorphisms. Furthermore, each $\pi_\alpha \Psi_2$ is an isomorphism

□

Now let us prove the commutativity of the Diagram 3.

**Proposition 17.** Let $\mu \in B$, $f \in \prod_{\alpha \in A} X_{\alpha}^{\mu} = \prod_{\alpha \in A} \pi_{\alpha} \Phi^{-1}[Y_{\mu}^{\Phi(s)}]$, with $\Psi_1$ and $\Psi_2$ as defined in Proposition 16. Then for all $\beta \in B$ and $\alpha \in A$

$$ \pi_{\beta}\pi_{\alpha}(\gamma^{-1} \circ \Psi_{1} \circ \Phi)(f) = \pi_{\beta}\pi_{\alpha}\Psi_{2}(f) = \begin{cases} f_{\alpha} & \text{if } \beta = \mu \\ s_{\alpha} & \text{otherwise} \end{cases} $$
Proof. By definition of $\gamma$, the equality of Proposition 17 above is equivalent to

$$ (\Psi_1 \circ \Phi(f)_\beta)_\alpha = ((\gamma \circ \Psi_2(f))_\beta)_\alpha = \begin{cases} f_\alpha & \text{if } \beta = \mu \\ s_\alpha & \text{otherwise} \end{cases} $$

Let $f = (f_\alpha)_{\alpha \in A} \in \prod_{\lambda \in A} X_\lambda^\mu$. By Proposition 14, $\Phi(f) \in Y_\mu^{\Phi(s)}$ with $\Phi(f) = (\Phi(id_s), \Phi(f)_\mu, \mu)$ and $\Phi(f)_\mu \in Y_\mu$.

$$ \bullet \text{ For } \Psi_1 \circ \Phi = \prod_{\beta \in B} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \circ \pi_{\beta} \Phi $$

$$ \begin{aligned} \pi_{\beta} \Psi_{1} \circ \Phi(f) &= \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \circ \Phi(f)_{\beta} \\ &= \Phi^{-1}(\mathrm{id}_{\Phi(s)}, \Phi(f)_{\beta}, \beta) \qquad \text{Definition 7} \\ &= \Phi^{-1}(\mathrm{id}_{\Phi(s)}, (\mathrm{id}_{\Phi(s)}, \Phi(f)_{\mu}, \mu)_{\beta}, \beta) \end{aligned} $$

$$ \pi_{\beta} \Psi_{1} \circ \Phi(f) = \begin{cases} \Phi^{-1}(\mathrm{id}_{\Phi(s)}) = \mathrm{id}_{s} & \text{if } \mu \neq \beta \\ \Phi^{-1}(\mathrm{id}_{\Phi(s)}, \Phi(f)_{\mu}, \mu) = f & \text{if } \mu = \beta \end{cases} $$

$$ \bullet \text{ For } \gamma \circ \Psi_2 = \prod_{\alpha \in A} \left( \prod_{\beta \in B} \pi_{\alpha} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) (\Phi \circ \Xi_{\alpha}^{s}) $$

$$ - \beta \neq \mu. $$

By definition, $id_s = \Phi^{-1}\Phi(id_s) \in \Phi^{-1}[Y_\mu^{\Phi(s)}] = \prod_{\alpha \in A} X_\alpha^\mu$, such that for all $\alpha \in A$, $\Xi_\alpha^s f_\alpha \in \prod_{\alpha \in A} X_\alpha^\mu$ i.e. $\Phi \circ \Xi_\alpha^s(f_\alpha) \in Y_\mu^{\Phi(s)}$ and thus for all $\beta \neq \mu$, $\pi_\beta \Phi \circ \Xi_\alpha^s(f_\alpha) = \Phi(id_s)_\beta$.

Thus, for all $\beta \neq \mu$

$$ \begin{aligned} \pi_{\alpha} \pi_{\beta} \circ \gamma \circ \Psi_{2}(f) &= \pi_{\alpha} \Phi^{-1} \Xi_{\beta}^{\Phi(s)} \left( \pi_{\beta} \Phi \circ \Xi_{\alpha}^{s} (f_{\alpha}) \right) \\ &= \pi_{\alpha} \Phi^{-1} \Xi_{\beta}^{\Phi(s)} (\Phi(id_{s})_{\beta}) \\ \pi_{\alpha} \pi_{\beta} \circ \gamma \circ \Psi_{2}(f) &= \pi_{\alpha} id_{s} \end{aligned} $$

$$ - \mu = \beta. \text{ Then, } f \in \prod_{\lambda \in A} X_{\lambda}^{\mu} \text{ therefore } \Phi(f) = (\Phi(id_{s}), \Phi(f)_{\beta}, \beta). \text{ It follows that} $$

$$ \forall g_{\beta} \in Y_{\beta}, (\Phi(f), g_{\beta}, \beta) = (\Phi(id_{s}), g_{\beta}, \beta) \qquad (10) $$

Furthermore $\pi_\alpha \Phi^{-1} \Phi(f) = \pi_\alpha \Phi^{-1} \Phi(id_s, f_\alpha, \alpha) = f_\alpha$. Hence,

$$ \begin{aligned} f_{\alpha} &= \pi_{\alpha} \Phi^{-1}(\Phi(f), (\Phi(id_{s}, f_{\alpha}, \alpha))_{\beta}, \beta) && \text{By Corollary 9} \\ &= \pi_{\alpha} \Phi^{-1}(\Phi(id_{s}), (\Phi(id_{s}, f_{\alpha}, \alpha))_{\beta}, \beta) && \text{By Eq. (10)} \end{aligned} $$

$$ f_{\alpha} = \pi_{\alpha} \pi_{\beta} \gamma \circ \Psi_{2}(f) \qquad \text{By definition of } \Psi_{2} $$

□
Now that commutativity of Diagram 3 is proven, we extend the commutativity along one of the $\lambda \in A$, thus proving the commutativity of the Diagram 2. First as explained in the outline, we will to prove the faithfulness of the restriction, which is less trivial in our case.

**Lemma 18.** With the previous notation, $\gamma: \prod_{\beta \in B} \prod_{\alpha \in A} X_{\alpha}^{\beta} \to \prod_{\alpha \in A} \prod_{\beta \in B} X_{\alpha}^{\beta}$ the natural isomorphism and with $\tilde{s}_{\lambda}$ the singleton category for a given $\lambda \in A$, the following restrictions are faithful functors.

$$ \begin{array}{ccc} \pi_{\lambda}\gamma^{-1}\Psi_1 \circ \Phi|_{X_{\lambda}^s} & \pi_{\{\alpha \in A | \alpha \neq \lambda\}}\gamma^{-1}\Psi_1 \circ \Phi|_{\prod_{\alpha \neq \lambda} X_{\alpha} \times \tilde{s}_{\lambda}} & \pi_{\lambda}\Psi_2|_{X_{\lambda}^s} \end{array} $$

$$ \textit{Proof.} \bullet \Psi_1 \circ \Phi = \left( \prod_{\beta \in B} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi $$

Let $f = (f_{\alpha})_{\alpha \in A} \in X_{\lambda}^{s}$, then $\pi_{\alpha}f = \pi_{\alpha}\mathrm{id}_{s}$ for all $\alpha \neq \lambda$. Thus, by Corollary 9, for all $\beta \in B$ and all $\alpha \neq \lambda$,

$$ \pi_{\alpha}\Phi^{-1}(\Phi(\mathrm{id}_{s}), \Phi(f)_{\beta}, \beta) = \pi_{\alpha}\mathrm{id}_{s} $$

i.e. $\pi_{\alpha}\pi_{\beta}\Psi_1 \circ \Phi(f) = \pi_{\alpha}\mathrm{id}_{s}$. Thus

$$ \begin{aligned} \Psi_1(f) \circ \Phi &= (\mathrm{id}_s, (\pi_{\beta}\Psi_1(f))_{\lambda}, \lambda)_{\beta \in B} \\ &= (\Xi_{\lambda}^s(\pi_{\lambda}\pi_{\beta}\Psi_1(f)))_{\beta \in B} \\ &= \left(\prod_{\beta \in B} \Xi_{\lambda}^s\right) (\pi_{\lambda}\pi_{\beta}\Psi_1(f))_{\beta \in B} \\ \Psi_1 \circ \Phi(f) &= \left(\prod_{\beta \in B} \Xi_{\lambda}^s\right) \circ (\pi_{\lambda}\gamma^{-1}\Psi_1 \circ \Phi)(f) \end{aligned} $$

This is true for all $f \in X_{\lambda}^{s}$, thus:

$$ \Psi_1 \circ \Phi|_{X_{\lambda}^s} = \left( \prod_{\beta \in B} \Xi_{\lambda}^s \right) \circ \left( \pi_{\lambda}\gamma^{-1}\Psi_1 \circ \Phi \right)|_{X_{\lambda}^s} $$

By faithfulness of $\Psi_1 \circ \Phi$ (Proposition 16) and $\Xi_{\lambda}^s$ (Lemma 11), this implies $\pi_{\lambda}\gamma^{-1}\Psi_1 \circ \Phi|_{X_{\lambda}^s}$ faithful.

Now let $f \in (f_{\alpha})_{\alpha \in A} \in \prod_{\alpha \neq \lambda} X_{\alpha} \times \tilde{s}_{\lambda}$, then $\pi_{\lambda}f = \pi_{\lambda}\mathrm{id}_{s}$. By Corollary 9, this implies for all $\beta \in B$

$$ \pi_{\lambda}\Phi^{-1}(\Phi(\mathrm{id}_{s}), \Phi(f)_{\beta}, \beta) = \pi_{\lambda}\mathrm{id}_{s} $$

i.e. $\pi_{\lambda}\pi_{\beta}\Psi_1 \circ \Phi(f) = \pi_{\lambda}\mathrm{id}_{s}$ such that

$$ \begin{aligned} \Psi_1 \circ \Phi(f) &= (\pi_{\beta}\Psi_1 \circ \Phi(f), \mathrm{id}_{s_{\lambda}}, \lambda)_{\beta \in B} \\ &= ((\pi_{\alpha}\pi_{\beta}\Psi_1 \circ \Phi(f))_{\alpha \in A}, \mathrm{id}_{s_{\lambda}}, \lambda)_{\beta \in B} \end{aligned} \qquad \textit{Corollary 9} $$
$$ \Psi_1 \circ \Phi(f) = ((\pi_\beta \pi_\alpha \gamma^{-1} \Psi_1 \circ \Phi(f))_{\alpha \in A}, \mathrm{id}_{s_\lambda}, \lambda)_{\beta \in B} $$

Faithfulness of $\Psi_1 \circ \Phi$ then implies the faithfulness of $((\pi_\beta \pi_\alpha \gamma^{-1} \Psi_1 \circ \Phi(\cdot))_{\alpha \neq \lambda})_{\beta \in B}$, i.e. the faithfulness of $\pi_{\alpha \neq \lambda} \gamma^{-1} \Psi_1 \circ \Phi$ on the subcategory $\prod_{\alpha \neq \lambda} X_\alpha \times \tilde{s}_\lambda$

$$ \Psi_2 = \prod_{\alpha \in A} \left( \prod_{\beta \in B} \left( \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi \circ \Xi_{\alpha}^{s} \right) $$

By Proposition 16, each $\pi_\alpha \Psi_2$ is an isomorphism, thus a fortiori, the restriction $\pi_\alpha \Psi_2|_{X_\alpha^s}$ is faithful. Hence, $\pi_{\{\alpha \in A | \alpha \neq \lambda\}} \Psi_2|_{\prod_{\alpha \neq \lambda} X_\alpha \times \tilde{s}_\lambda}$ is faithful as a product of faithful functors. □

**Proposition 19.** With the previous notation, $\Psi_1 \circ \Phi = \gamma \circ \Psi_2$

*Proof.* Let $\Psi \in \{\Psi_2, \gamma^{-1} \circ \Psi_1 \circ \Phi\}$ and $\mu \in B$. Let $f_\lambda^\mu \in X_\lambda^\mu$. By Proposition 17, $\Psi_2$ and $\gamma^{-1} \circ \Psi_1 \circ \Phi$ are equal when we restrict to $\prod_{\alpha \in A} X_\alpha^\mu$. As explained above, we wish to extend this equality to the full domain. Proposition 17 also implies that for all $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$, $\pi_\lambda \Psi(g^\mu, f_\lambda^\mu, \lambda) = \pi_\lambda \Psi(s, f_\lambda^\mu, \lambda)$. Thus, by Lemma 10, for all $f_\lambda \in X_\lambda$, for all $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$

$$ \pi_{\lambda} \Psi(g^{\mu}, f_{\lambda}, \lambda) = \pi_{\lambda} \Psi(s, f_{\lambda}, \lambda) = \pi_{\lambda} \Psi \Xi_{\lambda}^{s}(f_{\lambda}) \stackrel{\text{def}}{=} \Psi_{\lambda}(f_{\lambda}) \quad (11) $$

We want to prove that for all $\lambda \in A$, $\mu \in B$, $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$, $f_\lambda \in X_\lambda$, the projection on any $\alpha \neq \lambda$ of $\Psi(g^\mu, f_\lambda, \alpha)$ depends only on $g^\mu$, i.e.

$$ (g^{\mu}, f_{\lambda}, \lambda) = \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) $$

$$ \bullet \text{ For } \alpha \neq \lambda, \pi_{\alpha} \Psi^{-1} \Psi(g^{\mu}, f_{\lambda}, \lambda) = g_{\alpha}^{\mu} = \pi_{\alpha} \Psi^{-1} \Psi(g^{\mu}). \text{ Thus, by Corollary 9,} $$

$$ \pi_{\alpha} \Psi^{-1}(\Psi(g^{\mu}), \Psi(g^{\mu}, f_{\lambda}, \lambda)_{\lambda}, \lambda) = g_{\alpha}^{\mu} $$

By definition of $\Psi_\lambda(f_\lambda)$ (Eq. (11))

$$ \pi_{\alpha} \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) = g_{\alpha}^{\mu} \quad (12) $$

$$ \bullet \text{ For } \lambda, \text{ By Eq. (12), } \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) \in (X_{\alpha}^{\mu}, X_{\lambda}, \lambda), \text{ such that by Eq. (11)} $$

$$ \begin{aligned} \pi_{\lambda} \Psi \Xi_{\lambda}^{s} (\pi_{\lambda} \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda)) &= \pi_{\lambda} \Psi \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) \\ &= \Psi_{\lambda}(f_{\lambda}) \\ \pi_{\lambda} \Psi \Xi_{\lambda}^{s} (\pi_{\lambda} \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda)) &= \pi_{\lambda} \Psi \Xi_{\lambda}^{s}(f_{\lambda}) \quad \text{Eq. (11)} \end{aligned} $$

By faithfulness of $\pi_\lambda \Psi \Xi_\lambda^s$ (Lemma 18),

$$ \pi_{\lambda} \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) = f_{\lambda} \quad (13) $$
By Eq. (12) and Eq. (13), we have $(g^\mu, f_\lambda, \lambda) = \Psi^{-1}(\Psi(g^\mu), \Psi_\lambda(f_\lambda), \lambda)$ i.e.

$$ \Psi(g^\mu, f_\lambda, \lambda) = (\Psi(g^\mu), \Psi_\lambda(f_\lambda), \lambda) \qquad (14) $$

So far Eq. (14) only holds when $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$. Let us prove that it is in fact valid for all $g \in \prod_{\alpha \in A} X_\alpha$, i.e. for all $\lambda \in A$ and for all $f_\lambda \in X_\lambda$

$$ \Psi(g, f_\lambda, \lambda) = (\Psi(g), \Psi_\lambda(f_\lambda), \lambda) $$

Let $\rho \in A$, $\rho \neq \lambda$. By Eq. (14), for all $f_\lambda \in X_\lambda$, $\pi_\rho \Psi(g^\mu, f_\lambda, \lambda) = \pi_\rho \Psi(g^\mu)$. By Lemma 10 this implies, for all $g \in \prod_{\alpha \in A} X_\alpha$, for all $f_\lambda \in X_\lambda$

$$ \pi_{\bar{\lambda}} \Psi(g, f_{\lambda}, \lambda) = \pi_{\bar{\lambda}} \Psi(g) := \Psi_{\bar{\lambda}}(g) \qquad (15) $$

where $\pi_{\bar{\lambda}}$ is the projection on $A \setminus \{\lambda\}$.

Thus, proving $\Psi(g, f_\lambda, \lambda) = (\Psi(g), \Psi_\lambda(f_\lambda), \lambda)$ is equivalent to proving,

$$ (\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) = \Psi(g, f_\lambda, \lambda) $$

i.e.

$$ \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) = (g, f_\lambda, \lambda) $$

Let us look at the different projections

* On $X_\lambda$.

$$ \pi_\lambda \Psi^{-1}(\Psi(g, f_\lambda, \lambda)) = \pi_\lambda \Psi^{-1}(\Psi \Xi_\lambda^s(f_\lambda)) = f_\lambda \text{ implies by Corollary 9} $$

$$ \pi_\lambda \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \pi_\lambda \Psi \Xi_\lambda^s(f_\lambda), \lambda) = f_\lambda $$

$$ \pi_\lambda \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) = f_\lambda \quad \text{Eq. (11)} $$

* On $\prod \alpha \neq \lambda X_\alpha$

By Eq. (15), for all $h \in \prod_{\alpha \in A} X_\alpha$, $\pi_{\bar{\lambda}} \Psi(h, \mathrm{id}_{s_\lambda}, \lambda) = \pi_{\bar{\lambda}} \Psi(h)$. Applying this to the element $h = \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda)$ we get

$$ \begin{aligned} \pi_{\bar{\lambda}} \Psi(\Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda), \mathrm{id}_{s_\lambda}, \lambda) &= \pi_{\bar{\lambda}} \Psi \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) \\ &= \pi_{\bar{\lambda}}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) \\ &= \pi_{\bar{\lambda}} \Psi(g, f_\lambda, \lambda) \end{aligned} $$

$$ \pi_{\bar{\lambda}} \Psi(\Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda), \mathrm{id}_{s_\lambda}, \lambda) = \pi_{\bar{\lambda}} \Psi(g, \mathrm{id}_{s_\lambda}, \lambda) \qquad \text{Eq. (15)} $$

By faithfulness of $\pi_{\bar{\lambda}} \Psi|_{(\prod_{\alpha \in A} X_\alpha, \mathrm{id}_{s_\lambda}, \lambda)}$ (Lemma 18),

$$ (\Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda), \mathrm{id}_{s_\lambda}, \lambda) = (g, \mathrm{id}_{s_\lambda}, \lambda) $$

$$ \pi_{\bar{\lambda}} \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda)) = \pi_{\bar{\lambda}} g $$
Thus $\Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) = (g, f_\lambda, \lambda)$ and as such, for all $f_\lambda \in \lambda$, for all $g \in \prod_{\alpha \in A} X_\alpha$,

$$ \Psi(g, f_\lambda, \lambda) = (\Psi(g), \Psi_\lambda(f_\lambda), \lambda) $$

As this is true for any $f, g \in \prod_{\alpha \in A} X_\alpha$, and any $\lambda$, we get

$$ \Psi(f) = (\Psi_\alpha(f_\alpha))_{\alpha \in A} $$

All that is left to do is to prove that $\Psi_\alpha(f_\alpha)$ is the same whether $\Psi = \Psi_2$ or $\Psi = \gamma^{-1} \circ \Psi_1 \circ \Phi$. By Eq. (11)

$$ \Psi_\lambda(f_\lambda) = \pi_\lambda \Psi \Xi_\lambda^s(f_\lambda) $$

But, by definition

$$ \pi_\beta \pi_\lambda \Psi_2(\Xi_\lambda^s f_\lambda) = \pi_\beta \pi_\lambda (\Phi^{-1} \circ \Xi_\beta^{\Phi(s)} \circ \pi_\beta \circ \Phi \circ \Xi_\lambda^s)(\pi_\lambda(\Xi_\lambda^s f_\lambda)) $$

$$ = \pi_\beta \pi_\lambda (\Phi^{-1} \circ \Xi_\beta^{\Phi(s)} \circ \pi_\beta \circ \Phi \circ \Xi_\lambda^s)(f_\lambda) \qquad \text{Lemma 11} $$

$$ = \pi_\beta \pi_\lambda (\Phi^{-1} \Xi_\beta^{\Phi(s)})(\pi_\beta \Phi)(\Xi_\lambda^s f_\lambda) $$

$$ \pi_\beta \pi_\lambda \Psi_2(\Xi_\lambda^s f_\lambda) = \pi_\beta \pi_\lambda \gamma^{-1} \circ \Psi_1 \circ \Phi(\Xi_\lambda^s f_\lambda) \qquad \text{by Definition of } \Psi_1 $$

This is true for all $\lambda$ and $\beta$, thus $\Psi_2 = \gamma^{-1} \circ \Psi_1 \circ \Phi$

<figure><img src="image_13.png" /></figure>

This concludes the proof of the commutativity of the diagram in Theorem A.

## References

[1] Schröder, B.S.W.: Ordered sets. Springer 29, 30 (2003)

[2] Hashimoto, J.: On direct product decomposition of partially ordered sets. Annals of Mathematics, 315–318 (1951)

[3] Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages: NATO Advanced Study Institute. proceedings of the summer school held at Villars-de-Lans, 1966, pp. 43–112. Academic Press, ??? (1968). Reprint of the eponymous technical report published in september 1965 by the Technological University of Eindhoven, The Netherlands. Also in Hansen, P. B., editor, *The Origin of Concurrent Programming*, Springer 2002.

[4] Haucourt, E.: The geometry of conservative programs. Mathematical Structures in Computer Science 28(10), 1723–1769 (2018) https://doi.org/10.1017/S0960129517000226
[5] Fajstrup, L., Goubault, É., Haucourt, E., Mimram, S., Raussen, M.: Directed Algebraic Topology and Concurrency. Springer, ??? (2016). https://doi.org/10.1007/978-3-319-15398-8

[6] Haucourt, E.: Categories of components and loop-free categories. Theory and Applications of Categories 16(27), 736–770 (2006)