6 Many-sorted discretization transformations
Every many-sorted \(n\)-category can be embedded into a higher-dimensional \(m\)-category by extending the family of sets with copies of the top-level set: dimensions above \(n\) are filled with the \(n\)-morphism set, and the extra operations are declared trivial. This construction extends naturally to the \(\omega \)-categorical setting. Moreover, any many-sorted \(n\)-functor automatically preserves this extended structure, giving rise to a functor between the resulting higher-dimensional categories, with the extra dimensions acted upon by the top-level component of the original functor. We call this process the discretization transformation, and we show that it is functorial and that discretization transformations at different dimensions commute with one another.
6.1 Discrete many-sorted categories
We begin by defining the extended family of sets and then construct a many-sorted category structure on it.
Let \(\mathsf{C}\) be a many-sorted \(n\)-category on a family \((C_k)_{k \leq n}\), and let \(m \in \mathbb {N}\) with \(n {\lt} m\). The discrete finite family \((C^{{\gt}m}_k)_{k \leq m}\) is defined by
Let \(\mathsf{C}\) be a many-sorted \(n\)-category on a family \((C_k)_{k \leq n}\), and let \(m \in \mathbb {N}\) with \(n {\lt} m\). The discrete \(m\)-category of \(\mathsf{C}\) is the many-sorted \(m\)-category \(\mathsf{C}^{{\gt}m}\) on the discrete family \((C^{{\gt}m}_k)_{k \leq m}\) of Definition 6.1, where the operations at each pair \((k, j)\) with \(j {\lt} k\) are defined as follows:
If \(k \leq n\) (and hence \(j {\lt} k \leq n\)): the source \(\operatorname{sc}^{(k,j)}\), target \(\operatorname{tg}^{(k,j)}\), identity \(\operatorname{i}^{(k,j)}\), and composition \(\circ ^{(k,j)}\) are those of \(\mathsf{C}\).
If \(k {\gt} n\) and \(j \leq n\): we have \(C^{{\gt}m}_k = C_n\) and \(C^{{\gt}m}_j = C_j\), so the source and target maps \(\operatorname{sc}^{(k,j)}, \operatorname{tg}^{(k,j)} \colon C_n \to C_j\) are defined as \(\operatorname{sc}^{(n,j)}\) and \(\operatorname{tg}^{(n,j)}\) respectively; the identity map \(\operatorname{i}^{(k,j)} \colon C_j \to C_n\) is defined as \(\operatorname{i}^{(n,j)}\); and composition \(\circ ^{(k,j)}\) is defined as \(\circ ^{(n,j)}\).
If \(j {\gt} n\) (and hence \(k {\gt} j {\gt} n\)): we have \(C^{{\gt}m}_k = C^{{\gt}m}_j = C_n\). The source and target maps are the identity on \(C_n\), the identity map \(\operatorname{i}^{(k,j)}\) is also the identity, and composition is defined only between equal morphisms and returns the morphism itself.
Each axiom, whether a pre-category axiom at a pair \((k, j)\) or a cross-dimensional axiom at a triple \(i {\lt} j {\lt} k\), either involves only indices at most \(n\), in which case it reduces to the corresponding axiom of \(\mathsf{C}\); involves indices above \(n\) whose operations coincide with those at the top dimension \(n\), in which case it again follows from an axiom of \(\mathsf{C}\); or involves only indices above \(n\), where all operations are trivial and the axiom holds immediately.
Let \(\mathsf{C}\) be a many-sorted \(n\)-category on a family \((C_k)_{k \leq n}\). The discrete omega family \((C^{{\gt}\omega }_k)_{k \in \mathbb {N}}\) is defined by
Let \(\mathsf{C}\) be a many-sorted \(n\)-category on a family \((C_k)_{k \leq n}\). The discrete \(\omega \)-category of \(\mathsf{C}\) is the many-sorted \(\omega \)-category \(\mathsf{C}^{{\gt}\omega }\) on the discrete omega family \((C^{{\gt}\omega }_k)_{k \in \mathbb {N}}\) of Definition 6.3, defined by the same case distinction as in Definition 6.2, now with the indices \(k\) and \(j\) ranging over all of \(\mathbb {N}\).
The many-sorted category axioms follow by the same argument as in Definition 6.2.
6.2 Discrete many-sorted functors
Let \(\mathsf{C}\) and \(\mathsf{D}\) be many-sorted \(n\)-categories, and let \(F = (F_k)_{k \leq n} \colon \mathsf{C} \to \mathsf{D}\) be a many-sorted \(n\)-functor. For any \(m \in \mathbb {N}\) with \(n {\lt} m\), the family \((F^{{\gt}m}_k)_{k \leq m}\) defined by
is a many-sorted \(m\)-functor \(F^{{\gt}m} \colon \mathsf{C}^{{\gt}m} \to \mathsf{D}^{{\gt}m}\).
Each preservation axiom at a pair \((k, j)\) with \(j {\lt} k\) either involves only indices at most \(n\), where it follows from the functor axioms of \(F\); involves indices above \(n\) whose maps and operations coincide with those at the top dimension \(n\), where it again follows from a functor axiom of \(F\); or involves only indices above \(n\), where all maps coincide and all operations are trivial, so the axiom holds immediately.
Let \(\mathsf{C}\) and \(\mathsf{D}\) be many-sorted \(n\)-categories, and let \(F = (F_k)_{k \leq n} \colon \mathsf{C} \to \mathsf{D}\) be a many-sorted \(n\)-functor. The family \((F^{{\gt}\omega }_k)_{k \in \mathbb {N}}\) defined by
is a many-sorted \(\omega \)-functor \(F^{{\gt}\omega } \colon \mathsf{C}^{{\gt}\omega } \to \mathsf{D}^{{\gt}\omega }\).
The argument is identical to that of Definition 6.5.
6.3 Many-sorted discretization functors
The discrete constructions of the previous sections are in fact functorial, as the following definition makes precise.
Let \(n, m \in \overline{\mathbb {N}}\) with \(n \leq m\). The many-sorted discretization functor \(\operatorname{\mathcal{D}}_{\mathrm{ms}}^{(n, m)}\) from \(n\mathsf{Cat}_{\mathrm{ms}}\) to \(m\mathsf{Cat}_{\mathrm{ms}}\) is the functor that maps every many-sorted \(n\)-category \(\mathsf{C}\) to its discrete \(m\)-category \(\mathsf{C}^{{\gt}m}\) and every many-sorted \(n\)-functor \(F \colon \mathsf{C} \to \mathsf{D}\) to its discrete \(m\)-functor \(F^{{\gt}m} \colon \mathsf{C}^{{\gt}m} \to \mathsf{D}^{{\gt}m}\). If \(n = m\), then \(\operatorname{\mathcal{D}}_{\mathrm{ms}}^{(n, n)}\) stands for the identity functor on \(n\mathsf{Cat}_{\mathrm{ms}}\).
Functoriality follows from the fact that the discrete constructions preserve the underlying maps: the identity functor on \(\mathsf{C}\) yields the identity functor on \(\mathsf{C}^{{\gt}m}\), and the composition of two \(n\)-functors yields the composition of their discrete \(m\)-functors.