Underlying transformations

In this chapter, for any two naturals \(n\) and \(m\) with \(m {\lt} n\), we provide a way to transform single-sorted \(n\)-categories (or \(\omega \)-categories) into single-sorted \(m\)-categories by forgetting morphisms that are not \(m\)-cells in the original category.

Similarly, we provide a way to transform single-sorted \(n\)-functors (or \(\omega \)-functors) into single-sorted \(m\)-functors by forgetting the action on morphisms that are not \(m\)-cells in the original category.

We conclude the chapter by showing that these transformations are functorial, i.e., they define a functor from \(n\mathsf{Cat}\) (or \(\omega \mathsf{Cat}\)) to \(m\mathsf{Cat}\).

Underlying single-sorted categories

Lemma .1

def:cell HigherCategoryTheory.SingleSorted.underlying_source_is_cell Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f \in \mathsf{C}\) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), we have that \(\Sc ^k (f)\) is a \(m\)-cell in \(\mathsf{C}\).

▼

Applying one of the axioms of single-sorted categories, we have that

\[ \Sc ^m (\Sc ^k f) = \Sc ^k (f). \]

▼

Lemma .2

thm:cell_sc_iff_cell_tg HigherCategoryTheory.SingleSorted.underlying_target_is_cell Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f \in \mathsf{C}\) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), we have that \(\Tg ^k (f)\) is a \(m\)-cell in \(\mathsf{C}\).

▼

Applying one of the axioms of single-sorted categories, we have that

\[ \Tg ^m (\Tg ^k f) = \Tg ^k (f). \]

That is, \(\Tg ^k (f)\) is a target-based \(m\)-cell in \(\mathsf{C}\). However, we know that every target-based \(m\)-cell is also a \(m\)-cell.

▼

Lemma .3

def:cell HigherCategoryTheory.SingleSorted.underlying_comp_is_cell Let \(\mathsf{C}\) be a single-sorted \(\mathcal{I}\)-category and \(m \in \mathcal{I}\). Then, for every \(f, g \in C_m\) (i.e., \(f\) and \(g\) are \(m\)-cells in \(\mathsf{C}\)) and every \(k \in \mathcal{I}\) such that \(k {\lt} m\), if the comoposition \(g \Pcomp ^k f\) is defined, then \(g \Pcomp ^k f\) is a \(m\)-cell in \(\mathsf{C}\).

▼

Applying one of the axioms of single-sorted categories and the fact that \(f\) and \(g\) are \(m\)-cells, we have that

\[ \Sc ^m (g \Pcomp ^k f) = \Sc ^m (g) \Pcomp ^k \Sc ^m (f) = g \Pcomp ^k f. \]

▼

Definition .4 Underlying single-sorted category

lem:underlying_source_is_cell, lem:underlying_target_is_cell, lem:underlying_comp_is_cell, HigherCategoryTheory.SingleSorted.NCategory.underlying, HigherCategoryTheory.SingleSorted.OmegaCategory.underlying Let \(\mathsf{C}\) be a single-sorted \(n\)-category (or \(\omega \)-category) and \(m\) be a natural number such that \(m {\lt} n\) ¹ . We define the underlying single-sorted \(m\)-category of \(\mathsf{C}\) as the single-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) defined on the set of \(m\)-cells of \(\mathsf{C}\), \(C_m\), with the source, target, and composition operations of \(\mathsf{C}\) restricted to \(C_m\).

Note that, by Lemmas .1, .2, and .3, these operations are well-defined. Also, the axioms of single-sorted categories for \(\mathsf{C}_m\) follow directly from the corresponding axioms for \(\mathsf{C}\).

Underlying single-sorted functors

Lemma .5

def:cell, def:SingleSortedFunctor HigherCategoryTheory.SingleSorted.underlying_functor_is_cell Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(\mathcal{I}\)-categories, \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted functor, and \(m \in \mathcal{I}\). Then, for every \(f \in C_m\) we have that \(F(f) \in D_m\), i.e., the image of \(m\)-cells under a single-sorted functor are \(m\)-cells.

▼

Applying one of the axioms of single-sorted functors and the fact that \(f\) is a \(m\)-cell, we have that

\[ \Sc ^m (F(f)) = F(\Sc ^m (f)) = F(f). \]

▼

Definition .6 Underlying single-sorted functor

lem:underlying_functor_is_cell HigherCategoryTheory.SingleSorted.NFunctor.underlying, HigherCategoryTheory.SingleSorted.OmegaFunctor.underlying Let \(\mathsf{C}\) and \(\mathsf{D}\) be single-sorted \(n\)-categories (or \(\omega \)-categories), \(F \colon \mathsf{C} \to \mathsf{D}\) be a single-sorted \(n\)-functor (or \(\omega \)-functor), and \(m {\lt} n\) ² . We define the underlying single-sorted \(m\)-functor of \(F\) as the single-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\) defined as the restriction of \(F\) to the sets of \(m\)-cells \(C_m\) and \(D_m\).

Note that, by Lemma .5, this function is well-defined. Also, the axioms of single-sorted functors for \(F_m\) follow directly from the corresponding axioms for \(F\).

Functoriality of the underlying transformations

For any two naturals \(n\) and \(m\) with \(m \leq n\), we first note that the underlying transformations defined in Definitions .4 and .6 are in fact functorial transformations from \(n\mathsf{Cat}\) to \(m\mathsf{Cat}\).

Definition .7 Underlying functor

def:SingleSortedCategory_underlying, def:SingleSortedFunctor_underlying, HigherCategoryTheory.SingleSorted.UnderlyingFunctor Let \(n\) and \(m\) be naturals such that \(m \le n\). We define the underlying functor \(\Underlying ^{(n, m)} \colon n\mathsf{Cat}\to m\mathsf{Cat}\) as the functor that maps every single-sorted \(n\)-category \(\mathsf{C}\) to its underlying single-sorted \(m\)-category \(\mathsf{C}^{{\lt}m}\) (as defined in Definition .4) and every single-sorted \(n\)-functor \(F \colon \mathsf{C} \to \mathsf{D}\) to its underlying single-sorted \(m\)-functor \(F^{{\lt}m} \colon \mathsf{C}^{{\lt}m} \to \mathsf{D}^{{\lt}m}\) (as defined in Definition .6).