arXiv reader

Foundations of Algebraic Theories and Higher Dimensional Categories

Soichiro Fujii

arXiv
1903.07030v1 · PDF · 17 March 2019
Categories
math.CT
Licence
CC BY 4.0 The site shows the text.

Abstract

Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or abstract clones. The ubiquity of algebraic structures in mathematics and related fields has given rise to several variants of universal algebra, such as symmetric operads, non-symmetric operads, generalised operads, and monads. These variants of universal algebra are called notions of algebraic theory. In the first part of this thesis, we develop a unified framework for notions of algebraic theory which includes all of the above examples. Our key observation is that each notion of algebraic theory can be identified with a monoidal category, in such a way that theories correspond to monoid objects therein. We introduce a categorical structure called metamodel, which underlies the definition of models of theories. We also consider morphisms between notions of algebraic theory, which are a monoidal version of profunctors. Every strong monoidal functor gives rise to an adjoint pair of such morphisms, and provides a uniform way to establish isomorphisms between categories of models in different notions of algebraic theory. A general structure-semantics adjointness result and a double categorical universal property of categories of models are also shown. In the second part of this thesis, we shift from the general study of algebraic structures, and focus on a particular algebraic structure: higher dimensional categories. Among several existing definitions of higher dimensional categories, we choose to look at the one proposed by Batanin and later refined by Leinster. We show that the notion of extensive category plays a central role in Batanin and Leinster’s definition. Using this, we generalise their definition by allowing enrichment over any locally presentable extensive category.

Items 157

Definition

Definition 1.1

QK1S

A set \mathcal{U} is called a universe if the following hold:

  • if x\in\mathcal{U} and y\in x, then y\in\mathcal{U};

  • if x\in\mathcal{U}, then \{x\}\in\mathcal{U};

  • if x\in\mathcal{U}, then \mathcal{P}(x)=\{y\mid y\subseteq x\}\in\mathcal{U};

  • if I\in\mathcal{U} and (x_i)_{i\in I} is an I-indexed family of elements of \mathcal{U}, then \bigcup_{i\in I} x_i\in\mathcal{U};

  • \mathbb{N}\in\mathcal{U}, where \mathbb{N}=\{0,1,\dots\} and for all n\in\mathbb{N}, n=\{0,1,\dots, n-1\}.

Axiom

Axiom 1.2

WI6P

For each set x, there exists a universe \mathcal{U} such that x\in\mathcal{U}.

Convention

Convention 1.3

A7AW

A set or other mathematical structure (group, category, etc.) is said to be:

  • small if it is in \mathcal{U}_1;

  • large if it is in \mathcal{U}_2;

  • huge if it is in \mathcal{U}_3.

Sets and other mathematical structures are often assumed to be small by default, even when we do not say so explicitly.

A category (or a 2-category) is said to be:

  • locally small if it is large and locally in \mathcal{U}_1;

  • locally large if it is huge and locally in \mathcal{U}_2.

Used by Example 3.14
Definition

Definition 2.1

0CG9
  1. An (\mathbb{N}-)graded set \Gamma is a family \Gamma=(\Gamma_n)_{n\in\mathbb{N}} of sets indexed by natural numbers \mathbb{N}=\{0,1,2,\dots\}. By an element of \Gamma we mean an element of the set \coprod_{n\in\mathbb{N}} \Gamma_n=\{\,(n,\gamma)\mid n\in\mathbb{N}, \gamma\in \Gamma_n\,\}. We write x\in\Gamma if x is an element of \Gamma.

  2. If \Gamma=(\Gamma_n)_{n\in\mathbb{N}} and \Gamma'=(\Gamma'_n)_{n\in\mathbb{N}} are graded sets, then a morphism of graded sets f\colon \Gamma\longrightarrow \Gamma' is a family of functions f=(f_n\colon \Gamma_n\longrightarrow \Gamma'_n)_{n\in\mathbb{N}}.

Definition

Definition 2.2

D1U3

Let \Sigma be a graded set.

  1. A \Sigma-algebra is a set A equipped with, for each n\in\mathbb{N} and \sigma\in\Sigma_n, a function {[\![\sigma]\!]}^A\colon A^n\longrightarrow A called the interpretation of \sigma. We write such a \Sigma-algebra as (A,({[\![\sigma]\!]}^A)_{n\in\mathbb{N},\sigma\in\Sigma_n}) or simply (A,{[\![-]\!]}^A). We often omit the superscript in {[\![-]\!]}^A.

  2. If (A,{[\![-]\!]}^A) and (B,{[\![-]\!]}^{B}) are \Sigma-algebras, then a \Sigma-homomorphism from (A,{[\![-]\!]}^A) to (B,{[\![-]\!]}^{B}) is a function f\colon A\longrightarrow B such that for any n\in\mathbb{N}, \sigma\in\Sigma_n and a_1,\dots,a_n\in A,

    f({[\![\sigma]\!]}^A(a_1,\dots,a_n))={[\![\sigma]\!]}^B(f(a_1),\dots,f(a_n))

    holds (that is, the diagram

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$A^n$}; \node (TR) at (3,2) {$B^n$}; \node (BL) at (0,0) {$A$}; \node (BR) at (3,0) {$B$}; \draw[->] (TL) to node[auto,labelsize](T) {$f^n$} (TR); \draw[->] (TR) to node[auto,labelsize] {${[\![\sigma]\!]}^{B}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {${[\![\sigma]\!]}^A$} (BL); \draw[->] (BL) to node[auto,labelsize](B) {$f$} (BR); \end{tikzpicture}

    commutes).

Definition

Definition 2.3

H8JQ

Let \Sigma be a graded set. The graded set T(\Sigma)=(T(\Sigma)_n)_{n\in\mathbb{N}} of \Sigma-terms is defined inductively as follows.

  1. For each n\in\mathbb{N} and i\in\{1,\dots,n\},

    x_i^{(n)}\in T(\Sigma)_n.

    We sometimes omit the superscript and write x_i for x_i^{(n)}.

  2. For each n,k\in\mathbb{N}, \sigma\in\Sigma_k and t_1,\dots,t_k\in T(\Sigma)_n,

    \sigma(t_1,\dots,t_k)\in T(\Sigma)_n.

    When k=0, we usually omit the parentheses in \sigma() and write instead as \sigma.

Definition

Definition 2.4

EHWQ

Let \Sigma be a graded set and (A,{[\![-]\!]}) be a \Sigma-algebra. We define the interpretation {[\![-]\!]'} of \Sigma-terms recursively as follows.

  1. For each n\in\mathbb{N} and i\in\{1,\dots,n\},

    {[\![x^{(n)}_i]\!]'}\colon A^n\longrightarrow A

    is the i-th projection (a_1,\dots,a_n)\longmapsto a_i.

  2. For each n,k\in\mathbb{N}, \sigma\in\Sigma_k and t_1\dots,t_k\in T(\Sigma)_n,

    {[\![\sigma(t_1,\dots,t_k)]\!]'}\colon A^n\longrightarrow A

    maps (a_1,\dots,a_n)\in A^n to {[\![\sigma]\!]}({[\![t_1]\!]'}(a_1,\dots,a_n),\dots, {[\![t_k]\!]'}(a_1,\dots,a_n)); that is, {[\![\sigma(t_1,\dots,t_k)]\!]'} is the following composite:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (1) at (0,0) {$A^n$}; \node (2) at (3,0) {$A^k$}; \node (3) at (5,0) {$A.$}; \draw[->] (1) to node[auto,labelsize]{$\langle {[\![t_1]\!]'},\dots,{[\![t_k]\!]'}\rangle$} (2); \draw[->] (2) to node[auto,labelsize] {${[\![\sigma]\!]}$} (3); \end{tikzpicture}

Note that for any n\in\mathbb{N} and \sigma\in\Sigma_n, {[\![\sigma]\!]}={[\![\sigma(x^{(n)}_1,\dots,x^{(n)}_n)]\!]'}. Henceforth, for any \Sigma-term t we simply write {[\![t]\!]} for {[\![t]\!]'} defined above.

Definition

Definition 2.5

18N0

Let \Sigma be a graded set. An element of the graded set T(\Sigma)\times T(\Sigma) is called a \Sigma-equation. We write a \Sigma-equation (n,(t,s))\in T(\Sigma)\times T(\Sigma) (that is, n\in\mathbb{N} and t,s\in T(\Sigma)_n) as t\approx_n s or t\approx s.

Definition

Definition 2.6

CABC

A presentation of an equational theory {{\langle\, \Sigma\, |\, E \,\rangle}} is a pair consisting of:

  • a graded set \Sigma of basic operations, and

  • a graded set E\subseteq T(\Sigma)\times T(\Sigma) of equational axioms.

Definition

Definition 2.7

6AWO

Let {{\langle\, \Sigma\, |\, E \,\rangle}} be a presentation of an equational theory.

  1. A model of {{\langle\, \Sigma\, |\, E \,\rangle}} is a \Sigma-algebra (A,{[\![-]\!]}) such that for any t\approx_n s\in E, {[\![t]\!]}={[\![s]\!]} holds.

  2. A homomorphism between models of {{\langle\, \Sigma\, |\, E \,\rangle}} is just a \Sigma-homomorphism between the corresponding \Sigma-algebras.

Definition

Definition 2.8

H49S

Let {{\langle\, \Sigma\, |\, E \,\rangle}} be a presentation of an equational theory.

  1. Define the set of {{\langle\, \Sigma\, |\, E \,\rangle}}-proofs inductively by the following inference rules. Every {{\langle\, \Sigma\, |\, E \,\rangle}}-proof is a finite rooted tree whose vertices are labelled by \Sigma-equations.

    (Ax) (if t\approx_n s \in E) t\approx_n s

    (Refl) t\approx_n t t\approx_n s (Sym) s\approx_n t t\approx_n s s\approx_n u (Trans) t\approx_n u

    s\approx_k s' t_1\approx_n t'_1 \cdots t_k\approx_n t'_k (Cong) s[x^{(k)}_1 \mapsto t_1, \dots, x^{(k)}_k\mapsto t_k]\approx_n s'[x^{(k)}_1 \mapsto t'_1, \dots, x^{(k)}_k\mapsto t'_k]

  2. A \Sigma-equation t\approx_n s\in T(\Sigma)\times T(\Sigma) is called an equational theorem of {{\langle\, \Sigma\, |\, E \,\rangle}} if there exists a {{\langle\, \Sigma\, |\, E \,\rangle}}-proof whose root is labelled by t\approx_n s. We write

    {{\langle\, \Sigma\, |\, E \,\rangle}}\vdash t\approx_n s

    to mean that t\approx_n s is an equational theorem of {{\langle\, \Sigma\, |\, E \,\rangle}}, and denote by \overline{E}\subseteq T(\Sigma)\times T(\Sigma) the graded set of all equational theorems of {{\langle\, \Sigma\, |\, E \,\rangle}}.

Definition

Definition 2.9

9IBZ
  1. Let \Sigma be a graded set and (A,{[\![-]\!]}) be a \Sigma-algebra. For any \Sigma-equation t\approx_n s\in T(\Sigma)\times T(\Sigma), we write

    (A,{[\![-]\!]})\vDash t\approx_n s

    to mean {[\![t]\!]}={[\![s]\!]}.

  2. Let {{\langle\, \Sigma\, |\, E \,\rangle}} be a presentation of an equational theory. For any \Sigma-equation t\approx_n s\in T(\Sigma)\times T(\Sigma), we write

    {{\langle\, \Sigma\, |\, E \,\rangle}}\vDash t\approx_n s

    to mean that for any model (A,{[\![-]\!]}) of {{\langle\, \Sigma\, |\, E \,\rangle}}, (A,{[\![-]\!]})\vDash t\approx_n s.

Theorem

Theorem 2.10

PVX3

Let {{\langle\, \Sigma\, |\, E \,\rangle}} be a presentation of an equational theory.

  1. (Soundness) Let t\approx_n s\in T(\Sigma)\times T(\Sigma). If {{\langle\, \Sigma\, |\, E \,\rangle}}\vdash t\approx_n s then {{\langle\, \Sigma\, |\, E \,\rangle}}\vDash t\approx_n s.

  2. (Completeness) Let t\approx_n s\in T(\Sigma)\times T(\Sigma). If {{\langle\, \Sigma\, |\, E \,\rangle}}\vDash t\approx_n s then {{\langle\, \Sigma\, |\, E \,\rangle}}\vdash t\approx_n s.

Proof of Theorem 2.10

The soundness theorem is proved by a straightforward induction over {{\langle\, \Sigma\, |\, E \,\rangle}}-proofs. For the completeness theorem, see e.g., [Johnstone_notes, Corollary 1.5] or [Burris_Sankappanavar, Section II.14].

Definition

Definition 2.11

G8ZF

A clone \mathsf{T} consists of:

  • (CD1) a graded set T=(T_n)_{n\in\mathbb{N}};

  • (CD2) for each n\in\mathbb{N} and i\in\{1,\dots,n\}, an element

    p^{(n)}_i\in T_n;
  • (CD3) for each k,n\in\mathbb{N}, a function

    \circ^{(n)}_k\colon T_k\times (T_n)^k\longrightarrow T_n

    whose action on an element (\phi,\theta_1,\dots,\theta_k)\in T_k\times (T_n)^k we write as \phi\circ^{(n)}_k(\theta_1,\dots,\theta_k) or simply as \phi\circ(\theta_1,\dots,\theta_k);

satisfying the following equations:

  • (CA1) for each k,n\in\mathbb{N}, j\in\{1,\dots,k\} and \theta_1,\dots,\theta_k\in T_n,

    p^{(k)}_j\circ^{(n)}_k(\theta_1,\dots,\theta_k) = \theta_j;
  • (CA2) for each n\in\mathbb{N}, \theta\in T_n,

    \theta\circ^{(n)}_n (p^{(n)}_1,\dots,p^{(n)}_n) = \theta;
  • (CA3) for each l,k,n\in\mathbb{N}, \psi\in T_l, \phi_1,\dots,\phi_l\in T_k, \theta_1,\dots,\theta_k\in T_n,

    \begin{gathered} \psi\circ^{(k)}_l\big(\phi_1\circ^{(n)}_k(\theta_1,\dots,\theta_k),\ \dots,\ \phi_l\circ^{(n)}_k(\theta_1,\dots,\theta_k)\big) \\= \big(\psi\circ^{(k)}_l(\phi_1,\dots,\phi_l)\big)\circ^{(n)}_k (\theta_1,\dots,\theta_k). \end{gathered}

Such a clone is written as \mathsf{T}=(T,(p^{(i)}_n)_{n\in\mathbb{N},i\in\{1,\dots,n\}}, (\circ^{(n)}_k)_{k,n\in\mathbb{N}}) or simply (T,p,\circ).

Definition

Definition 2.12

IXYQ

Let A be a set. Define the clone \mathsf{End}(A)=({\langle A, A\rangle},p,\circ)

as follows:

  • (CD1) for each n\in\mathbb{N}, let {\langle A, A\rangle}_n be the set of all functions from A^n to A;

  • (CD2) for each n\in\mathbb{N} and i\in\{1,\dots,n\}, let p^{(n)}_i be the i-th projection A^n\longrightarrow A, (a_1,\dots,a_n)\longmapsto a_i;

  • (CD3) for each k,n\in\mathbb{N}, g\colon A^k\longrightarrow A and f_1,\dots,f_k\colon A^n\longrightarrow A, let g\circ^{(n)}_k(f_1,\dots,f_k) be the function (a_1,\dots,a_n)\longmapsto g(f_1(a_1,\dots,a_n),\dots,f_k(a_1,\dots,a_n)), that is, the following composite:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (1) at (0,0) {$A^n$}; \node (2) at (3,0) {$A^k$}; \node (3) at (5,0) {$A.$}; \draw[->] (1) to node[auto,labelsize]{$\langle f_1,\dots,f_k\rangle$} (2); \draw[->] (2) to node[auto,labelsize] {$g$} (3); \end{tikzpicture}

It is straightforward to check the axioms (CA1)–(CA3).

Used by Example 3.14
Definition

Definition 2.13

G1TB

Let \mathsf{T}=(T,p,\circ) and \mathsf{T'}=(T',p',\circ') be clones. A clone homomorphism from \mathsf{T} to \mathsf{T'} is a morphism of graded sets (Definition 2.1) h\colon T\longrightarrow T' which preserves the structure of clones; precisely,

  • for each n\in\mathbb{N} and i\in\{1,\dots,n\}, h_n(p^{(n)}_i)=p'^{(n)}_i;

  • for each k,n\in\mathbb{N}, \phi\in T_k and \theta_1,\dots,\theta_k\in T_n,

    h_n\big(\phi\circ^{(n)}_k(\theta_1,\dots,\theta_k)\big)= h_k(\phi)\circ'^{(n)}_k \big(h_n(\theta_1),\dots,h_n(\theta_k)\big).\qedhere
Definition

Definition 2.14

3L1V

Let \mathsf{T} be a clone. A model of \mathsf{T} consists of a set A and a clone homomorphism \alpha\colon \mathsf{T}\longrightarrow \mathsf{End}(A).

Definition

Definition 2.15

Q51R
  1. Let A and B be sets. The graded set {\langle A, B\rangle} is defined by setting, for each n\in\mathbb{N}, {\langle A, B\rangle}_n be the set of all functions from A^n to B.

  2. Let A,A' and B be sets and f\colon A'\longrightarrow A be a function. The morphism of graded sets {\langle f, B\rangle}\colon{\langle A, B\rangle}\longrightarrow{\langle A', B\rangle} is defined by setting, for each n\in\mathbb{N}, {\langle f, B\rangle}_n\colon{\langle A, B\rangle}_n\longrightarrow{\langle A', B\rangle}_n be the precomposition by f^n\colon (A')^n\longrightarrow A^n; that is, h\longmapsto h\circ f^n.

  3. Let A,B and B' be sets and g\colon B\longrightarrow B' be a function. The morphism of graded sets {\langle A, g\rangle}\colon{\langle A, B\rangle}\longrightarrow{\langle A, B'\rangle} is defined by setting, for each n\in\mathbb{N}, {\langle A, g\rangle}_n\colon{\langle A, B\rangle}_n\longrightarrow{\langle A, B'\rangle}_n be the postcomposition by g\colon B\longrightarrow B'; that is, h\longmapsto g\circ h.

Definition

Definition 2.16

WXT4

Let \mathsf{T} be a clone, and (A,\alpha) and (B,\beta) be models of \mathsf{T}. A homomorphism from (A,\alpha) to (B,\beta) is a function f\colon A\longrightarrow B making the following diagram of morphisms of graded sets commute:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T$}; \node (TR) at (3,2) {${\langle A, A\rangle}$}; \node (BL) at (0,0) {${\langle B, B\rangle}$}; \node (BR) at (3,0) {${\langle A, B\rangle}.$}; \draw[->] (TL) to node[auto,labelsize](T) {$\alpha$} (TR); \draw[->] (TR) to node[auto,labelsize] {${\langle A, f\rangle}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\beta$} (BL); \draw[->] (BL) to node[auto,swap,labelsize](B) {${\langle f, B\rangle}$} (BR); \end{tikzpicture} \qedhere
Proposition

Proposition 2.17

2UNZ

Let \Sigma be a graded set. The clone \mathsf{T}(\Sigma) is the free clone generated from the graded set \Sigma. That is, the morphism of graded sets \eta_\Sigma\colon \Sigma\longrightarrow T(\Sigma), defined by (\eta_\Sigma)_n(\sigma)=\sigma(x^{(n)}_1,\dots,x^{(n)}_n) for each n\in\mathbb{N} and \sigma\in\Sigma_n, satisfies the following property: given any clone \mathsf{S}=(S,p,\circ) and any morphism of graded sets f\colon \Sigma\longrightarrow S, there exists a unique clone homomorphism g\colon \mathsf{T}(\Sigma)\longrightarrow \mathsf{S} such that g\circ \eta_\Sigma=f.

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$\Sigma$}; \node (TR) at (3,1) {${T}(\Sigma)$}; \node (BR) at (3,-1) {$S$}; \node (B) at (1.5,-1.8) {{(graded sets)}}; \draw[->] (TL) to node[auto,labelsize](T) {$\eta_\Sigma$} (TR); \draw[->] (TR) to node[auto,labelsize] {$g$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$f$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TR) at (3,1) {$\mathsf{T}(\Sigma)$}; \node (BR) at (3,-1) {$\mathsf{S}$}; \node (B) at (3,-1.8) {(clones)}; \draw[->,dashed] (TR) to node[auto,labelsize] {$g$} (BR); \end{tikzpicture}
Proof of Proposition 2.17

The clone homomorphism g may be defined by using the inductive nature of the definition of T(\Sigma), as follows:

  1. for each n\in\mathbb{N} and i\in\{1,\dots,n\}, let

    g_n(x^{(n)}_i)=p^{(n)}_i;
  2. for each k,n\in\mathbb{N}, \sigma\in\Sigma_k and t_1,\dots,t_k\in T(\Sigma)_n, let

    g_n(\sigma(t_1,\dots,t_k))=f_k(\sigma)\circ^{(n)}_k(g_n(t_1),\dots,g_n(t_k)).

To check that g is indeed a clone homomorphism, it suffices to show for each s\in T(\Sigma)_k and t_1,\dots,t_k\in T(\Sigma)_n,

g_n(s[x^{(k)}_1\mapsto t_1,\dots,x^{(k)}_k\mapsto t_k])= g_k(s)\circ^{(n)}_k(g_n(t_1),\dots, g_n(t_k));

this can be shown by induction on s. The uniqueness of g is clear.

Proposition

Proposition 2.18

5EDZ

Let {{\langle\, \Sigma\, |\, E \,\rangle}} be a presentation of an equational theory. The clone homomorphism q\colon \mathsf{T}(\Sigma)\longrightarrow \mathsf{T}^{{\langle\, \Sigma\, |\, E \,\rangle}}, defined by q_n(\theta)=[\theta]_{\overline{E}} for each n\in\mathbb{N} and \theta\in T(\Sigma)_n, satisfies the following property: given any clone \mathsf{S}=(S,p,\circ) and a clone homomorphism g\colon \mathsf{T}(\Sigma)\longrightarrow \mathsf{S} such that for any t\approx_n s\in E, g_n(t)=g_n(s), there exists a unique clone homomorphism h\colon \mathsf{T}^{{\langle\, \Sigma\, |\, E \,\rangle}}\longrightarrow\mathsf{S} such that h\circ q=g.

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$\mathsf{T}(\Sigma)$}; \node (TR) at (3,1) {$\mathsf{T}^{{\langle\, \Sigma\, |\, E \,\rangle}}$}; \node (BR) at (3,-1) {$\mathsf{S}$}; \draw[->] (TL) to node[auto,labelsize](T) {$q$} (TR); \draw[->,dashed] (TR) to node[auto,labelsize] {$h$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$g$} (BR); \end{tikzpicture}
Proof of Proposition 2.18

The clone homomorphism h is given by h_n([\theta]_{\overline{E}})=g_n(\theta); this is shown to be well-defined by induction on {{\langle\, \Sigma\, |\, E \,\rangle}}-proofs (see Definition 2.8). The uniqueness of h is immediate from the surjectivity of q.

Definition

Definition 2.19

DE2M

Let \Sigma be a graded set. The graded set T_\mathrm{SR}(\Sigma)=(T_\mathrm{SR}(\Sigma)_n)_{n\in\mathbb{N}} of strongly regular \Sigma-terms is defined inductively as follows.

  1. x^{(1)}_1\in T_\mathrm{SR}(\Sigma)_1.

  2. For each k,n_1,\dots,n_k\in\mathbb{N}, \sigma\in\Sigma_k and t_1\in T_\mathrm{SR}(\Sigma)_{n_1},\dots,t_k\in T_\mathrm{SR}(\Sigma)_{n_k}, writing n_1+\dots+n_k=n,

    \begin{gathered} \sigma(t_1[x^{(n_1)}_1\mapsto x^{(n)}_1,\dots,x^{(n_1)}_{n_1}\mapsto x^{(n)}_{n_1}], \dots,\\ t_k[x^{(n_k)}_1\mapsto x^{(n)}_{n_1+\dots+n_{k-1}+1},\dots, x^{(n_k)}_{n_k}\mapsto x^{(n)}_{n_1+\dots+n_{k-1}+n_k}]) \in T_\mathrm{SR}(\Sigma)_{n}. \end{gathered}

    When k=0, we usually write \sigma instead of \sigma().

Definition

Definition 2.20 (cf. Definition 2.5)

XYGA

Let \Sigma be a graded set. An element of the graded set T_\mathrm{SR}(\Sigma)\times T_\mathrm{SR}(\Sigma) is called a strongly regular \Sigma-equation. We write a strongly regular \Sigma-equation (n,(t,s))\in T_\mathrm{SR}(\Sigma)\times T_\mathrm{SR}(\Sigma) as t\approx_n s or t\approx s.

Definition

Definition 2.21 (cf. Definition 2.6)

T5CE

A strongly regular presentation of an equational theory {{\langle\, \Sigma\, |\, E \,\rangle}} is a pair consisting of:

  • a graded set \Sigma of basic operations, and

  • a graded set E\subseteq T_\mathrm{SR}(\Sigma)\times T_\mathrm{SR}(\Sigma) of (strongly regular) equational axioms.

Definition

Definition 2.22 (cf. Definition 2.11)

JUAQ

A non-symmetric operad \mathsf{T} consists of:

  • (ND1) a graded set T=(T_n)_{n\in\mathbb{N}};

  • (ND2) an element {\mathrm{id}_{}}\in T_1;

  • (ND3) for each k,n_1,\dots,n_k\in \mathbb{N}, a function (we omit the sub- and superscripts)

    \circ\colon T_k\times T_{n_1}\times\dots\times T_{n_k}\longrightarrow T_{n_1+\dots+ n_k}

    whose action we write as (\phi,\theta_1,\dots,\theta_k)\longmapsto \phi\circ (\theta_1,\dots,\theta_k)

satisfying the following equations:

  • (NA1) for each n\in\mathbb{N} and \theta\in T_n,

    {\mathrm{id}_{}}\circ (\theta)=\theta;
  • (NA2) for each n\in\mathbb{N} and \theta\in T_n,

    \theta\circ ({\mathrm{id}_{}},\dots,{\mathrm{id}_{}}) = \theta;
  • (NA3) for each l,\ k_1,\dots,k_l,\ n_{1,1},\dots,n_{1,k_1},\dots,n_{l,1}, \dots,n_{l,k_l}\in\mathbb{N}, \psi\in T_l, \phi_1\in T_{k_1}, \dots, \phi_l\in T_{k_l}, \theta_{1,1}\in T_{n_{1,1}},\dots,\theta_{1,k_1}\in T_{n_{1,k_1}}, \dots, \theta_{l,1}\in T_{n_{l,1}},\dots, \theta_{l,k_l}\in T_{n_{l, k_l}},

    \begin{gathered} \psi\circ\big(\phi_1\circ (\theta_{1,1},\dots,\theta_{1,k_1}),\ \dots\ , \phi_l\circ (\theta_{l,1},\dots,\theta_{l,k_l}) \big)\\ = \big(\psi\circ (\phi_1,\dots,\phi_l)\big)\circ(\theta_{1,1},\dots,\theta_{1,k_1},\ \dots,\ \theta_{l,1},\dots,\theta_{l,k_l}). \end{gathered}

Such a non-symmetric operad is written as \mathsf{T}=(T,{\mathrm{id}_{}},\circ).

Definition

Definition 2.23 (cf. Definition 2.12)

ZF1P

Let A be a set. Define the non-symmetric operad \mathsf{End}_\mathbf{Set}(A)=({\langle A, A\rangle},{\mathrm{id}_{}},\circ) as follows:

  • (ND1) for each n\in\mathbb{N}, let {\langle A, A\rangle}_n be the set of all functions from A^n to A;

  • (ND2) the element {\mathrm{id}_{}}\in{\langle A, A\rangle} is the identity function on A;

  • (ND3) for each k,n_1,\dots,n_k\in\mathbb{N}, g\colon A^k\longrightarrow A, f_1\colon A^{n_1}\longrightarrow A,\dots,f_k\colon A^{n_k}\longrightarrow A, let g\circ (f_1,\dots,f_k) be the following composite:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (1) at (-1,0) {$A^{n_1+\dots+n_k}$}; \node (2) at (3,0) {$A^{k}$}; \node (3) at (5,0) {$A.$}; \draw[->] (1) to node[auto,labelsize]{$f_1\times\dots\times f_k$} (2); \draw[->] (2) to node[auto,labelsize] {$g$} (3); \end{tikzpicture} \qedhere
Definition

Definition 2.24

HP0W

Let A be an abelian group. Define the non-symmetric operad \mathsf{End}_\mathbf{Ab}(A)=({\langle A, A\rangle},{\mathrm{id}_{}},\circ) as follows:

  • (ND1) for each n\in\mathbb{N}, let {\langle A, A\rangle}_n be the set of all group homomorphisms from A^{\otimes n} to A;

  • (ND2) the element {\mathrm{id}_{}}\in{\langle A, A\rangle} is the identity homomorphism on A;

  • (ND3) for each k,n_1,\dots,n_k\in\mathbb{N}, g\colon A^{\otimes k} \longrightarrow A, f_1\colon A^{\otimes n_1}\longrightarrow A,\dots, f_k\colon A^{\otimes n_k}\longrightarrow A, let g\circ (f_1,\dots,f_k) be the following composite:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (1) at (-1,0) {$A^{\otimes (n_1+\dots+n_k)}$}; \node (2) at (3,0) {$A^{\otimes k}$}; \node (3) at (5,0) {$A.$}; \draw[->] (1) to node[auto,labelsize]{$f_1\otimes\dots\otimes f_k$} (2); \draw[->] (2) to node[auto,labelsize] {$g$} (3); \end{tikzpicture} \qedhere
Definition

Definition 2.25 (cf. Definition 2.14)

C5JN

Let \mathsf{T} be a non-symmetric operad.

  1. A set model of \mathsf{T} consists of a set A and a non-symmetric operad homomorphism \mathsf{T}\longrightarrow \mathsf{End}_\mathbf{Set}(A).

  2. An abelian group model of \mathsf{T} consists of an abelian group A and a non-symmetric operad homomorphism \mathsf{T}\longrightarrow \mathsf{End}_\mathbf{Ab}(A).

Homomorphisms between set or abelian group models of \mathsf{T} are defined just as in Definition 2.16.

Definition

Definition 2.26 (cf. Definition 2.5)

S39X

Let \Sigma be a graded set. An element of the graded set T_\mathrm{R}(\Sigma)\times T_\mathrm{R}(\Sigma) is called a regular \Sigma-equation. We write a regular \Sigma-equation (n,(t,s))\in T_\mathrm{R}(\Sigma)\times T_\mathrm{R}(\Sigma) as t\approx_n s or t\approx s.

Definition

Definition 2.27 (cf. Definition 2.6)

UWWK

A regular presentation of an equational theory {{\langle\, \Sigma\, |\, E \,\rangle}} is a pair consisting of:

  • a graded set \Sigma of basic operations, and

  • a graded set E\subseteq T_\mathrm{R}(\Sigma)\times T_\mathrm{R}(\Sigma) of (regular) equational axioms.

Definition

Definition 2.28 (cf. Definition 2.11)

S2Z2

A symmetric operad \mathsf{T} consists of:

  • (SD1) a graded set T=(T_n)_{n\in\mathbb{N}};

  • (SD2) an element {\mathrm{id}_{}}\in T_1;

  • (SD3) for each k,n_1,\dots,n_k\in\mathbb{N}, a function (we omit the sub- and superscripts)

    \circ\colon T_k\times T_{n_1}\times\dots\times T_{n_k}\longrightarrow T_{n_1+\dots+n_k}

    whose action we write as (\phi,\theta_1,\dots,\theta_k)\longmapsto \phi\circ(\theta_1,\dots,\theta_k);

  • (SD4) for each n\in\mathbb{N}, a function

    \bullet\colon \mathfrak{S}_n\times T_n\longrightarrow T_n

satisfying the following equations:

  • (SA1) for each n\in\mathbb{N} and \theta\in T_n,

    {\mathrm{id}_{}}\circ (\theta)=\theta;
  • (SA2) for each n\in\mathbb{N} and \theta\in T_n,

    \theta\circ ({\mathrm{id}_{}},\dots,{\mathrm{id}_{}}) = \theta;
  • (SA3) for each l,\ k_1,\dots,k_l,\ n_{1,1},\dots,n_{1,k_1},\dots,n_{l,1}, \dots,n_{l,k_l}\in\mathbb{N}, \psi\in T_l, \phi_1\in T_{k_1}, \dots, \phi_l\in T_{k_l}, \theta_{1,1}\in T_{n_{1,1}},\dots,\theta_{1,k_1}\in T_{n_{1,k_1}}, \dots, \theta_{l,1}\in T_{n_{l,1}},\dots, \theta_{l,k_l}\in T_{n_{l, k_l}},

    \begin{gathered} \psi\circ\big(\phi_1\circ (\theta_{1,1},\dots,\theta_{1,k_1}),\ \dots\ , \phi_l\circ (\theta_{l,1},\dots,\theta_{l,k_l}) \big)\\ = \big(\psi\circ (\phi_1,\dots,\phi_l)\big)\circ(\theta_{1,1},\dots,\theta_{1,k_1},\ \dots\ , \theta_{l,1},\dots,\theta_{l,k_l}); \end{gathered}
  • (SA4) for each n\in\mathbb{N}, the function \bullet\colon \mathfrak{S}_n\times T_n\longrightarrow T_n is a left group action, that is, for each \theta\in T_n and u,v\in \mathfrak{S}_n,

    e_n\bullet \theta =\theta, \quad (v\cdot u)\bullet \theta=v\bullet(u\bullet\theta);
  • (SA5) for each k,n_1,\dots,n_k\in\mathbb{N}, \phi\in T_k, \theta_1\in T_{n_1},\dots,\theta_k\in T_{n_k} and u_1\in\mathfrak{S}_{n_1},\dots, u_k\in\mathfrak{S}_{n_k},

    \phi\circ(u_1\bullet\theta_1,\dots,u_k\bullet\theta_k) =(u_1\oplus \dots\oplus u_k)\bullet\big(\phi\circ(\theta_1,\dots,\theta_k)\big);
  • (SA6) for each k,n_1,\dots,n_k\in\mathbb{N}, \phi\in T_k, \theta_1\in T_{n_1},\dots,\theta_k\in T_{n_k} and v\in\mathfrak{S}_k,

    (v\bullet \phi)\circ(\theta_{v^{-1}(1)},\dots,\theta_{v^{-1}(k)}) =v_{n_1,\dots,n_k}\bullet \big(\phi\circ(\theta_1,\dots,\theta_k)\big).\qedhere
Definition

Definition 2.29

0BGN

Let \mathcal{C} be a large category.

  1. A monad on \mathcal{C} consists of:

    • a functor T\colon \mathcal{C}\longrightarrow \mathcal{C};

    • a natural transformation \eta\colon {\mathrm{id}_{\mathcal{C}}}\longrightarrow T (called the unit);

    • a natural transformation \mu\colon T\circ T\longrightarrow T (called the multiplication),

    making the following diagrams commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {${\mathrm{id}_{\mathcal{C}}}\circ T$}; \node (TR) at (2,2) {$T\circ T$}; \node (BR) at (2,0) {$T$}; \draw[->] (TL) to node[auto,labelsize](T) {$\eta\circ T$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$\mu$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {${\mathrm{id}_{T}}$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T\circ {\mathrm{id}_{\mathcal{C}}}$}; \node (TR) at (2,2) {$T\circ T$}; \node (BR) at (2,0) {$T$}; \draw[->] (TL) to node[auto,labelsize](T) {$T\circ \eta$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$\mu$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {${\mathrm{id}_{T}}$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T\circ T\circ T$}; \node (TR) at (3,2) {$T\circ T$}; \node (BL) at (0,0) {$T\circ T$}; \node (BR) at (3,0) {$T$}; \draw[->] (TL) to node[auto,labelsize](T) {$\mu\circ T$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\mu$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$T\circ \mu$} (BL); \draw[->] (BL) to node[auto,labelsize](B) {$\mu$} (BR); \end{tikzpicture}
  2. Let \mathsf{T}=(T,\eta,\mu) and \mathsf{T'}=(T',\eta',\mu') be monads on \mathcal{C}. A morphism of monads on \mathcal{C} from \mathsf{T} to \mathsf{T'} is a natural transformation \alpha\colon T\longrightarrow T' which commutes with the units and multiplications.

We denote the category of monads on \mathcal{C} by {\mathbf{Mnd}(\mathcal{C})}.

Definition

Definition 2.30

5KN2

Let \mathcal{C} be a large category and \mathsf{T}=(T,\eta,\mu) be a monad on \mathcal{C}.

  1. An Eilenberg–Moore algebra of \mathsf{T} consists of:

    • an object C\in\mathcal{C};

    • a morphism \gamma\colon TC\longrightarrow C in \mathcal{C},

    making the following diagrams commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$C$}; \node (TR) at (2,2) {$TC$}; \node (BR) at (2,0) {$C$}; \draw[->] (TL) to node[auto,labelsize](T) {$\eta_C$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$\gamma$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {${\mathrm{id}_{C}}$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$TTC$}; \node (TR) at (2,2) {$TC$}; \node (BL) at (0,0) {$TC$}; \node (BR) at (2,0) {$C.$}; \draw[->] (TL) to node[auto,labelsize](T) {$\mu_C$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\gamma$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$T\gamma$} (BL); \draw[->] (BL) to node[auto,labelsize](B) {$\gamma$} (BR); \end{tikzpicture}
  2. Let (C,\gamma) and (C',\gamma') be Eilenberg–Moore algebras of \mathsf{T}. A homomorphism from (C,\gamma) to (C',\gamma') is a morphism f\colon C\longrightarrow C' in \mathcal{C} making the following diagram commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$TC$}; \node (TR) at (2,2) {$TC'$}; \node (BL) at (0,0) {$C$}; \node (BR) at (2,0) {$C'.$}; \draw[->] (TL) to node[auto,labelsize](T) {$Tf$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\gamma'$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\gamma$} (BL); \draw[->] (BL) to node[auto,labelsize](B) {$f$} (BR); \end{tikzpicture}

The category of all Eilenberg–Moore algebras of \mathsf{T} and their homomorphism is celled the Eilenberg–Moore category of \mathsf{T}, and is denoted by \mathcal{C}^\mathsf{T}.

Definition

Definition 2.31

BBNP
  1. Let \mathcal{C} and \mathcal{D} be categories, and F,G\colon \mathcal{C}\longrightarrow \mathcal{D} be functors. A natural transformation \alpha\colon F\longrightarrow G is called cartesian if and only if all naturality squares of \alpha are pullback squares; that is, if and only if for any morphism f\colon C\longrightarrow C' in \mathcal{C}, the square

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$FC$}; \node (TR) at (2,2) {$GC$}; \node (BL) at (0,0) {$FC'$}; \node (BR) at (2,0) {$GC'$}; \draw[->] (TL) to node[auto,labelsize](T) {$\alpha_C$} (TR); \draw[->] (TR) to node[auto,labelsize] {$Gf$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$Ff$} (BL); \draw[->] (BL) to node[auto,labelsize](B) {$\alpha_{C'}$} (BR); \end{tikzpicture}

    is a pullback of Gf and \alpha_{C'}.

  2. Let \mathcal{C} be a category with all pullbacks. A monad \mathsf{S}=(S,\eta,\mu) on \mathcal{C} is called cartesian if and only if the functor S preserves pullbacks, and \eta and \mu are cartesian.

Definition

Definition 2.32

IQ0J

Let \mathcal{C} be a large category with all finite limits and \mathsf{S}=(S,\eta,\mu) a cartesian monad on \mathcal{C}.

  1. An \mathsf{S}-operad is a monoid object in the monoidal category (\mathcal{C}/S1,I,\otimes) introduced above; see Definition 3.1 for the definition of monoid object in a monoidal category.

  2. A morphism of \mathsf{S}-operads is a homomorphism of monoid objects; see Definition 3.1 again.

We denote the category of \mathsf{S}-operads by {{\mathsf{S}}\mhyphen\mathbf{Opd}}; by definition it is identical to the category {\mathbf{Mon}(\mathcal{C}/S1)} of monoid objects in \mathcal{C}/S1.

Example

Example 2.33

M3ZR

If we let \mathcal{C}=\mathbf{Set} and \mathsf{S} be the free monoid monad (which is cartesian), then \mathsf{S}-operads are equivalent to non-symmetric operads. The arities are the natural numbers: S1\cong\mathbb{N}.

In more detail, the data of an \mathsf{S}-operad in this case consist of a set T, and functions {\mathrm{ar}_{T}}\colon T\longrightarrow \mathbb{N}, e\colon 1\longrightarrow T and m\colon (T,{\mathrm{ar}_{T}})\ast T\longrightarrow T. Unravelling this, we obtain a graded set (T_n)_{n\in\mathbb{N}}, an element {\mathrm{id}_{}}\in T_1 and a family of functions (m_{k,n_1,\dots n_k}\colon T_k\times T_{n_1}\times\dots \times T_{n_k} \longrightarrow T_{n_1+\dots +n_k})_{k,n_1,\dots,n_k\in\mathbb{N}}, agreeing with Definition 2.22. Note that indeed T_n may be interpreted as the set of all (derived) operations of arity n.

Example

Example 2.34

JLR1

If we set \mathcal{C}={{n}\mhyphen\mathbf{Gph}}, the category of n-graphs for n\in\mathbb{N}\cup\{\omega\} and \mathsf{S} be the free strict n-category monad, then \mathsf{S}-operads are called n-globular operads; see [Leinster_book, Chapter 8] for illustrations. These generalised operads have been used to give a definition of weak n-categories, and they (and their generalisations) will play a central role in the second part of this thesis.

Definition

Definition 2.35

YM1D

Let \mathcal{C} be a large category with finite limits, \mathsf{S}=(S,\eta,\mu) a cartesian monad on \mathcal{C}, and \mathsf{T}=(T,e,m) an \mathsf{S}-operad.

  1. A model of \mathsf{T} consists of:

    • an object C\in\mathcal{C};

    • a morphism \gamma\colon T\ast C\longrightarrow C in \mathcal{C},

    making the following diagrams commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$I\ast C$}; \node (TR) at (2,2) {$T\ast C$}; \node (BR) at (2,0) {${C}$}; \draw[->] (TL) to node[auto,labelsize] {$e\ast C$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\gamma$} (BR); \draw[->] (TL) to node[auto,swap,labelsize](B) {$\cong$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$(T\otimes T)\ast C$}; \node (TR) at (5,2) {$T\ast C$}; \node (BL) at (0,0) {$T\ast (T\ast C)$}; \node (BM) at (3,0) {$T\ast C$}; \node (BR) at (5,0) {${C},$}; \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (TL) to node[auto,labelsize] {$m\ast C$} (TR); \draw[->] (BL) to node[auto,labelsize] {$T\ast \gamma$} (BM); \draw[->] (BM) to node[auto,labelsize] {$\gamma$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {$\gamma$} (BR); \end{tikzpicture}

    where the arrows labelled with \cong refer to the isomorphisms provided by the pseudo action.

  2. Let (C,\gamma) and (C',\gamma') be models of \mathsf{T}. A homomorphism from (C,\gamma) to (C',\gamma') is a morphism f\colon C\longrightarrow C' in \mathcal{C} making the following diagram commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T\ast C$}; \node (TR) at (3,2) {$T\ast C'$}; \node (BL) at (0,0) {$C$}; \node (BR) at (3,0) {$C'.$}; \draw[->] (TL) to node[auto,swap,labelsize] {$\gamma$} (BL); \draw[->] (TL) to node[auto,labelsize] {$T\ast f$} (TR); \draw[->] (BL) to node[auto,labelsize] {${f}$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {$\gamma'$} (BR); \end{tikzpicture} \qedhere
Definition

Definition 3.1

7FVQ

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category.

  1. A monoid object in \mathcal{M} (or simply a monoid in \mathcal{M}) is a triple \mathsf{T}=(T,e,m) consisting of an object T in \mathcal{M}, and morphisms e\colon I\longrightarrow T and m\colon T\otimes T\longrightarrow T in \mathcal{M}, such that the following diagrams commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$I\otimes T$}; \node (TR) at (2,1) {$T\otimes T$}; \node (BR) at (2,-1) {$T$}; \draw[->] (TL) to node[auto,labelsize](T) {$e\otimes T$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$m$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$\cong$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$T\otimes I$}; \node (TR) at (2,1) {$T\otimes T$}; \node (BR) at (2,-1) {$T$}; \draw[->] (TL) to node[auto,labelsize](T) {$T\otimes e$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$m$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$\cong$} (BR); \end{tikzpicture}
    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$(T\otimes T)\otimes T$}; \node (TR) at (5,2) {$T\otimes T$}; \node (BL) at (0,0) {$T\otimes (T\otimes T)$}; \node (BM) at (3,0) {$T\otimes T$}; \node (BR) at (5,0) {$T$}; \draw[->] (TL) to node[auto,labelsize](T) {$m\otimes T$} (TR); \draw[->] (TR) to node[auto,labelsize] {$m$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,labelsize] {$T\otimes m$} (BM); \draw[->] (BM) to node[auto,labelsize](B) {$m$} (BR); \end{tikzpicture}

    (Recall that the arrows labelled with \cong are the suitable instances of structural isomorphisms of \mathcal{M}.)

  2. Let \mathsf{T}=(T,e,m) and \mathsf{T'}=(T',e',m') be monoid objects in \mathcal{M}. A homomorphism from \mathsf{T} to \mathsf{T'} is a morphism f\colon T\longrightarrow T' in \mathcal{M} such that the following diagrams commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (1,2) {$I$}; \node (BL) at (0,0) {$T$}; \node (BR) at (2,0) {$T'$}; \draw[->] (TL) to node[auto,swap,labelsize] {$e$} (BL); \draw[->] (BL) to node[auto,labelsize] {$f$} (BR); \draw[->] (TL) to node[auto,labelsize](B) {$e'$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T\otimes T$}; \node (TR) at (3,2) {$T'\otimes T'$}; \node (BL) at (0,0) {$T$}; \node (BR) at (3,0) {$T'$}; \draw[->] (TL) to node[auto,swap,labelsize] {$m$} (BL); \draw[->] (TL) to node[auto,labelsize] {$f\otimes f$} (TR); \draw[->] (BL) to node[auto,labelsize] {$f$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {$m'$} (BR); \end{tikzpicture}

The category of all monoid objects in \mathcal{M} and homomorphisms is denoted by {\mathbf{Mon}(\mathcal{M})}.

Definition

Definition 3.2

UQII

Let \mathbf{F} be the category defined as follows:

  • The set of objects is {\mathrm{ob}(\mathbf{F})}=\{\,[n]\mid n\in\mathbb{N}\,\}, where for each natural number n\in\mathbb{N}, [n] is defined to be the n-element set \{1,\dots,n\}.

  • A morphism is any function between these sets.

Definition

Definition 3.3

C9MG

The substitution monoidal structure on [\mathbf{F},\mathbf{Set}] is defined as follows:

  • The unit object is I=\mathbf{F}([1],-)\colon \mathbf{F}\longrightarrow\mathbf{Set}.

  • Given X,Y\colon \mathbf{F}\longrightarrow\mathbf{Set}, their monoidal product Y\otimes X\colon \mathbf{F}\longrightarrow\mathbf{Set} maps [n]\in\mathbf{F} to

    (Y\otimes X)_n=\int^{[k]\in\mathbf{F}} Y_k\times (X_n)^k.
Proposition

Proposition 3.4 (cf. )

JWHF

The above constructions establish an isomorphism of categories between the category of clones and {\mathbf{Mon}([\mathbf{F},\mathbf{Set}])}.

Definition

Definition 3.5

NG9N

Let \mathbf{P} be the category defined as follows:

  • The set of objects is the same as \mathbf{F}: {\mathrm{ob}(\mathbf{P})}=\{\,[n]\mid n\in\mathbb{N}\,\} where [n]=\{1,\dots,n\}.

  • A morphism is any bijective function.

Definition

Definition 3.6

Y7T0

The substitution monoidal structure on [\mathbf{P},\mathbf{Set}] is defined as follows:

  • The unit object is I=\mathbf{P}([1],-)\colon\mathbf{P}\longrightarrow\mathbf{Set}.

  • Given X,Y\colon\mathbf{P}\longrightarrow\mathbf{Set}, their monoidal product Y\otimes X\colon \mathbf{P}\longrightarrow\mathbf{Set} maps [n]\in\mathbf{P} to

    (Y\otimes X)_n =\int^{[k]\in\mathbf{P}} Y_k\times (X^{\circledast k})_n,

    where

    (X^{\circledast k})_n=\int^{[n_1],\dots,[n_k]\in\mathbf{P}} \mathbf{P}([n_1+\dots+n_k],[n])\times X_{n_1}\times\dots\times X_{n_k}.\qedhere
Proposition

Proposition 3.7 (cf. )

2LXS

The category of symmetric operads is isomorphic to {\mathbf{Mon}([\mathbf{P},\mathbf{Set}])}.

Definition

Definition 3.8

BCPD

Let \mathbf{N} be the category defined as follows:

  • The set of objects is the same as \mathbf{F} and \mathbf{P}.

  • There are only identity morphisms in \mathbf{N}.

Definition

Definition 3.9

SHGQ

The substitution monoidal structure on [\mathbf{N},\mathbf{Set}] is defined as follows:

  • The unit object is I=\mathbf{N}([1],-)\colon \mathbf{N}\longrightarrow \mathbf{Set}.

  • Given X,Y\colon \mathbf{N}\longrightarrow\mathbf{Set}, their monoidal product Y\otimes X\colon\mathbf{N}\longrightarrow\mathbf{Set} maps [n]\in\mathbf{N} to

    (Y\otimes X)_n=\coprod_{[k]\in\mathbf{N}} Y_k\times\bigg(\coprod_{\substack{[n_1],\dots,[n_k]\in\mathbf{N}\\n_1+\dots+n_k=n}} X_{n_1}\times\dots\times X_{n_k}\bigg).\qedhere
Proposition

Proposition 3.10 (cf. )

5XWJ

The category of non-symmetric operads is isomorphic to {\mathbf{Mon}([\mathbf{N},\mathbf{Set}])}.

Definition

Definition 3.11

BVGL

Let \mathcal{C} be a large category. Define the monoidal category [\mathcal{C},\mathcal{C}]=([\mathcal{C},\mathcal{C}],{\mathrm{id}_{\mathcal{C}}},\circ) of endofunctors on \mathcal{C} as follows:

  • The underlying category is the category [\mathcal{C},\mathcal{C}] of all functors \mathcal{C}\longrightarrow\mathcal{C} and natural transformations.

  • The unit object is the identity functor {\mathrm{id}_{C}} on \mathcal{C}.

  • The monoidal product is given by composition of functors.

Definition

Definition 3.12

4VJ4

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category. An enrichment over \mathcal{M} consists of:

  • a large category \mathcal{C};

  • a functor {\langle -, -\rangle}\colon\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathcal{M};

  • a natural transformation (j_C\colon I\longrightarrow{\langle C, C\rangle})_{C\in\mathcal{C}};

  • a natural transformation (M_{A,B,C}\colon{\langle B, C\rangle}\otimes{\langle A, B\rangle} \longrightarrow{\langle A, C\rangle})_{A,B,C\in\mathcal{C}},

making the following diagrams commute for all A,B,C,D\in\mathcal{C}:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$I\otimes{\langle A, B\rangle}$}; \node (TR) at (4,1) {${\langle B, B\rangle}\otimes{\langle A, B\rangle}$}; \node (BR) at (4,-1) {${\langle A, B\rangle}$}; \draw[->] (TL) to node[auto,labelsize](T) {$j_B\otimes{\langle A, B\rangle}$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$M_{A,B,B}$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$\cong$} (BR); \end{tikzpicture} \quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {${\langle A, B\rangle}\otimes I$}; \node (TR) at (4,1) {${\langle A, B\rangle}\otimes{\langle A, A\rangle}$}; \node (BR) at (4,-1) {${\langle A, B\rangle}$}; \draw[->] (TL) to node[auto,labelsize](T) {${\langle A, B\rangle}\otimes j_A$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$M_{A,A,B}$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$\cong$} (BR); \end{tikzpicture}
\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$({\langle C, D\rangle}\otimes {\langle B, C\rangle})\otimes {\langle A, B\rangle}$}; \node (TR) at (9,1) {${\langle B, D\rangle}\otimes{\langle A, B\rangle}$}; \node (BL) at (0,-1) {${\langle C, D\rangle}\otimes({\langle B, C\rangle}\otimes{\langle A, B\rangle})$}; \node (BM) at (6,-1) {${\langle C, D\rangle}\otimes{\langle A, C\rangle}$}; \node (BR) at (9,-1) {${\langle A, D\rangle}.$}; \draw[->] (TL) to node[auto,labelsize](T) {$M_{B,C,D}\otimes{\langle A, B\rangle}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$M_{A,B,D}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,labelsize] {${\langle C, D\rangle}\otimes M_{A,B,C}$} (BM); \draw[->] (BM) to node[auto,labelsize](B) {$M_{A,C,D}$} (BR); \end{tikzpicture}

We say that (\mathcal{C},{\langle -, -\rangle},j,M) is an enrichment over \mathcal{M}, or that ({\langle -, -\rangle},j,M) is an enrichment of \mathcal{C} over \mathcal{M}.

Definition

Definition 3.13

DXKB

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category, \mathsf{T}=(T,e,m) be a monoid object in \mathcal{M}, \mathcal{C} be a large category, and {\langle -, -\rangle}=({\langle -, -\rangle},j,M) be an enrichment of \mathcal{C} over \mathcal{M}.

  1. A model of \mathsf{T} in \mathcal{C} with respect to {\langle -, -\rangle} is a pair (C,\chi) consisting of an object C of \mathcal{C} and a monoid homomorphism \chi\colon \mathsf{T}\longrightarrow\mathsf{End}_{\langle -, -\rangle}(C); that is, a morphism \chi\colon T\longrightarrow {\langle C, C\rangle} in \mathcal{M} making the following diagrams commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$I$}; \node (TR) at (2,2) {$T$}; \node (BR) at (2,0) {${\langle C, C\rangle}$}; \draw[->] (TL) to node[auto,labelsize] {$e$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\chi$} (BR); \draw[->] (TL) to node[auto,swap,labelsize](B) {$j_C$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T\otimes T$}; \node (TR) at (4,2) {$T$}; \node (BL) at (0,0) {${\langle C, C\rangle}\otimes{\langle C, C\rangle}$}; \node (BR) at (4,0) {${\langle C, C\rangle}.$}; \draw[->] (TL) to node[auto,swap,labelsize] {$\chi\otimes\chi$} (BL); \draw[->] (TL) to node[auto,labelsize] {$m$} (TR); \draw[->] (BL) to node[auto,labelsize] {$M_{C,C,C}$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {$\chi$} (BR); \end{tikzpicture}
  2. Let (C,\chi) and (C',\chi') be models of \mathsf{T} in \mathcal{C} with respect to {\langle -, -\rangle}. A homomorphism from (C,\chi) to (C',\chi') is a morphism f\colon C\longrightarrow C' in \mathcal{C} making the following diagram commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T$}; \node (TR) at (3,2) {${\langle C', C'\rangle}$}; \node (BL) at (0,0) {${\langle C, C\rangle}$}; \node (BR) at (3,0) {${\langle C, C'\rangle}.$}; \draw[->] (TL) to node[auto,swap,labelsize] {$\chi$} (BL); \draw[->] (TL) to node[auto,labelsize] {$\chi'$} (TR); \draw[->] (BL) to node[auto,labelsize] {${\langle C, f\rangle}$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {${\langle f, C'\rangle}$} (BR); \end{tikzpicture}

We denote the (large) category of models of \mathsf{T} in \mathcal{C} with respect to {\langle -, -\rangle} by {\mathbf{Mod}(\mathsf{T},(\mathcal{C},{\langle -, -\rangle}))}.

Example

Example 3.14

82U7

Recall that clones may be identified with monoids in [\mathbf{F},\mathbf{Set}] with the substitution monoidal structure. Let \mathcal{C} be a locally small(Recall that by Convention 1.3, “locally small” implies “large”.) category with all finite powers. We have an enrichment of \mathcal{C} over [\mathbf{F},\mathbf{Set}] defined as follows:

  • The functor {\langle -, -\rangle}\colon \mathcal{C}^{\mathrm{op}}\times\mathcal{C} \longrightarrow[\mathbf{F},\mathbf{Set}] maps A,B\in\mathcal{C} and [n]\in\mathbf{F} to the set

    {\langle A, B\rangle}_n=\mathcal{C}(A^n,B).
  • The natural transformation (j_C\colon I\longrightarrow {\langle C, C\rangle})_{C\in\mathcal{C}} corresponds by the Yoneda lemma (recall that I=\mathbf{F}([1],-)) to the family

    (\overline{j}_C={\mathrm{id}_{C}}\in {\langle C, C\rangle}_1)_{C\in\mathcal{C}}.
  • The natural transformation (M_{A,B,C}\colon {\langle B, C\rangle}\otimes {\langle A, B\rangle}\longrightarrow{\langle A, C\rangle})_{A,B,C\in\mathcal{C}} corresponds by the universality of coends (recall that (Y\otimes X)_{n}=\int^{[k]\in\mathbf{F}} Y_k\times (X_n)^k) to the family whose (A,B,C)-th component is given by

    (\overline{M}_{A,B,C})_{n,k}\colon {\langle B, C\rangle}_k\times ({\langle A, B\rangle}_n)^k \longrightarrow{\langle A, B\rangle}_n

    mapping (g,f_1,\dots,f_k)\in \mathcal{C}(B^k,C)\times \mathcal{C}(A^n,B)^k to g\circ\langle f_1,\dots,f_k\rangle\in\mathcal{C}(A^n,B).

Clearly the definition of the clone \mathsf{End}(A) from a set A (Definition 2.12) is derived from the above enrichment, by setting \mathcal{C}=\mathbf{Set}. Consequently, we restore the classical definitions of model (Definition 2.14) and homomorphism between models (Definition 2.16) for clones as instances of Definition 3.13.

Example

Example 3.15

RA0A

Symmetric operads may be identified with monoids in [\mathbf{P},\mathbf{Set}] with the substitution monoidal structure. Let \mathcal{C}=(\mathcal{C},I',\otimes') be a locally small symmetric monoidal category. We have an enrichment of \mathcal{C} over [\mathbf{P},\mathbf{Set}] defined as follows:

  • The functor {\langle -, -\rangle}\colon \mathcal{C}^{\mathrm{op}}\times\mathcal{C} \longrightarrow[\mathbf{P},\mathbf{Set}] maps A,B\in\mathcal{C} and [n]\in\mathbf{P} to the set

    {\langle A, B\rangle}_n=\mathcal{C}(A^{\otimes' n},B),

    where A^{\otimes' n} is the monoidal product of n many copies of A.

  • The natural transformation (j_C\colon I\longrightarrow {\langle C, C\rangle})_{C\in\mathcal{C}} corresponds by the Yoneda lemma (recall that I=\mathbf{P}([1],-)) to the family

    (\overline{j}_C={\mathrm{id}_{C}}\in {\langle C, C\rangle}_1)_{C\in\mathcal{C}}.
  • The natural transformation (M_{A,B,C}\colon {\langle B, C\rangle}\otimes {\langle A, B\rangle}\longrightarrow{\langle A, C\rangle})_{A,B,C\in\mathcal{C}} corresponds by the universality of coends (recall Definition 3.6) to the family whose (A,B,C)-th component is given by

    \begin{gathered} (\overline{M}_{A,B,C})_{n,k,n_1,\dots,n_k}\colon {\langle B, C\rangle}_k\times \mathbf{P}([n_1+\dots+n_k],[n])\\ \times {\langle A, B\rangle}_{n_1}\times\dots\times{\langle A, B\rangle}_{n_k} \longrightarrow{\langle A, B\rangle}_n, \end{gathered}

    which is the unique function from the empty set if n\neq n_1+\dots+n_k and, if n= n_1+\dots+n_k, maps (g,u,f_1,\dots,f_k)\in \mathcal{C}(B^{\otimes' k},C)\times \mathbf{P}([n_1+\dots+n_k],[n])\times \mathcal{C}(A^{\otimes' n_1},B) \times\dots\times \mathcal{C}(A^{\otimes' n_k},B) to g\circ (f_1\otimes'\dots\otimes' f_k)\circ A^{\otimes' u}.

Via the above enrichment, we restore the classical definitions of model and homomorphism between models for symmetric operads.

Example

Example 3.16

4QWG

Non-symmetric operads may be identified with monoids in [\mathbf{N},\mathbf{Set}] with the substitution monoidal structure. Let \mathcal{C}=(\mathcal{C},I',\otimes') be a locally small monoidal category. We have an enrichment of \mathcal{C} over [\mathbf{N},\mathbf{Set}] which is similar to, and simpler than, the one in the previous example.

This enrichment restores the classical definitions of model and homomorphism between models for non-symmetric operads, including Definition 2.25 (take \mathcal{C}=(\mathbf{Set},1,\times) for set models and \mathcal{C}=(\mathbf{Ab},\mathbb{Z},\otimes) for abelian group models).

Example

Example 3.17

U4G2

We may also consider infinitary variants of Example 3.14. Here we take an extreme. Let \mathcal{C} be a locally small category with all small powers. Then we obtain an enrichment of \mathcal{C} over [\mathbf{Set},\mathbf{Set}], the category of endofunctors on \mathbf{Set} with composition as the monoidal product.

  • The functor {\langle -, -\rangle}\colon \mathcal{C}^{\mathrm{op}}\times \mathcal{C}\longrightarrow[\mathbf{Set},\mathbf{Set}] maps A,B\in\mathcal{C} and X\in \mathbf{Set} to the set

    {\langle A, B\rangle}(X)=\mathcal{C}(A^X,B),

    where A^X is the X-th power of A.

  • The natural transformation (j_C\colon {\mathrm{id}_{\mathbf{Set}}}\longrightarrow {\langle C, C\rangle})_{C\in\mathcal{C}} corresponds by the Yoneda lemma (note that {\mathrm{id}_{\mathbf{Set}}}\cong\mathbf{Set}(1,-), where 1 is a singleton) to the family

    (\overline{j}_C={\mathrm{id}_{C}}\in{\langle C, C\rangle}(1))_{C\in\mathcal{C}}.
  • The natural transformation (M_{A,B,C}\colon {\langle B, C\rangle}\circ{\langle A, B\rangle}\longrightarrow{\langle A, C\rangle})_{A,B,C\in\mathcal{C}} has the X-th component (X\in\mathbf{Set})

    {\langle B, C\rangle}\circ{\langle A, B\rangle}(X)=\mathcal{C}(B^{\mathcal{C}(A^X,B)},C)\longrightarrow \mathcal{C}(A^X,C)={\langle A, C\rangle}(X)

    the function induced from the canonical morphism A^X\longrightarrow B^{\mathcal{C}(A^X,B)} in \mathcal{C}.

Since monoids in [\mathbf{Set},\mathbf{Set}] are precisely monads on \mathbf{Set}, this enrichment gives us a definition of model of a monad \mathsf{T} on \mathbf{Set} in \mathcal{C}. To spell this out, first note that for any object C\in\mathcal{C}, the functor {\langle C, C\rangle}\colon \mathbf{Set}\longrightarrow\mathbf{Set} which maps X\in\mathbf{Set} to \mathcal{C}(C^X,C) acquires the monad structure, giving rise to the monad \mathsf{End}_{{\langle -, -\rangle}}(C) on \mathbf{Set}. A model of \mathsf{T} is then an object C\in\mathcal{C} together with a monad morphism \mathsf{T}\longrightarrow\mathsf{End}_{{\langle -, -\rangle}}(C). This is the definition of relative algebra of a monad on \mathbf{Set} by Hino, Kobayashi, Hasuo and Jacobs [Hino]. As noted in [Hino], in the case where \mathcal{C}=\mathbf{Set}, relative algebras of a monad \mathsf{T} on \mathbf{Set} agree with Eilenberg–Moore algebras of \mathsf{T}; we shall later show this fact in Example 3.30.

Example

Example 3.18

JTTG

Let \mathcal{S} be a large category and consider the monoidal category [\mathcal{S},\mathcal{S}] of endofunctors on \mathcal{S}, with composition as the monoidal product. Then an enrichment over [\mathcal{S},\mathcal{S}] is the same thing as an \mathcal{S}-parameterised monad (without strength) in the sense of Atkey [Atkey_parameterised, Definition 1], introduced in the study of computational effects.

Definition

Definition 3.19

9YZQ

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category. The (locally large) 2-category {\mathscr{E}\!nrich(\mathcal{M})} of enrichments over \mathcal{M} is defined as follows:

  • An object is an enrichment (\mathcal{C},{\langle -, -\rangle},j,M) over \mathcal{M}.

  • A 1-cell from (\mathcal{C},{\langle -, -\rangle},j,M) to (\mathcal{C'},{\langle -, -\rangle}',j',M') is a functor G\colon\mathcal{C}\longrightarrow\mathcal{C'} together with a natural transformation (g_{A,B}\colon{\langle A, B\rangle}\longrightarrow{\langle GA, GB\rangle}')_{A,B\in\mathcal{C}} making the following diagrams commute for all A,B,C\in\mathcal{C}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$I$}; \node (TR) at (4,1) {${\langle C, C\rangle}$}; \node (BR) at (4,-1) {${\langle GC, GC\rangle}'$}; \draw[->] (TL) to node[auto,labelsize](T) {$j_C$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$g_{C,C}$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$j'_{GC}$} (BR); \end{tikzpicture}
    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {${\langle B, C\rangle}\otimes{\langle A, B\rangle}$}; \node (TR) at (6,1) {${\langle A, C\rangle}$}; \node (BL) at (0,-1) {${\langle GB, GC\rangle}'\otimes{\langle GA, GB\rangle}'$}; \node (BR) at (6,-1) {${\langle GA, GC\rangle}'.$}; \draw[->] (TL) to node[auto,labelsize](T) {$M_{A,B,C}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$g_{A,C}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$g_{B,C}\otimes g_{A,B}$} (BL); \draw[->] (BL) to node[auto,labelsize] {$M'_{GA,GB,GC}$} (BR); \end{tikzpicture}
  • A 2-cell from (G,g) to (G',g'), both from (\mathcal{C},{\langle -, -\rangle},j,M) to (\mathcal{C'},{\langle -, -\rangle}',j', M'), is a natural transformation \theta\colon G\Longrightarrow G' making the following diagram commute for all A,B\in\mathcal{C}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {${\langle A, B\rangle}$}; \node (TR) at (4,2) {${\langle GA, GB\rangle}'$}; \node (BL) at (0,0) {${\langle G'A, G'B\rangle}'$}; \node (BR) at (4,0) {${\langle GA, G'B\rangle}'.$}; \draw[->] (TL) to node[auto,labelsize](T) {$g_{A,B}$} (TR); \draw[->] (TR) to node[auto,labelsize] {${\langle GA, \theta_B\rangle}'$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$g'_{A,B}$} (BL); \draw[->] (BL) to node[auto,labelsize] {${\langle \theta_A, G'B\rangle}'$} (BR); \end{tikzpicture} \qedhere
Example

Example 3.20

J77U

Let {\mathscr{F\!P}\!ow} be the 2-category of locally small categories with chosen finite powers, functors preserving finite powers (in the usual sense(That is, we do not require these functors to preserve the chosen finite powers on the nose.)) and all natural transformations. We have a canonical 2-functor

{\mathscr{F\!P}\!ow}\longrightarrow{\mathscr{E}\!nrich([\mathbf{F},\mathbf{Set}])}

which is fully faithful (see Section ? for the definition of full faithfulness for 2-functors).

Let {\mathscr{F\!P}\!rod} be the 2-category of locally small categories with chosen finite products, functors preserving finite products (in the usual sense) and all natural transformations. We have a canonical 2-functor

{\mathscr{F\!P}\!rod}\longrightarrow{\mathscr{E}\!nrich([\mathbf{F},\mathbf{Set}])}

which is locally fully faithful.

Hence we may restore the classical functoriality of {\mathbf{Mod}(\mathsf{T},-)} for a clone \mathsf{T}, recalled above, if we could show that it is functorial with respect to morphisms in {\mathscr{E}\!nrich([\mathbf{F},\mathbf{Set}])}.

Definition

Definition 3.21

0IO3

Let \mathcal{M}=(\mathcal{M},I_\mathcal{M},\otimes_\mathcal{M}) and \mathcal{N}=(\mathcal{N},I_\mathcal{N},\otimes_\mathcal{N}) be large monoidal categories, F=(F,f_\cdot,f)\colon\mathcal{M}\longrightarrow\mathcal{N} be a lax monoidal functor,(In more detail, such a lax monoidal functor (also called monoidal functors in e.g., [MacLane_CWM]) (F,f_\cdot,f) consists of a functor F\colon\mathcal{M}\longrightarrow\mathcal{N}, a morphism f_\cdot\colon I_\mathcal{N}\longrightarrow FI_\mathcal{M} and a natural transformation (f_{X,Y}\colon FY\otimes_\mathcal{N}FX\longrightarrow F(Y\otimes_\mathcal{M} X))_{X,Y\in\mathcal{M}} satisfying the suitable axioms.) \mathcal{C} be a large category and {\langle -, -\rangle}=({\langle -, -\rangle},j,M) be an enrichment of \mathcal{C} over \mathcal{M}. We define the enrichment F_\ast({\langle -, -\rangle})=({\langle -, -\rangle}',j',M') of \mathcal{C} over \mathcal{N} as follows:

  • The functor {\langle -, -\rangle}'\colon\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathcal{N} maps (A,B)\in\mathcal{C}^{\mathrm{op}}\times\mathcal{C} to F{\langle A, B\rangle}.

  • The natural transformation (j'_C\colon I_\mathcal{N}\longrightarrow{\langle C, C\rangle}')_{C\in\mathcal{C}} is defined by j'_C=Fj_C\circ f_\cdot:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$I_\mathcal{N}$}; \node (M) at (2,0) {$FI_\mathcal{M}$}; \node (R) at (4.5,0) {$F{\langle C, C\rangle}$.}; \draw[->] (L) to node[auto,labelsize] {$f_\cdot$} (M); \draw[->] (M) to node[auto,labelsize] {$Fj_C$} (R); \end{tikzpicture}
  • The natural transformation (M'_{A,B,C}\colon {\langle B, C\rangle}'\otimes_\mathcal{N}{\langle A, B\rangle}'\longrightarrow{\langle A, C\rangle}')_{A, B,C\in\mathcal{C}} is defined by M'_{A,B,C}=FM_{A,B,C}\circ f_{{\langle A, B\rangle},{\langle B, C\rangle}}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$F{\langle B, C\rangle}\otimes_\mathcal{N}F{\langle A, B\rangle}$}; \node (M) at (5.5,0) {$F({\langle B, C\rangle}\otimes_\mathcal{M}{\langle A, B\rangle})$}; \node (R) at (9.5,0) {$F{\langle A, C\rangle}$.}; \draw[->] (L) to node[auto,labelsize] {$f_{{\langle A, B\rangle},{\langle B, C\rangle}}$} (M); \draw[->] (M) to node[auto,labelsize] {$FM_{A,B,C}$} (R); \end{tikzpicture} \qedhere
Definition

Definition 3.22

RCHO

Let \mathcal{M} be a large monoidal category. The 2-category {\mathscr{E}\!nrich'(\mathcal{M})} is defined as follows:

  • An object is a triple (\mathcal{C},\mathcal{D},J) consisting of a large category \mathcal{C}, a large \mathcal{M}-category \mathcal{D} and an identity-on-objects functor J\colon\mathcal{C}\longrightarrow \mathcal{D}_0.

  • A 1-cell from (\mathcal{C},\mathcal{D},J) to (\mathcal{C'},\mathcal{D'},J') is given by a functor G\colon \mathcal{C}\longrightarrow\mathcal{C'} and an \mathcal{M}-functor H\colon \mathcal{D}\longrightarrow\mathcal{D'} such that H_0\circ J=J'\circ G.

  • A 2-cell from (G,H) to (G',H'), both from (\mathcal{C},\mathcal{D},J) to (\mathcal{C'},\mathcal{D'},J'), is given by a natural transformation \theta\colon G\Longrightarrow G' and an \mathcal{M}-natural transformation \phi\colon H\Longrightarrow H' such that \phi_0\circ J=J'\circ \theta.

Definition

Definition 3.23

1621

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category. An oplax action of \mathcal{M} consists of:

  • a large category \mathcal{C};

  • a functor \ast \colon \mathcal{M}\times\mathcal{C}\longrightarrow\mathcal{C};

  • a natural transformation (\varepsilon_C\colon I\ast C\longrightarrow C)_{C\in\mathcal{C}};

  • a natural transformation (\delta_{X,Y,C}\colon (Y\otimes X)\ast C\longrightarrow Y\ast (X\ast C))_{X,Y\in\mathcal{M},C\in\mathcal{C}},(We have chosen to set \delta_{X,Y,C}\colon (Y\otimes X)\ast C \longrightarrow Y\ast (X\ast C) and not \delta_{X,Y,C}\colon (X\otimes Y)\ast C \longrightarrow X\ast (Y\ast C), because the former agrees with the convention to write composition of morphisms in the anti-diagrammatic order, which we adopt throughout this thesis.)

making the following diagrams commute for all X,Y,Z\in\mathcal{M} and C\in\mathcal{C}:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$(I\otimes X)\ast C$}; \node (TR) at (4,1) {$I\ast(X\ast C)$}; \node (BR) at (4,-1) {$X\ast C$}; \draw[->] (TL) to node[auto,labelsize](T) {$\delta_{X,I,C}$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$\varepsilon_{X\ast C}$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$\cong$} (BR); \end{tikzpicture} \quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$(X\otimes I)\ast C$}; \node (TR) at (4,1) {$X\ast(I\ast C)$}; \node (BR) at (4,-1) {$X\ast C$}; \draw[->] (TL) to node[auto,labelsize](T) {$\delta_{I,X,C}$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$X\ast \varepsilon_{C}$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$\cong$} (BR); \end{tikzpicture}
\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$((Z\otimes Y)\otimes X)\ast C$}; \node (TR) at (9,1) {$(Z\otimes Y)\ast (X\ast C)$}; \node (BL) at (0,-1) {$(Z\otimes (Y\otimes X))\ast C$}; \node (BM) at (4.5,-1) {$Z\ast ((Y\otimes X)\ast C)$}; \node (BR) at (9,-1) {$Z\ast (Y\ast (X\ast C)).$}; \draw[->] (TL) to node[auto,labelsize](T) {$\delta_{X,Z\otimes Y,C}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\delta_{Y,Z,X\ast C}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,labelsize] {$\delta_{Y\otimes X,Z,C}$} (BM); \draw[->] (BM) to node[auto,labelsize](B) {$Z\ast \delta_{X,Y,C}$} (BR); \end{tikzpicture}

We say that (\mathcal{C},\ast,\varepsilon,\delta) is an oplax action of \mathcal{M}, or that (\ast,\varepsilon,\delta) is an oplax action of \mathcal{M} on \mathcal{C}.

Definition

Definition 3.24

YRXG

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category, \mathsf{T}=(T,e,m) be a monoid object in \mathcal{M}, \mathcal{C} be a large category, and \ast=(\ast,\varepsilon,\delta) be an oplax action of \mathcal{M} on \mathcal{C}.

  1. A model of \mathsf{T} in \mathcal{C} with respect to \ast is a pair (C,\gamma) consisting of an object C\in\mathcal{C} and a morphism \gamma\colon T\ast C\longrightarrow C in \mathcal{C} making the following diagrams commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$I\ast C$}; \node (TR) at (2,2) {$T\ast C$}; \node (BR) at (2,0) {${C}$}; \draw[->] (TL) to node[auto,labelsize] {$e\ast C$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\gamma$} (BR); \draw[->] (TL) to node[auto,swap,labelsize](B) {$\varepsilon_C$} (BR); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$(T\otimes T)\ast C$}; \node (TR) at (5,2) {$T\ast C$}; \node (BL) at (0,0) {$T\ast (T\ast C)$}; \node (BM) at (3,0) {$T\ast C$}; \node (BR) at (5,0) {${C}.$}; \draw[->] (TL) to node[auto,swap,labelsize] {$\delta_{T,T,C}$} (BL); \draw[->] (TL) to node[auto,labelsize] {$m\ast C$} (TR); \draw[->] (BL) to node[auto,labelsize] {$T\ast \gamma$} (BM); \draw[->] (BM) to node[auto,labelsize] {$\gamma$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {$\gamma$} (BR); \end{tikzpicture}
  2. Let (C,\gamma) and (C',\gamma') be models of \mathsf{T} in \mathcal{C} with respect to \ast. A homomorphism from (C,\gamma) to (C',\gamma') is a morphism f\colon C\longrightarrow C' in \mathcal{C} making the following diagram commute:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$T\ast C$}; \node (TR) at (3,2) {$T\ast C'$}; \node (BL) at (0,0) {$C$}; \node (BR) at (3,0) {$C'.$}; \draw[->] (TL) to node[auto,swap,labelsize] {$\gamma$} (BL); \draw[->] (TL) to node[auto,labelsize] {$T\ast f$} (TR); \draw[->] (BL) to node[auto,labelsize] {${f}$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {$\gamma'$} (BR); \end{tikzpicture}

We denote the (large) category of models of \mathsf{T} in \mathcal{C} with respect to \ast by {\mathbf{Mod}(\mathsf{T},(\mathcal{C},\ast))}.

Example

Example 3.25

0VA0

Let \mathcal{C} be a large category. Recall that monads on \mathcal{C} are precisely monoids in the monoidal category [\mathcal{C},\mathcal{C}] whose monoidal product is given by composition. We have a strict action

\ast\colon [\mathcal{C},\mathcal{C}]\times\mathcal{C}\longrightarrow\mathcal{C}

given by evaluation: (X,C)\longmapsto XC.

This clearly generates the definitions of Eilenberg–Moore algebra and homomorphism (Definition 2.30).

Used by Example 3.49
Example

Example 3.26

KWJP

Let \mathcal{C} be a large category with finite limits and \mathsf{S}=(S,\eta,\mu) be a cartesian monad on \mathcal{C}. Recall that under these assumptions the slice category \mathcal{C}/S1 acquires a structure (I,\otimes) of monoidal category, and an \mathsf{S}-operad is a monoid in (\mathcal{C}/S1,I,\otimes). Models of an \mathsf{S}-operad and their homomorphisms (Definition 2.35) were introduced by using the pseudo action

\ast\colon(\mathcal{C}/S1)\times \mathcal{C}\longrightarrow\mathcal{C}

in the first place, and therefore are immediately an instance of the above general definitions.

Definition

Definition 3.27

DPIC

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category. The (locally large) 2-category {\mathscr{A}\!ct_{\mathrm{oplax}}(\mathcal{M})} of oplax actions of \mathcal{M} is defined as follows:

  • An object is an oplax action (\mathcal{C},\ast,\varepsilon,\delta) of \mathcal{M}.

  • A 1-cell from (\mathcal{C},\ast,\varepsilon,\delta) to (\mathcal{C'},\ast',\varepsilon',\delta') is a functor G\colon \mathcal{C} \longrightarrow\mathcal{C'} together with a natural transformation (g_{X,C}\colon X\ast' GC\longrightarrow G(X\ast C))_{X\in\mathcal{M},C\in\mathcal{C}} making the following diagrams commute for all X,Y\in\mathcal{M} and C\in\mathcal{C}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$I\ast' GC$}; \node (TR) at (4,1) {$G(I\ast C)$}; \node (BR) at (4,-1) {$GC$}; \draw[->] (TL) to node[auto,labelsize](T) {$g_{I,C}$} (TR); \draw[->] (TR) to node[auto,labelsize](R) {$G\varepsilon_C$} (BR); \draw[->] (TL) to node[auto,labelsize,swap] (L) {$\varepsilon'_{GC}$} (BR); \end{tikzpicture}
    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$(Y\otimes X)\ast' GC$}; \node (TR) at (8,1) {$G((Y\otimes X)\ast C)$}; \node (BL) at (0,-1) {$Y\ast'(X\ast'GC)$}; \node (BM) at (4,-1) {$Y\ast'G(X\ast C)$}; \node (BR) at (8,-1) {$G(Y\ast (X\ast C)).$}; \draw[->] (TL) to node[auto,labelsize](T) {$g_{Y\otimes X,C}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$G\delta_{X,Y,C}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\delta'_{X,Y,GC}$} (BL); \draw[->] (BL) to node[auto,labelsize] {$Y\ast' g_{X,C}$} (BM); \draw[->] (BM) to node[auto,labelsize](B) {$g_{Y,X\ast C}$} (BR); \end{tikzpicture}
  • A 2-cell from (G,g) to (G',g'), both from (\mathcal{C},\ast,\varepsilon,\delta) to (\mathcal{C'},\ast',\varepsilon',\delta'), is a natural transformation \theta\colon G\Longrightarrow G' making the following diagram commute for all X\in\mathcal{M} and C\in\mathcal{C}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$X\ast' GC$}; \node (TR) at (4,2) {$G(X\ast C)$}; \node (BL) at (0,0) {$X\ast' G'C$}; \node (BR) at (4,0) {$G'(X\ast C).$}; \draw[->] (TL) to node[auto,labelsize](T) {$g_{X,C}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\theta_{X\ast C}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$X\ast' \theta_C$} (BL); \draw[->] (BL) to node[auto,labelsize] {$g'_{X,C}$} (BR); \end{tikzpicture} \qedhere
Definition

Definition 3.28

UI8X

Let \mathcal{M}=(\mathcal{M},I_\mathcal{M},\otimes_\mathcal{M}) and \mathcal{N}=(\mathcal{N},I_\mathcal{N},\otimes_\mathcal{N}) be large monoidal categories, G=(G,g_\cdot,g)\colon\mathcal{N}\longrightarrow\mathcal{M} be an oplax monoidal functor,(Such an oplax functor consists of a functor G\colon\mathcal{N}\longrightarrow\mathcal{M}, a morphism g_\cdot\colon GI_\mathcal{N}\longrightarrow I_\mathcal{M} and a natural transformation (g_{X,Y}\colon G(Y\otimes_\mathcal{N}X) \longrightarrow GY\otimes_\mathcal{M} GX)_{X,Y\in\mathcal{N}} satisfying the suitable axioms.) \mathcal{C} be a large category and \ast=(\ast,\varepsilon,\delta) be an oplax action of \mathcal{M} on \mathcal{C}. We define the oplax action G^\ast(\ast)=(\ast',\varepsilon',\delta') of \mathcal{N} on \mathcal{C} as follows:

  • The functor \ast'\colon\mathcal{N}\times\mathcal{C}\longrightarrow\mathcal{C} maps (X,C)\in\mathcal{N}\times\mathcal{C} to (GX)\ast C.

  • The natural transformation (\varepsilon'_C\colon I_\mathcal{N}\ast' C\longrightarrow C)_{C\in\mathcal{C}} is defined by \varepsilon'_C=\varepsilon_C\circ (g_\cdot\ast C):

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$GI_\mathcal{N}\ast C$}; \node (M) at (2.5,0) {$I_\mathcal{M}\ast C$}; \node (R) at (4.5,0) {${C}$.}; \draw[->] (L) to node[auto,labelsize] {$g_\cdot\ast C$} (M); \draw[->] (M) to node[auto,labelsize] {$\varepsilon_C$} (R); \end{tikzpicture}
  • The natural transformation (\delta'_{X,Y,C}\colon (Y\otimes_\mathcal{N}X)\ast' C\longrightarrow Y\ast'(X\ast' C))_{X,Y\in\mathcal{N},C\in\mathcal{C}} is defined by \delta'_{X,Y,C}=\delta_{GX,GY,C}\circ (g_{X,Y}\ast C):

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$G(Y\otimes_\mathcal{N}X)\ast C$}; \node (M) at (4.5,0) {$(GY\otimes_\mathcal{M}GX)\ast C$}; \node (R) at (9,0) {$GY\ast(GX\ast{C})$.}; \draw[->] (L) to node[auto,labelsize] {$g_{X,Y}\ast C$} (M); \draw[->] (M) to node[auto,labelsize] {$\delta_{GX,GY,C}$} (R); \end{tikzpicture} \qedhere
Definition

Definition 3.29

W8U9

Let \mathcal{M} be a large monoidal category.

  1. Let {\mathscr{E}\!nrich^{\mathrm{r}}(\mathcal{M})} be the full sub-2-category of {\mathscr{E}\!nrich(\mathcal{M})} consisting of all enrichments (\mathcal{C},{\langle -, -\rangle},j,M) such that for each C\in\mathcal{C}, {\langle C, -\rangle} is a right adjoint.

  2. Let {\mathscr{A}\!ct^{\mathrm{l}}_{\mathrm{oplax}}(\mathcal{M})} be the full sub-2-category of {\mathscr{A}\!ct_{\mathrm{oplax}}(\mathcal{M})} consisting of all oplax actions (\mathcal{C},\ast,\varepsilon,\delta) such that for each C\in\mathcal{C}, -\ast C is a left adjoint.

Example

Example 3.30

DLOW

Let \mathcal{C} be a locally small category with all small powers. Recall the strict action

\ast\colon[\mathcal{C},\mathcal{C}]\times\mathcal{C}\longrightarrow\mathcal{C}

of the monoidal category [\mathcal{C},\mathcal{C}] of endofunctors on \mathcal{C} on \mathcal{C}, used to capture Eilenberg–Moore algebras of monads on \mathcal{C}. For any object C\in\mathcal{C}, write by {\lceil C\rceil}\colon 1\longrightarrow\mathcal{C} the functor from the terminal category 1 which maps the unique object of 1 to C\in\mathcal{C} ({\lceil C\rceil} is sometimes called the name of C).

By the assumptions on \mathcal{C}, for any object A\in\mathcal{C} the functor -\ast A (which may be seen as the precomposition by {\lceil A\rceil}\colon 1\longrightarrow\mathcal{C}) admits a right adjoint {\langle A, -\rangle}, which maps any B\in\mathcal{C} (equivalently, {\lceil B\rceil}\colon 1\longrightarrow\mathcal{C}) to the right Kan extension {\langle A, B\rangle}=\mathrm{Ran}_{{\lceil A\rceil}}{\lceil B\rceil} of {\lceil B\rceil} along {\lceil A\rceil}. The functor \mathrm{Ran}_{{\lceil A\rceil}}{\lceil B\rceil}\colon\mathcal{C}\longrightarrow\mathcal{C} maps C\in\mathcal{C} to \mathrm{Ran}_{{\lceil A\rceil}}{\lceil B\rceil}(C)=B^{\mathcal{C}(C,A)}.

For any object C\in\mathcal{C}, \mathrm{Ran}_{{\lceil C\rceil}}{\lceil C\rceil} exists and becomes a monad on \mathcal{C} in a canonical way (the codensity monad of {\lceil C\rceil}). For any monad \mathsf{T} on \mathcal{C}, to give a structure of an Eilenberg–Moore algebra on C\in\mathcal{C} is equivalent to give a monad morphism from \mathsf{T} to \mathrm{Ran}_{{\lceil C\rceil}}{\lceil C\rceil}. This observation is in e.g., [Kelly_coherence_lax_dist, Section 3].

In particular, if we take \mathcal{C}=\mathbf{Set}, we see that the above enrichment agrees with the one given in Example 3.17. Hence the notion of relative algebra [Hino] agrees with that of Eilenberg–Moore algebra in this case.

Definition

Definition 3.31

PWJB

A metatheory is a large monoidal category \mathcal{M}=(\mathcal{M},I,\otimes).

Definition

Definition 3.32

4GLZ

Let \mathcal{M} be a metatheory. A theory in \mathcal{M} is a monoid object \mathsf{T}=(T,e,m) in \mathcal{M}.

We denote the category of theories in \mathcal{M} by {\mathbf{Th}(\mathcal{M})}, which we define to be the same as {\mathbf{Mon}(\mathcal{M})}, the category of monoid objects in \mathcal{M}.

Definition

Definition 3.33

VWYM

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a large monoidal category. The convolution monoidal structure (\widehat{I},\mathbin{\widehat{\otimes}}) on the presheaf category \widehat{\mathcal{M}} =[\mathcal{M}^{\mathrm{op}},\mathbf{SET}] is defined as follows.

  • The unit object \widehat{I} is the representable functor \mathcal{M}(-,I)\colon \mathcal{M}^{\mathrm{op}}\longrightarrow\mathbf{SET}.

  • Given P,Q\in\widehat{\mathcal{M}}, their monoidal product Q\mathbin{\widehat{\otimes}} P\colon \mathcal{M}^{\mathrm{op}}\longrightarrow\mathbf{SET} maps Z\in\mathcal{M} to

    (Q\mathbin{\widehat{\otimes}} P)(Z)=\int^{X,Y\in\mathcal{M}} \mathcal{M}(Z,Y\otimes X) \times Q(Y)\times P(X).
Definition

Definition 3.34

68L7

We define the bicategory {\mathscr{P\!R\!O\!F}} as follows.

  • An object is a large category.

  • A 1-cell from \mathcal{A} to \mathcal{B} is a profunctor from \mathcal{A} to \mathcal{B}, which we define to be a functor

    H\colon \mathcal{B}^{\mathrm{op}}\times\mathcal{A}\longrightarrow\mathbf{SET}.

    We write H\colon \mathcal{A}\mathrel{\mathpalette\p@to@gets\to}\mathcal{B} if H is a profunctor from \mathcal{A} to \mathcal{B}. The identity 1-cell on a large category \mathcal{C} is the hom-functor \mathcal{C}(-,-). Given profunctors H\colon \mathcal{A}\mathrel{\mathpalette\p@to@gets\to}\mathcal{B} and K\colon \mathcal{B}\mathrel{\mathpalette\p@to@gets\to}\mathcal{C}, their composite K\odot H\colon\mathcal{A}\mathrel{\mathpalette\p@to@gets\to}\mathcal{C} maps (C,A)\in\mathcal{C}^{\mathrm{op}}\times\mathcal{A} to

    (K\odot H)(C,A)=\int^{B\in\mathcal{B}} K(C,B)\times H(B,A).
  • A 2-cell from H to H', both from \mathcal{A} to \mathcal{B}, is a natural transformation \alpha\colon H\Longrightarrow H' \colon\mathcal{B}^{\mathrm{op}}\times\mathcal{A}\longrightarrow\mathbf{SET}.

Definition

Definition 3.35

1FZR

Let \mathcal{C} be a large category. Define the monoidal category [\mathcal{C}^{\mathrm{op}}\times \mathcal{C},\mathbf{SET}] =([\mathcal{C}^{\mathrm{op}}\times\mathcal{C},\mathbf{SET}],\mathcal{C}(-,-),\mathbin{\odot^\mathrm{rev}}) of endo-profunctors on \mathcal{C} to be the endo-hom-category {\mathscr{P\!R\!O\!F}}^{\mathrm{op}}(\mathcal{C},\mathcal{C}). More precisely:

  • The unit object is the hom-functor \mathcal{C}(-,-)\colon \mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathbf{SET}.

  • Given H,K\colon\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathbf{SET}, define their monoidal product H\mathbin{\odot^\mathrm{rev}} K to be the functor which maps (A,C)\in\mathcal{C}^{\mathrm{op}}\times\mathcal{C} to

    (H\mathbin{\odot^\mathrm{rev}} K)(A,C)=\int^{B\in\mathcal{C}}H(B,C)\times K(A,B).\qedhere
Definition

Definition 3.36

LH0S

Let \mathcal{M}=(\mathcal{M},\otimes, I) be a metatheory. A metamodel of \mathcal{M} consists of:

  • a large category \mathcal{C};

  • a functor \Phi\colon \mathcal{M}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathbf{SET} (whose action we write as (X,A,B)\longmapsto \Phi_X(A,B));

  • a natural transformation ((\overline{\phi}_\cdot)_C\colon 1\longrightarrow\Phi_I(C,C))_{C\in\mathcal{C}};

  • a natural transformation

    ((\overline{\phi}_{X,Y})_{A,B,C}\colon \Phi_Y(B,C)\times\Phi_X(A,B) \longrightarrow\Phi_{Y\otimes X}(A,C))_{X,Y\in\mathcal{M},A,B,C\in\mathcal{C}},

making the following diagrams commute for all X,Y,Z\in\mathcal{M} and A,B,C,D\in\mathcal{C}:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$1\times \Phi_X(A,B)$}; \node (TR) at (6,1) {$\Phi_I(B,B)\times \Phi_X(A,B)$}; \node (BL) at (0,-1) {$\Phi_X(A,B)$}; \node (BR) at (6,-1) {$\Phi_{I\otimes X}(A,B)$}; \draw[->] (TL) to node[auto,labelsize](T) {$(\overline{\phi}_\cdot)_B\times \Phi_X(A,B)$} (TR); \draw[->] (TR) to node[auto,labelsize] {$(\overline{\phi}_{X,I})_{A,B,B}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,labelsize] {$\cong$} (BR); \end{tikzpicture}
\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$\Phi_X(A,B)\times 1$}; \node (TR) at (6,1) {$\Phi_X(A,B)\times\Phi_I(A,A)$}; \node (BL) at (0,-1) {$\Phi_X(A,B)$}; \node (BR) at (6,-1) {$\Phi_{X\otimes I}(A,B)$}; \draw[->] (TL) to node[auto,labelsize](T) {$\Phi_X(A,B)\times(\overline{\phi}_\cdot)_A$} (TR); \draw[->] (TR) to node[auto,labelsize] {$(\overline{\phi}_{I,X})_{A,A,B}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,labelsize] {$\cong$} (BR); \end{tikzpicture}
\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$\big(\Phi_Z(C,D)\times \Phi_Y(B,C)\big)\times \Phi_X(A,B)$}; \node (TM) at (8,2) {$\Phi_{Z\otimes Y}(B,D)\times \Phi_X(A,B)$}; \node (TR) at (8,0) {$\Phi_{(Z\otimes Y)\otimes X}(A,D)$}; \node (BL) at (0,0) {$\Phi_Z(C,D)\times \big(\Phi_Y(B,C)\times \Phi_X(A,B)\big)$}; \node (BM) at (0,-2) {$\Phi_Z(C,D)\times\Phi_{Y\otimes X}(A,C)$}; \node (BR) at (8,-2) {$\Phi_{Z\otimes (Y\otimes X)}(A,D).$}; \draw[->] (TL) to node[auto,labelsize](T) {$(\overline{\phi}_{Y,Z})_{B,C,D}\times\Phi_X(A,B)$} (TM); \draw[->] (TM) to node[auto,labelsize](T) {$(\overline{\phi}_{X,Z\otimes Y})_{A,B,D}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\cong$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,swap,labelsize] {$\Phi_Z(C,D)\times (\overline{\phi}_{X,Y})_{A,B,C}$} (BM); \draw[->] (BM) to node[auto,labelsize](B) {$(\overline{\phi}_{Y\otimes X,Z})_{A,C,D}$} (BR); \end{tikzpicture}

We say that (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) is a metamodel of \mathcal{M}, or that (\Phi,\overline{\phi}_\cdot,\overline{\phi}) is a metamodel of \mathcal{M} in \mathcal{C}.

Definition

Definition 3.37

SMFJ

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a metatheory, \mathsf{T}=(T,e,m) be a theory in \mathcal{M}, \mathcal{C} be a large category and \Phi=(\Phi,\overline{\phi}_\cdot,\overline{\phi}) be a metamodel of \mathcal{M} in \mathcal{C}.

  1. A model of \mathsf{T} in \mathcal{C} with respect to \Phi is a pair (C,\xi) consisting of an object C of \mathcal{C} and an element \xi\in \Phi_T(C,C) such that (\Phi_e)_{C,C}(\xi)=(\overline{\phi}_\cdot)_{C}(\ast) (where \ast is the unique element of 1) and (\Phi_m)_{C,C}(\xi)=(\overline{\phi}_{T,T})_{C,C,C}(\xi,\xi):

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(11) at (0,1.5) {$\Phi_T(C,C)$}; \node(12) at (2,0) {$\Phi_I(C,C)$}; \node(21) at (4,1.5) {$1$}; \draw [->] (11) to node [auto,swap,labelsize]{$(\Phi_e)_{C,C}$} (12); \draw [->] (21) to node [auto,labelsize]{$(\overline{\phi}_\cdot)_{C}$} (12); \end{tikzpicture} \quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(11) at (0,1.5) {$\Phi_T(C,C)$}; \node(12) at (2,0) {$\Phi_{T\otimes T}(C,C).$}; \node(21) at (4,1.5) {$\Phi_T(C,C)\times \Phi_T(C,C)$}; \draw [->] (11) to node [auto,swap,labelsize]{$(\Phi_m)_{C,C}$} (12); \draw [->] (21) to node [auto,labelsize]{$(\overline{\phi}_{T,T})_{C,C,C}$} (12); \end{tikzpicture}
  2. Let (C,\xi) and (C',\xi') be models of \mathsf{T} in \mathcal{C} with respect to \Phi. A homomorphism from (C,\xi) to (C',\xi') is a morphism f\colon C\longrightarrow C' in \mathcal{C} such that \Phi_T(C,f)(\xi)=\Phi_T(f,C')(\xi'):

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(11) at (0,1.5) {$\Phi_T(C,C)$}; \node(12) at (2,0) {$\Phi_T(C,C').$}; \node(21) at (4,1.5) {$\Phi_T(C',C')$}; \draw [->] (11) to node [auto,swap,labelsize]{$\Phi_T(C,f)$} (12); \draw [->] (21) to node [auto,labelsize]{$\Phi_T(f,C')$} (12); \end{tikzpicture}

We denote the (large) category of models of \mathsf{T} in \mathcal{C} with respect to \Phi by {\mathbf{Mod}(\mathsf{T},(\mathcal{C},\Phi))}.

Used by Proof
Example

Example 3.38

4V7D

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a metatheory, \mathcal{C} be a large category and ({\langle -, -\rangle},j,M) be an enrichment of \mathcal{C} over \mathcal{M}. This induces a metamodel (\Phi,\overline{\phi}_\cdot,\overline{\phi}) of \mathcal{M} in \mathcal{C} as follows.

  • The functor \Phi\colon\mathcal{M}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathbf{SET} maps (X,A,B)\in \mathcal{M}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C} to

    \Phi_X(A,B)=\mathcal{M}(X,{\langle A, B\rangle}).
  • For each C\in\mathcal{C}, (\overline{\phi}_\cdot)_C\colon 1\longrightarrow\Phi_I(C,C) is the name of j_C (i.e., (\overline{\phi}_\cdot)_C maps the unique element of the singleton 1 to {j_C}).

  • For each A,B,C\in\mathcal{C} and X,Y\in\mathcal{M}, the function (\overline{\phi}_{X,Y})_{A,B,C}\colon \Phi_Y(B,C)\times\Phi_X(A,B) \longrightarrow\Phi_{Y\otimes X}(A,C) maps g\colon Y\longrightarrow{\langle B, C\rangle} and f\colon X\longrightarrow{\langle A, B\rangle} to

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$Y\otimes X$}; \node (M) at (3,0) {${\langle B, C\rangle}\otimes {\langle A, B\rangle}$}; \node (R) at (6,0) {${\langle A, C\rangle}.$}; \draw[->] (L) to node[auto,labelsize](T) {$g\otimes f$} (M); \draw[->] (M) to node[auto,labelsize] {$M_{A,B,C}$} (R); \end{tikzpicture}

The definition of model and homomorphism (Definition 3.13) we derive from an enrichment may be seen as a special case of the corresponding definition (Definition 3.37) for metamodel.

Example

Example 3.39

ZNFT

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a metatheory, \mathcal{C} be a large category and (\ast,\varepsilon,\delta) be an oplax action of \mathcal{M} on \mathcal{C}. This induces a metamodel (\Phi,\overline{\phi}_\cdot,\overline{\phi}) of \mathcal{M} in \mathcal{C} as follows.

  • The functor \Phi\colon\mathcal{M}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathbf{SET} maps (X,A,B)\in \mathcal{M}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C} to

    \Phi_X(A,B)=\mathcal{C}(X\ast A,{B}).
  • For each C\in\mathcal{C}, (\overline{\phi}_\cdot)_C\colon 1\longrightarrow\Phi_I(C,C) is the name of \varepsilon_C.

  • For each A,B,C\in\mathcal{C} and X,Y\in\mathcal{M}, the function (\overline{\phi}_{X,Y})_{A,B,C}\colon \Phi_Y(B,C)\times\Phi_X(A,B) \longrightarrow\Phi_{Y\otimes X}(A,C) maps g\colon Y\ast{B}\longrightarrow{C} and f\colon X\ast{A}\longrightarrow{B} to

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (-0.5,0) {$(Y\otimes X)\ast A$}; \node (M) at (3,0) {$Y\ast(X\ast A)$}; \node (R) at (6,0) {$Y\ast B$}; \node (RR) at (8,0) {$C.$}; \draw[->] (L) to node[auto,labelsize](T) {$\delta_{X,Y,A}$} (M); \draw[->] (M) to node[auto,labelsize] {$Y\ast f$} (R); \draw[->] (R) to node[auto,labelsize] {$g$} (RR); \end{tikzpicture}

The definition of model and homomorphism (Definition 3.24) we derive from an oplax action may be seen as a special case of the corresponding definition (Definition 3.37) for metamodel.

Definition

Definition 3.40

31JY

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a metatheory. We define the (locally large) 2-category {\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})} of metamodels of \mathcal{M} as follows.

  • An object is a metamodel (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) of \mathcal{M}.

  • A 1-cell from (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) to (\mathcal{C'},\Phi',\overline{\phi'}_\cdot,\overline{\phi'}) is a functor G\colon \mathcal{C}\longrightarrow \mathcal{C'} together with a natural transformation (g_{X,A,B}\colon \Phi_X(A,B)\longrightarrow \Phi'_X(GA,GB))_{X\in\mathcal{M},A,B\in\mathcal{C}} making the following diagrams commute for all X,Y\in\mathcal{M} and A,B,C\in\mathcal{C}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$1$}; \node (TR) at (4,1) {$\Phi_I(C,C)$}; \node (BR) at (4,-1) {$\Phi'_I(GC,GC)$}; \draw[->] (TL) to node[auto,labelsize](T) {$(\overline{\phi}_\cdot)_{C}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$g_{I,C,C}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$(\overline{\phi'}_\cdot)_{GC}$} (BR); \end{tikzpicture}
    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$\Phi_Y(B,C)\times \Phi_X(A,B)$}; \node (TR) at (8,1) {$\Phi_{Y\otimes X}(A,C)$}; \node (BL) at (0,-1) {$\Phi'_Y(GB,GC)\times \Phi'_X(GA,GB)$}; \node (BR) at (8,-1) {$\Phi'_{Y\otimes X}(GA,GC).$}; \draw[->] (TL) to node[auto,labelsize](T) {$(\overline{\phi}_{X,Y})_{A,B,C}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$g_{Y\otimes X,A,C}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$g_{Y,B,C}\times g_{X,A,B}$} (BL); \draw[->] (BL) to node[auto,labelsize] {$(\overline{\phi'}_{X,Y})_{GA,GB,GC}$} (BR); \end{tikzpicture}
  • A 2-cell from (G,g) to (G',g'), both from (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) to (\mathcal{C'},\Phi',\overline{\phi'}_\cdot,\overline{\phi'}), is a natural transformation \theta\colon G\Longrightarrow G' making the following diagram commute for all X\in\mathcal{M} and A,B\in\mathcal{C}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$\Phi_X(A,B)$}; \node (TR) at (6,2) {$\Phi'_X(GA,GB)$}; \node (BL) at (0,0) {$\Phi'_X(G'A,G'B)$}; \node (BR) at (6,0) {$\Phi'_X(GA,G'B).$}; \draw[->] (TL) to node[auto,labelsize](T) {$g_{X,A,B}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\Phi'_X(GA,\theta_B)$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$g'_{X,A,B}$} (BL); \draw[->] (BL) to node[auto,labelsize] {$\Phi'_X(\theta_A,G'B)$} (BR); \end{tikzpicture} \qedhere
Proposition

Proposition 3.41

OKVN

Let \mathcal{M} be a metatheory. The construction given in Example 3.38 canonically extends to a fully faithful 2-functor

{\mathscr{E}\!nrich(\mathcal{M})}\longrightarrow{\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})}.

A metamodel (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) of \mathcal{M} is in the essential image of this 2-functor if and only if for each A,B\in\mathcal{C}, the functor

\Phi_{(-)}(A,B)\colon\mathcal{M}^{\mathrm{op}}\longrightarrow\mathbf{SET}

is representable.

Proof of Proposition 3.41

The construction of the 2-functor {\mathscr{E}\!nrich(\mathcal{M})}\longrightarrow{\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})} is straightforward. The rest can also be proved by a standard argument using the Yoneda lemma. We sketch the argument below.

Let us focus on the characterisation of the essential image. Suppose that (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) is a metamodel of \mathcal{M} such that for each A,B\in\mathcal{C}, the functor \Phi_{(-)}(A,B) is representable. From such a metamodel we obtain an enrichment ({\langle -, -\rangle},j,M) of \mathcal{C} over \mathcal{M} as follows. For each A,B\in\mathcal{C}, choose an object {\langle A, B\rangle}\in\mathcal{M} and an isomorphism \alpha_{A,B}\colon\mathcal{M}(-,{\langle A, B\rangle})\longrightarrow\Phi_{(-)}(A,B). By functoriality of \Phi, {\langle -, -\rangle} uniquely extends to a functor of type \mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathcal{M} while making (\alpha_{A,B})_{A,B\in\mathcal{C}} natural. For each C\in\mathcal{C}, (\overline{\phi}_\cdot)_C\colon 1\longrightarrow \Phi_I(C,C)\cong \mathcal{M}(I,{\langle C, C\rangle}) gives rise to a morphism j_C\colon I\longrightarrow{\langle C, C\rangle} in \mathcal{M}. For each A,B,C\in\mathcal{M}, consider the function

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TT) at (0,4.5) {$\mathcal{M}({\langle B, C\rangle},{\langle B, C\rangle})\times\mathcal{M}({\langle A, B\rangle}, {\langle A, B\rangle})$}; \node (T) at (0,3) {$\Phi_{{\langle B, C\rangle}}(B,C)\times\Phi_{\langle A, B\rangle}(A,B)$}; \node (L) at (0,1.5) {$\Phi_{{\langle B, C\rangle}\otimes{\langle A, B\rangle}}(A,C)$}; \node (LL) at (0,0) {$\mathcal{M}({\langle B, C\rangle}\otimes{\langle A, B\rangle}, {\langle A, C\rangle}).$}; \draw[->] (T) to node[auto,labelsize] {$(\overline{\phi}_{{\langle A, B\rangle},{\langle B, C\rangle}})_{A,B,C}$} (L); \draw[->] (TT) to node[auto,labelsize]{$(\alpha_{B,C})_{\langle B, C\rangle} \times(\alpha_{A,B})_{{\langle A, B\rangle}}$} (T); \draw[->] (L) to node[auto,labelsize]{$(\alpha_{A,C})_{{\langle B, C\rangle} \otimes{\langle A, B\rangle}}^{-1}$} (LL); \end{tikzpicture}

Let the image of ({\mathrm{id}_{{\langle B, C\rangle}}},{\mathrm{id}_{{\langle A, B\rangle}}}) under this function be M_{A,B,C}\colon {\langle B, C\rangle}\otimes{\langle A, B\rangle}\longrightarrow{\langle A, C\rangle}. The axioms of metamodel then shows that ({\langle -, -\rangle},j,M) is an enrichment.

Moreover, if we consider the metamodel induced from this enrichment (see Example 3.38), then it is isomorphic to our original (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}). In particular, for each X,Y\in\mathcal{M} and A,B,C\in\mathcal{C}, the function (\overline{\phi}_{X,Y})_{A,B,C} is completely determined by M_{A,B,C}, as in Example 3.38. To see this, note that for each f\in\mathcal{M}(X,{\langle A, B\rangle}) and g\in\mathcal{M}(Y,{\langle B, C\rangle}), the diagram

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TT1) at (7.5,4.5) {$\mathcal{M}(Y,{\langle B, C\rangle})\times\mathcal{M}(X,{\langle A, B\rangle})$}; \node (T1) at (7.5,3) {$\Phi_Y(B,C)\times\Phi_X(A,B)$}; \node (L1) at (7.5,1.5) {$\Phi_{Y\otimes X}(A,C)$}; \node (LL1) at (7.5,0) {$\mathcal{M}({\langle B, C\rangle}\otimes{\langle A, B\rangle}, {\langle A, C\rangle})$}; \node (TT) at (0,4.5) {$\mathcal{M}({\langle B, C\rangle},{\langle B, C\rangle})\times\mathcal{M}({\langle A, B\rangle}, {\langle A, B\rangle})$}; \node (T) at (0,3) {$\Phi_{{\langle B, C\rangle}}(B,C)\times\Phi_{\langle A, B\rangle}(A,B)$}; \node (L) at (0,1.5) {$\Phi_{{\langle B, C\rangle}\otimes{\langle A, B\rangle}}(A,C)$}; \node (LL) at (0,0) {$\mathcal{M}({\langle B, C\rangle}\otimes{\langle A, B\rangle}, {\langle A, C\rangle})$}; \draw[->] (T) to node[auto,swap,labelsize] {$(\overline{\phi}_{{\langle A, B\rangle},{\langle B, C\rangle}})_{A,B,C}$} (L); \draw[->] (TT) to node[auto,swap,labelsize]{$\alpha \times\alpha$} (T); \draw[->] (L) to node[auto,swap,labelsize]{$\alpha^{-1}$} (LL); \draw[->] (T1) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,B,C}$} (L1); \draw[->] (TT1) to node[auto,labelsize]{$\alpha \times\alpha$} (T1); \draw[->] (L1) to node[auto,labelsize]{$\alpha^{-1}$} (LL1); \draw[->] (TT) to node[auto,labelsize] {$\mathcal{M}(g,{\mathrm{id}_{}})\times\mathcal{M}(f,{\mathrm{id}_{}})$} (TT1); \draw[->] (T) to node[auto,labelsize] {$\Phi_g(B,C)\times\Phi_f(A,B)$} (T1); \draw[->] (L) to node[auto,labelsize] {$\Phi_{g\otimes f}(A,C)$} (L1); \draw[->] (LL) to node[auto,labelsize] {$\mathcal{M}(g\otimes f,{\mathrm{id}_{}})$} (LL1); \end{tikzpicture}

commutes. Hence by chasing the element ({\mathrm{id}_{{\langle B, C\rangle}}},{\mathrm{id}_{{\langle A, B\rangle}}}) in the top left set, we observe that (modulo the isomorphisms \alpha) (g,f) is mapped by (\overline{\phi}_{X,Y})_{A,B,C} to M_{A,B,C}\circ (g\otimes f).

Proposition

Proposition 3.42

W1EZ

Let \mathcal{M} be a metatheory. The construction given in Example 3.39 canonically extends to a fully faithful 2-functor

{\mathscr{A}\!ct_{\mathrm{oplax}}(\mathcal{M})}\longrightarrow{\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})}.

A metamodel (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) of \mathcal{M} is in the essential image of this 2-functor if and only if for each X\in\mathcal{M} and A\in\mathcal{C}, the functor

\Phi_X(A,-)\colon \mathcal{C}\longrightarrow\mathbf{SET}

is representable.

Proof of Proposition 3.42

Similar to the proof of Proposition 3.41.

In particular, given a metamodel (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) of \mathcal{M} such that for each X\in\mathcal{M} and A\in\mathcal{C}, the functor \Phi_X(A,-) is representable, we may construct an oplax action (\ast,\varepsilon,\delta) of \mathcal{C} as follows. For each X\in\mathcal{M} and A\in\mathcal{C}, choose an object X\ast A\in\mathcal{C} and an isomorphism \beta_{X,A}\colon \mathcal{C}(X\ast A,-) \longrightarrow\Phi_X(A,-). We easily obtain a functor \ast\colon\mathcal{M}\times\mathcal{C}\longrightarrow\mathcal{C} and a natural transformation (\varepsilon_C)_{C\in\mathcal{C}}. To get \delta, for each X,Y\in\mathcal{M} and A\in\mathcal{C} consider the function

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TT) at (0,4.5) {$\mathcal{C}(Y\ast (X\ast A),Y\ast (X\ast A))\times\mathcal{C} (X\ast A,X\ast A)$}; \node (T) at (0,3) {$\Phi_{Y}(X\ast A,Y\ast (X\ast A))\times\Phi_X(A,X\ast A)$}; \node (L) at (0,1.5) {$\Phi_{Y\otimes X}(A,Y\ast (X\ast A))$}; \node (LL) at (0,0) {$\mathcal{C}((Y\otimes X)\ast A, Y\ast (X\ast A)).$}; \draw[->] (T) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,X\ast A,Y\ast (X\ast A)}$} (L); \draw[->] (TT) to node[auto,labelsize]{$(\beta_{Y,X\ast A})_{Y\ast (X\ast A)} \times(\beta_{X,A})_{X\ast A}$} (T); \draw[->] (L) to node[auto,labelsize]{$(\beta_{Y\otimes X,A})_{Y\ast(X\ast A)}^{-1}$} (LL); \end{tikzpicture}

We define \delta_{X,Y,A}\colon (Y\otimes X)\ast A\longrightarrow Y\ast(X\ast A) to be the image of ({\mathrm{id}_{Y\ast (X\ast A)}},{\mathrm{id}_{X\ast A}}) under this function.

To verify that the metamodel induced from this oplax action (see Example 3.39) is isomorphic to (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}), essentially we only need to check that (\overline{\phi}_{X,Y})_{A,B,C} for each X,Y\in\mathcal{M} and A,B,C\in\mathcal{C} is determined by \delta_{X,Y,A} as in Example 3.39. Suppressing the isomorphisms \beta from now on, for each f\colon X\ast A\longrightarrow B and g\colon Y\ast B\longrightarrow C consider the following digram:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TT1) at (7.5,4) {$\mathcal{C}((Y\otimes X)\ast A,Y\ast (X\ast A))$}; \node (T1) at (7.5,2) {$\mathcal{C}((Y\otimes X)\ast A,C)$}; \node (L1) at (7.5,0) {$\mathcal{C}(Y\ast B,C)\times \mathcal{C}(X\ast A,B).$}; \node (TT) at (0,4) {$\mathcal{C}(Y\ast (X\ast A),Y\ast (X\ast A)) \times \mathcal{C}(X\ast A,X\ast A)$}; \node (T) at (0,2) {$\mathcal{C}(Y\ast (X\ast A),C)\times \mathcal{C}(X\ast A,X\ast A)$}; \node (L) at (0,0) {$\mathcal{C}(Y\ast B,C)\times \mathcal{C}(X\ast A,X\ast A)$}; \draw[<-] (T) to node[auto,swap,labelsize] {$\mathcal{C}(Y\ast f,{\mathrm{id}_{}})\times \mathcal{C}({\mathrm{id}_{}},{\mathrm{id}_{}})$} (L); \draw[->] (TT) to node[auto,swap,labelsize]{$\mathcal{C}({\mathrm{id}_{}},g\circ(Y\ast f))\times \mathcal{C}({\mathrm{id}_{}},{\mathrm{id}_{}})$} (T); \draw[<-] (T1) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,B,C}$} (L1); \draw[->] (TT1) to node[auto,labelsize]{$\mathcal{C}({\mathrm{id}_{}},g\circ(Y\ast f))$} (T1); \draw[->] (TT) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,X\ast A,Y\ast(X\ast A)}$} (TT1); \draw[->] (T) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,X\ast A,C}$} (T1); \draw[->] (L) to node[auto,labelsize] {$\mathcal{C}({\mathrm{id}_{}},{\mathrm{id}_{}})\times \mathcal{C}({\mathrm{id}_{}},f)$} (L1); \end{tikzpicture}

The top square commutes by naturality in C of ((\overline{\phi}_{X,Y})_{A,B,C}) and the bottom square commutes by (extra) naturality in B of it. By chasing the appropriate elements as follows

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TT1) at (6.5,3) {$\delta_{X,Y,A}$}; \node (T1) at (6.5,1.5) {$g\circ(Y\ast f)\circ \delta_{X,Y,A}$}; \node (L1) at (6.5,0) {$(g,f),$}; \node (TT) at (0,3) {$({\mathrm{id}_{Y\ast (X\ast A)}},{\mathrm{id}_{X\ast A}})$}; \node (T) at (0,1.5) {$(g\circ (Y\ast f), {\mathrm{id}_{X\ast A}})$}; \node (L) at (0,0) {$(g,{\mathrm{id}_{X\ast A}})$}; \draw[<-|] (T) to node[auto,swap,labelsize] {$\mathcal{C}(Y\ast f,{\mathrm{id}_{}})\times \mathcal{C}({\mathrm{id}_{}},{\mathrm{id}_{}})$} (L); \draw[|->] (TT) to node[auto,swap,labelsize]{$\mathcal{C}({\mathrm{id}_{}},g\circ(Y\ast f))\times \mathcal{C}({\mathrm{id}_{}},{\mathrm{id}_{}})$} (T); \draw[<-|] (T1) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,B,C}$} (L1); \draw[|->] (TT1) to node[auto,labelsize]{$\mathcal{C}({\mathrm{id}_{}},g\circ(Y\ast f))$} (T1); \draw[|->] (TT) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,X\ast A,Y\ast(X\ast A)}$} (TT1); \draw[|->] (T) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{A,X\ast A,C}$} (T1); \draw[|->] (L) to node[auto,labelsize] {$\mathcal{C}({\mathrm{id}_{}},{\mathrm{id}_{}})\times \mathcal{C}({\mathrm{id}_{}},f)$} (L1); \end{tikzpicture}

we conclude that (\overline{\phi}_{X,Y})_{A,B,C}(g,f)=g\circ(Y\ast f)\circ\delta_{X,Y,A}, as desired.

Corollary

Corollary 3.43

AVOO

Let \mathcal{M} be a metatheory.

  1. The 2-functors in Proposition 3.41 and Proposition 3.42 restrict to fully faithful 2-functors

    {\mathscr{E}\!nrich^{\mathrm{r}}(\mathcal{M})}\longrightarrow{\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})}\qquad {\mathscr{A}\!ct^{\mathrm{l}}_{\mathrm{oplax}}(\mathcal{M})}\longrightarrow{\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})}

    with the same essential image characterised as follows: a metamodel (\mathcal{C},\Phi,\overline{\phi}_\cdot,\overline{\phi}) of \mathcal{M} is in the essential image if and only if for each X\in\mathcal{M} and A,B\in\mathcal{C}, the functors

    \Phi_{(-)}(A,B)\colon\mathcal{M}^{\mathrm{op}}\longrightarrow\mathbf{SET}\qquad \Phi_X(A,-)\colon\mathcal{C}\longrightarrow\mathbf{SET}

    are representable.

  2. The 2-categories {\mathscr{E}\!nrich^{\mathrm{r}}(\mathcal{M})} and {\mathscr{A}\!ct^{\mathrm{l}}_{\mathrm{oplax}}(\mathcal{M})} are equivalent.

Proof of Corollary 3.43

The first clause is immediate from the definition of adjunction. For instance, an enrichment (\mathcal{C},{\langle -, -\rangle},j,M) over \mathcal{M} is in {\mathscr{E}\!nrich^{\mathrm{r}}(\mathcal{M})} if and only if for each A\in\mathcal{C}, {\langle A, -\rangle} is a right adjoint, which in turn is the case if and only if for each X\in\mathcal{M} and A\in\mathcal{C}, the functor

\mathcal{M}(X,{\langle A, -\rangle})\colon\mathcal{C}\longrightarrow\mathbf{SET}

is representable.

The second clause is a direct consequence of the first.

Proposition

Proposition 3.44

LA52

Let \mathcal{M} be a metatheory and \widehat{\mathcal{M}}=([\mathcal{M}^{\mathrm{op}},\mathbf{SET}],\widehat{I},\widehat{\otimes}) (see Definition 3.33). The 2-categories {\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})} and {\mathscr{E}\!nrich(\widehat{\mathcal{M}})} are canonically isomorphic.

Definition

Definition 3.45

SZVJ

Let \mathcal{M}=(\mathcal{M},I_\mathcal{M},\otimes_\mathcal{M}) and \mathcal{N}=(\mathcal{N},I_\mathcal{N},\otimes_\mathcal{N}) be metatheories. A morphism of metatheories from \mathcal{M} to \mathcal{N} is a lax monoidal functor

H=(H,h_\cdot,h)\colon\mathcal{N}^{\mathrm{op}}\times\mathcal{M}\longrightarrow\mathbf{SET}.

More precisely, such a morphism consists of:

  • a functor H\colon\mathcal{N}^{\mathrm{op}}\times\mathcal{M}\longrightarrow\mathbf{SET};

  • a function h_\cdot\colon1\longrightarrow H(I_\mathcal{N},I_\mathcal{M});

  • a natural transformation (h_{N,N',M,M'}\colon H(N',M')\times H(N,M)\longrightarrow H(N'\otimes_\mathcal{N} N,M'\otimes_\mathcal{M} M))_{N,N'\in\mathcal{N},M,M'\in\mathcal{M}}

making the following diagrams commute for each N,N',N''\in\mathcal{N} and M,M',M''\in\mathcal{M} (we omit subscripts on \otimes):

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$1\times H(N,M)$}; \node (TR) at (6,1) {$H(I_\mathcal{N},I_\mathcal{M})\times H(N,M)$}; \node (BL) at (0,-1) {$H(N,M)$}; \node (BR) at (6,-1) {$H(I_\mathcal{N}\otimes N,I_\mathcal{M}\otimes M)$}; \draw[->] (TL) to node[auto,labelsize](T) {$h_\cdot\times H(N,M)$} (TR); \draw[->] (TR) to node[auto,labelsize] {$h_{N,I_\mathcal{N},M,I_\mathcal{M}}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,labelsize] {$\cong$} (BR); \end{tikzpicture}
\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$H(N,M)\times 1$}; \node (TR) at (6,1) {$H(N,M)\times H(I_\mathcal{N},I_\mathcal{M})$}; \node (BL) at (0,-1) {$H(N,M)$}; \node (BR) at (6,-1) {$H(N\otimes I_\mathcal{N},M\otimes, I_\mathcal{M})$}; \draw[->] (TL) to node[auto,labelsize](T) {$H(N,M)\times h_\cdot$} (TR); \draw[->] (TR) to node[auto,labelsize] {$h_{I_\mathcal{N},N,I_\mathcal{M},M}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,labelsize] {$\cong$} (BR); \end{tikzpicture}
\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,2) {$\big(H(N'',M'')\times H(N',M')\big)\times H(N,M)$}; \node (TM) at (8,2) {$H(N''\otimes N',M''\otimes M')\times H(N,M)$}; \node (TR) at (8,0) {$H((N''\otimes N')\otimes N, (M''\otimes M')\otimes M)$}; \node (BL) at (0,0) {$H(N'',M'')\times \big(H(N',M')\times H(N,M)\big)$}; \node (BM) at (0,-2) {$H(N'',M'')\times H(N'\otimes N,M'\otimes M)$}; \node (BR) at (8,-2) {$H(N''\otimes(N'\otimes N),M''\otimes (M'\otimes M)).$}; \draw[->] (TL) to node[auto,labelsize](T) {$h_{N',N'',M',M''}\times H(N,M)$} (TM); \draw[->] (TM) to node[auto,labelsize](T) {$h_{N,N''\otimes N',M,M''\otimes M'}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\cong$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\cong$} (BL); \draw[->] (BL) to node[auto,swap,labelsize] {$H(N'',M'')\times h_{N,N',M,M'}$} (BM); \draw[->] (BM) to node[auto,labelsize](B) {$h_{N'\otimes N,N'',M'\otimes M,M''}$} (BR); \end{tikzpicture}

We write H\colon\mathcal{M}\mathrel{\mathpalette\p@to@gets\to}\mathcal{N} if H is a morphism of metatheories from \mathcal{M} to \mathcal{N}.

Definition

Definition 3.46

ONSA

We define the bicategory {\mathscr{M}\!\mathscr{T\!H}} of metatheories as follows.

  • An object is a metatheory.

  • A 1-cell from \mathcal{M} to \mathcal{N} is a morphism of metatheories \mathcal{M}\mathrel{\mathpalette\p@to@gets\to}\mathcal{N}. The identity 1-cell on a metatheory \mathcal{M} is the hom-functor \mathcal{M}(-,-), equipped with the evident structure for a morphism of metatheories. Given morphisms of metatheories (H,h_\cdot,h)\colon \mathcal{M}\mathrel{\mathpalette\p@to@gets\to}\mathcal{N} and (K,k_\cdot,k)\colon \mathcal{N}\mathrel{\mathpalette\p@to@gets\to}\mathcal{L}, their composite is (K\odot H,k_\cdot\odot h_\cdot, k \odot h) \colon \mathcal{M}\mathrel{\mathpalette\p@to@gets\to}\mathcal{L} where K\odot H is the composition of the profunctors H and K (Definition 3.34), and k_\cdot \odot h_\cdot and k\odot h are the evident natural transformations.

  • A 2-cell from H to H', both from \mathcal{M} to \mathcal{N}, is a monoidal natural transformation \alpha\colon H\Longrightarrow H'\colon\mathcal{N}^{\mathrm{op}}\times\mathcal{M}\longrightarrow\mathbf{SET}.

Definition

Definition 3.47

4N1K

Let \mathcal{M}=(\mathcal{M},I_\mathcal{M},\otimes_\mathcal{M}) and \mathcal{N}=(\mathcal{N},I_\mathcal{N},\otimes_\mathcal{N}) be metatheories, H=(H,h_\cdot,h)\colon\mathcal{M}\mathrel{\mathpalette\p@to@gets\to}\mathcal{N} a morphism of metatheories, \mathcal{C} a large category and \Phi=(\Phi,\overline{\phi}_\cdot,\overline{\phi}) a metamodel of \mathcal{M} in \mathcal{C}. We define the metamodel H(\Phi)=(\Phi',\overline{\phi'}_\cdot,\overline{\phi'}) of \mathcal{N} on \mathcal{C} as follows:

  • The functor \Phi'\colon\mathcal{N}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathbf{SET} maps (N,A,B)\in\mathcal{N}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C} to the set

    \Phi'_N(A,B)= \int^{M\in\mathcal{M}}H(N,M)\times \Phi_M(A,B).
  • The natural transformation ((\overline{\phi'}_\cdot)_C\colon 1\longrightarrow \Phi'_{I_\mathcal{N}}(C,C))_{C\in\mathcal{C}} is defined by mapping the unique element \ast of 1 to

    \begin{gathered} [I_\mathcal{M}\in\mathcal{M}, h_\cdot(\ast)\in H(I_\mathcal{N},I_\mathcal{M}), (\overline{\phi}_\cdot)_C(\ast)\in \Phi_{I_\mathcal{M}}(C,C)]\\ \in\int^{M\in\mathcal{M}}H(I_\mathcal{N},M)\times \Phi_M(C,C) \end{gathered}

    for each C\in\mathcal{C}.

  • The natural transformation

    ((\overline{\phi'}_{N,N'})_{A,B,C}\colon \Phi'_{N'}(B,C)\times\Phi'_N(A,B)\longrightarrow \Phi'_{N'\otimes_\mathcal{N} N}(A,C))_{N,N'\in\mathcal{N},A,B,C\in\mathcal{C}}

    is defined by mapping a pair consisting of [M',x',y']\in\Phi'_{N'}(B,C) and [M,x,y]\in\Phi'_N(A,B) to

    [M'\otimes_\mathcal{M}M, h_{N,N',M,M'}(x',x), (\overline{\phi}_{M,M'})_{A,B,C}(y',y)]

    for each N,N'\in\mathcal{N} and A,B,C\in\mathcal{C}.

Example

Example 3.48

OER4

Recall from Section ?, where we have compared clones, symmetric operads and non-symmetric operads, that there is a chain of lax monoidal functors

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$[\mathbf{N},\mathbf{Set}]$}; \node (M) at (3.5,0) {$[\mathbf{P},\mathbf{Set}]$}; \node (R) at (7,0) {$[\mathbf{F},\mathbf{Set}]$.}; \draw[->] (L) to node[auto,labelsize] {$\mathrm{Lan}_J$} (M); \draw[->] (M) to node[auto,labelsize] {$\mathrm{Lan}_{J'}$} (R); \end{tikzpicture}

These functors, being left adjoints in {\mathscr{M}\!on\mathscr{C\!A\!T}_{\mathrm{lax}}}, are in fact strong monoidal [Kelly:doctrinal]. Theories are mapped as follows, as noted in Section ?:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {${\mathbf{Th}([\mathbf{N},\mathbf{Set}])}$}; \node (M) at (4.5,0) {${\mathbf{Th}([\mathbf{P},\mathbf{Set}])}$}; \node (R) at (9,0) {${\mathbf{Th}([\mathbf{F},\mathbf{Set}])}.$}; \draw[->] (L) to node[auto,labelsize] {${\mathbf{Th}(\mathrm{Lan}_J)}$} (M); \draw[->] (M) to node[auto,labelsize] {${\mathbf{Th}(\mathrm{Lan}_{J'})}$} (R); \end{tikzpicture}

In this case, the suitable 2-functors between 2-categories of metamodels can be given either as {\mathscr{M}\!\mathscr{M}\!od((\mathrm{Lan}_J)^\ast)} or {\mathscr{M}\!\mathscr{M}\!od(([J,\mathbf{Set}])_\ast)} (and similarly for J'), because (\mathrm{Lan}_J)^\ast\cong ([J,\mathbf{Set}])_\ast in {\mathscr{M}\!\mathscr{T\!H}}.

Used by Example 3.49
Example

Example 3.49

NLAV

Let us consider the relationship between clones and monads on \mathbf{Set}. The inclusion functor

J''\colon \mathbf{F}\longrightarrow\mathbf{Set}

induces a functor

\mathrm{Lan}_{J''}\colon[\mathbf{F},\mathbf{Set}]\longrightarrow[\mathbf{Set},\mathbf{Set}],

which naturally acquires the structure of a strong monoidal functor. The essential image of this functor is precisely the finitary endofunctors on \mathbf{Set}, i.e., those endofunctors preserving filtered colimits. The functor {\mathbf{Th}(\mathrm{Lan}_{J''})} maps a clone to a finitary monad on \mathbf{Set}, in accordance with the well-known correspondence between clones (= Lawvere theories) and finitary monads on \mathbf{Set} [Linton_equational]. Between the 2-categories of metamodels, we have a 2-functor

{\mathscr{M}\!\mathscr{M}\!od((\mathrm{Lan}_{J''})^\ast)}\colon{\mathscr{M}\!\mathscr{M}\!od([\mathbf{Set},\mathbf{Set}])}\longrightarrow {\mathscr{M}\!\mathscr{M}\!od([\mathbf{F},\mathbf{Set}])}.

The standard metamodel of [\mathbf{Set},\mathbf{Set}] in \mathbf{Set} (corresponding to the definition of Eilenberg–Moore algebras) is given by the strict action described in Example 3.25; in particular, its functor part \Phi\colon [\mathbf{Set},\mathbf{Set}]^{\mathrm{op}}\times\mathbf{Set}^{\mathrm{op}}\times\mathbf{Set}\longrightarrow\mathbf{SET} maps (F,A,B) to \mathbf{Set}(FA,B). The metamodel (\mathrm{Lan}_{J''})^\ast(\Phi) of [\mathbf{F},\mathbf{Set}] in \mathbf{Set} has the functor part (\mathrm{Lan}_{J''})^\ast(\Phi)\colon[\mathbf{F},\mathbf{Set}]^{\mathrm{op}}\times\mathbf{Set}^{\mathrm{op}}\times \mathbf{Set}\longrightarrow\mathbf{SET} mapping (X,A,B) to

\begin{aligned} \mathbf{Set}((\mathrm{Lan}_{J''}X)A,B) &= \mathbf{Set}\left(\int^{[n]\in\mathbf{F}} A^n\times X_n,B\right)\\ &\cong \int_{[n]\in\mathbf{F}} \mathbf{Set} (X_n, \mathbf{Set}(A^n,B))\\ &\cong [\mathbf{F},\mathbf{Set}] (X, {\langle A, B\rangle}), \end{aligned}

where {\langle A, B\rangle}\in[\mathbf{F},\mathbf{Set}] in the final line is the one in Example 3.14. Hence {\mathscr{M}\!\mathscr{M}\!od((\mathrm{Lan}_{J''})^\ast)} preserves the standard metamodels and this way we restore the well-known observation that the classical correspondence of clones and finitary monads on \mathbf{Set} preserves semantics.

Note that by combining the previous example we obtain the chain

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$[\mathbf{N},\mathbf{Set}]$}; \node (M) at (2.5,0) {$[\mathbf{P},\mathbf{Set}]$}; \node (R) at (5,0) {$[\mathbf{F},\mathbf{Set}]$}; \node (RR) at (7.5,0) {$[\mathbf{Set},\mathbf{Set}]$}; \draw[->] (L) to node[auto,labelsize] {$\mathrm{Lan}_J$} (M); \draw[->] (M) to node[auto,labelsize] {$\mathrm{Lan}_{J'}$} (R); \draw[->] (R) to node[auto,labelsize] {$\mathrm{Lan}_{J''}$} (RR); \end{tikzpicture}

of strong monoidal functors, connecting non-symmetric and symmetric operads with monads on \mathbf{Set}.

Example

Example 3.50

XE0B

Let \mathcal{M} be a metatheory, \mathcal{C} a large category, and \ast a pseudo action of \mathcal{M} on \mathcal{C}. We obtain a strong monoidal functor

F\colon\mathcal{M}\longrightarrow[\mathcal{C},\mathcal{C}]

(where [\mathcal{C},\mathcal{C}] is equipped with the composition monoidal structure) as the transpose of \ast\colon\mathcal{M}\times\mathcal{C}\longrightarrow\mathcal{C}. The functor {\mathbf{Th}(F)} maps any theory \mathsf{T}=(T,e,m) in \mathcal{M} to the monad F(\mathsf{T})=(T\ast(-), e\ast(-),m\ast(-)) on \mathcal{C}. The 2-functor {\mathscr{M}\!\mathscr{M}\!od(F^\ast)}\colon{\mathscr{M}\!\mathscr{M}\!od([\mathcal{C},\mathcal{C}])}\longrightarrow{\mathscr{M}\!\mathscr{M}\!od(\mathcal{M})} maps the standard metamodel \Phi of [\mathcal{C},\mathcal{C}] in \mathcal{C} (Example 3.25) to the metamodel F^\ast(\Phi)\colon \mathcal{M}^{\mathrm{op}}\times\mathcal{C}^{\mathrm{op}}\times\mathcal{C}\longrightarrow\mathbf{SET} mapping (X,A,B) to

\mathcal{C}((FX)A,B)=\mathcal{C}(X\ast A,B).

Therefore it maps the standard metamodel \Phi to the metamodel induced from \ast.

As a special case, for a large category \mathcal{C} with finite limits and a cartesian monad \mathsf{S} on \mathcal{C}, the standard metamodel for \mathsf{S}-operads (Example 3.26) may be related to the standard metamodel of monads on \mathcal{C}, and models of an \mathsf{S}-operad \mathsf{T} may alternatively be defined as Eilenberg–Moore algebras of the monad on \mathcal{C} induced from \mathsf{T} (as noted in [Leinster_book]).

Theorem

Theorem 4.1

NP5Z

Let \mathcal{M} be a metatheory, \mathcal{C} be a large category and \Phi=(\Phi,\overline{\phi}_\cdot,\overline{\phi}) be a metamodel of \mathcal{M} in \mathcal{C}. The functors \mathrm{Sem} and \mathrm{Str} defined above form an adjunction:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(11) at (0,0) {${\mathbf{Th}(\widehat{\mathcal{M}})}^{\mathrm{op}}$}; \node(22) at (4,0) {${\mathbf{CAT}}/\mathcal{C}$.}; \draw [->,transform canvas={yshift=5pt}] (22) to node [auto,swap,labelsize]{$\mathrm{Str}$} (11); \draw [->,transform canvas={yshift=-5pt}] (11) to node [auto,swap,labelsize]{$\mathrm{Sem}$} (22); \path (11) to node[midway](m){} (22); \node at (m) [labelsize,rotate=90] {$\vdash$}; \end{tikzpicture}
Proof of Theorem 4.1

We show that there are bijections

{\mathbf{Th}(\widehat{\mathcal{M}})}(\mathsf{P},\mathrm{Str}(V))\cong ({\mathbf{CAT}}/\mathcal{C})(V,\mathrm{Sem}(\mathsf{P}))

natural in \mathsf{P}=(P,e,m)\in{\mathbf{Th}(\widehat{\mathcal{M}})} and (V\colon \mathcal{A}\longrightarrow\mathcal{C})\in{\mathbf{CAT}}/\mathcal{C}.

In fact, we show that the following three types of data naturally correspond to each other.

  1. A morphism \alpha\colon \mathsf{P}\longrightarrow\mathrm{Str}(V) in {\mathbf{Th}(\widehat{\mathcal{M}})}; that is, a natural transformation

    (\alpha_X\colon P(X)\longrightarrow P^{(V)}(X))_{X\in\mathcal{M}}

    making the suitable diagrams commute.

  2. A natural transformation

    (\xi_{A,X}\colon P(X)\longrightarrow \Phi_X(VA,VA))_{X\in\mathcal{M}, A\in\mathcal{A}}

    making the following diagrams commute for each A\in\mathcal{A} and X,Y\in\mathcal{M}:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$1$}; \node (TR) at (2,1) {$P(I)$}; \node (BR) at (2,-1) {$\Phi_I(VA,VA)$}; \draw[->] (TL) to node[auto,labelsize](T) {$\overline{e}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\xi_{A,I}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$(\overline{\phi}_\cdot)_{VA}$} (BR); \end{tikzpicture} \quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1) {$P(Y)\times P(X)$}; \node (TR) at (5.5,1) {$P({Y\otimes X})$}; \node (BL) at (0,-1) {$\Phi_Y(VA,VA)\times \Phi_X(VA,VA)$}; \node (BR) at (5.5,-1) {$\Phi_{Y\otimes X}(VA,VA).$}; \draw[->] (TL) to node[auto,labelsize](T) {$\overline{m}_{X,Y}$} (TR); \draw[->] (TR) to node[auto,labelsize] {$\xi_{A,Y\otimes X}$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\xi_{A,Y}\times \xi_{A,X}$} (BL); \draw[->] (BL) to node[auto,labelsize] {$(\overline{\phi}_{X,Y})_{VA,VA,VA}$} (BR); \end{tikzpicture}
  3. A morphism F\colon V\longrightarrow\mathrm{Sem}(\mathsf{P}) in {\mathbf{CAT}}/\mathcal{C}; that is, a functor F\colon\mathcal{A}\longrightarrow{\mathbf{Mod}(\mathsf{P},(\mathcal{C},\Phi))} such that U\circ F=V (U\colon{\mathbf{Mod}(\mathsf{P},(\mathcal{C},\Phi))}\longrightarrow\mathcal{C} is the forgetful functor).

The correspondence between 1 and 2 is by the universality of ends (see (?)). To give \xi as in 2 without requiring naturality in A\in\mathcal{A}, is equivalent to give a function {\mathrm{ob}(F)}\colon {\mathrm{ob}(\mathcal{A})}\longrightarrow{\mathrm{ob}({\mathbf{Mod}(\mathsf{P},(\mathcal{C},\Phi))})} such that {\mathrm{ob}(U)}\circ {\mathrm{ob}(F)}={\mathrm{ob}(V)} (see (?)). To say that \xi is natural also in A\in\mathcal{A} is equivalent to saying that {\mathrm{ob}(F)} extends to a functor F\colon \mathcal{A}\longrightarrow{\mathbf{Mod}(\mathsf{P},(\mathcal{C},\Phi))} by mapping each morphism f in \mathcal{A} to Vf.

Definition

Definition 5.1

7N32

A pseudo double category \mathbb{D} consists of the following data.

  • (DD1) A category \mathbb{D}_0, whose objects are called objects of \mathbb{D} and whose morphisms vertical morphisms of \mathbb{D}.

  • (DD2) A category \mathbb{D}_1, whose objects are called horizontal morphisms of \mathbb{D} and whose morphisms squares of \mathbb{D}.

  • (DD3) Functors

    \begin{aligned} s,t&\colon \mathbb{D}_1\longrightarrow\mathbb{D}_0,\\ I&\colon \mathbb{D}_0\longrightarrow \mathbb{D}_1,\\ \otimes&\colon\mathbb{D}_2\longrightarrow\mathbb{D}_1, \end{aligned}

    where \mathbb{D}_2 is the pullback

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1.5) {$\mathbb{D}_2$}; \node (TR) at (1.5,1.5) {$\mathbb{D}_1$}; \node (BL) at (0,0) {$\mathbb{D}_1$}; \node (BR) at (1.5,0) {$\mathbb{D}_0$}; \draw[->] (TL) to node[auto,labelsize](T) {$\pi_2$} (TR); \draw[->] (TR) to node[auto,labelsize] {$t$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$\pi_1$} (BL); \draw[->] (BL) to node[auto,swap,labelsize](B) {$s$} (BR); \draw (TL)++(0.2,-0.6)-- ++ (0.4,0) -- ++(0,0.4); \end{tikzpicture}

    of categories.

  • (DD4) Natural isomorphisms with components

    \begin{aligned} \mathfrak{a}_{X,Y,Z}&\colon (Z\otimes Y)\otimes X \longrightarrow Z\otimes(Y\otimes X),\\ \mathfrak{l}_X&\colon I_B\otimes X\longrightarrow X, \\ \mathfrak{r}_X&\colon X\otimes I_A\longrightarrow X \end{aligned}

    in \mathbb{D}_1, where (Z,Y,X)\in \mathbb{D}_3 which is the pullback

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1.5) {$\mathbb{D}_3$}; \node (TR) at (1.5,1.5) {$\mathbb{D}_1$}; \node (BL) at (0,0) {$\mathbb{D}_2$}; \node (BR) at (1.5,0) {$\mathbb{D}_0$}; \draw[->] (TL) to node[auto,labelsize](T) {} (TR); \draw[->] (TR) to node[auto,labelsize] {$t$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {} (BL); \draw[->] (BL) to node[auto,swap,labelsize](B) {$s\circ \pi_2$} (BR); \draw (TL)++(0.2,-0.6)-- ++ (0.4,0) -- ++(0,0.4); \end{tikzpicture}

    of categories and X\in \mathbb{D}_1 with s(X)=A and t(X)=B.

These data are subject to the following axioms.

  • (DA1) The diagrams

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1.5) {$\mathbb{D}_0$}; \node (BL) at (0,0) {$\mathbb{D}_1$}; \node (BR) at (1.5,0) {$\mathbb{D}_0$}; \node (BLL) at (-1.5,0) {$\mathbb{D}_0$}; \draw[->] (TL) to node[auto,labelsize](T) {${\mathrm{id}_{}}$} (BR); \draw[->] (TL) to node[auto,labelsize] {$I$} (BL); \draw[->] (BL) to node[auto,swap,labelsize](B) {$t$} (BR); \draw[->] (TL) to node[auto,swap,labelsize](T) {${\mathrm{id}_{}}$} (BLL); \draw[->] (BL) to node[auto,labelsize](B) {$s$} (BLL); \end{tikzpicture} \ \qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1.5) {$\mathbb{D}_2$}; \node (BL) at (0,0) {$\mathbb{D}_1$}; \node (BR) at (1.5,0) {$\mathbb{D}_0$}; \node (BLL) at (-1.5,0) {$\mathbb{D}_0$}; \draw[->] (TL) to node[auto,labelsize](T) {$t\circ \pi_1$} (BR); \draw[->] (TL) to node[auto,labelsize] {$\otimes$} (BL); \draw[->] (BL) to node[auto,swap,labelsize](B) {$t$} (BR); \draw[->] (TL) to node[auto,swap,labelsize](T) {$s\circ \pi_2$} (BLL); \draw[->] (BL) to node[auto,labelsize](B) {$s$} (BLL); \end{tikzpicture}

    commute (on the nose).

  • (DA2) The morphisms s(\mathfrak{a}_{X,Y,Z}),s(\mathfrak{l}_X) and s(\mathfrak{r}_X) are equal to {\mathrm{id}_{A}} for all (Z,Y,X) \in\mathbb{D}_3 and X\in\mathbb{D}_1, where A=s(X). Similarly for t.

  • (DA3) The coherence axioms (triangle and pentagon) for \mathfrak{a},\mathfrak{l} and \mathfrak{r}.

Example

Example 5.2

HU1C

Let \mathscr{B} be a bicategory. This induces a pseudo double category \mathbb{H}\mathscr{B}, given as follows:

  • an object of \mathbb{H}\mathscr{B} is an object of \mathscr{B};

  • all vertical morphisms of \mathbb{H}\mathscr{B} are vertical identity morphisms;

  • a horizontal morphism of \mathbb{H}\mathscr{B} is a 1-cell of \mathscr{B};

  • a square of \mathbb{H}\mathscr{B} is a 2-cell of \mathscr{B}.

The isomorphisms \mathfrak{a},\mathfrak{l} and \mathfrak{r} of \mathbb{H}\mathscr{B} is given by the corresponding iso-2-cells of \mathscr{B}.

Conversely, for any pseudo double category \mathbb{D}, we obtain a bicategory \mathscr{H}\mathbb{D} given as follows:

  • an object of \mathscr{H}\mathbb{D} is an object of \mathbb{D};

  • a 1-cell of \mathscr{H}\mathbb{D} is a horizontal morphism of \mathbb{D};

  • a 2-cell of \mathscr{H}\mathbb{D} is a square in \mathbb{D} whose horizontal source and target are both vertical identity morphisms.

Definition

Definition 5.3

OXXD

We define the pseudo double category {\mathbb{PROF}} as follows.

  • An object is a large category.

  • A vertical morphism from \mathcal{A} to \mathcal{A'} is a functor F\colon \mathcal{A}\longrightarrow\mathcal{A'}.

  • A horizontal morphism from \mathcal{A} to \mathcal{B} is a profunctor H\colon\mathcal{A}\mathrel{\mathpalette\p@to@gets\to} \mathcal{B}, i.e., a functor H\colon \mathcal{B}^{\mathrm{op}}\times\mathcal{A}\longrightarrow\mathbf{SET}. Horizontal identities and horizontal compositions are the same as in Definition 3.34.

  • A square as in

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1.5) {$\mathcal{A}$}; \node (TR) at (2,1.5) {$\mathcal{B}$}; \node (BL) at (0,0) {$\mathcal{A^\prime}$}; \node (BR) at (2,0) {$\mathcal{B^\prime}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$H$} (TR); \draw[->] (TR) to node[auto,labelsize] {$G$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$F$} (BL); \draw[pto] (BL) to node[auto,swap,labelsize](B) {$H^\prime$} (BR); \draw[2cell] (1,0.75)++(0,0.25) to node[auto,labelsize]{$\alpha$} ++(0,-0.5); \end{tikzpicture}

    is a natural transformation

    \alpha=(\alpha_{B,A}\colon H(B,A)\longrightarrow H'(GB,FA))_{B\in\mathcal{B},A\in\mathcal{A}},

    that is, of type

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (L) at (0,0) {$\mathcal{B}^{\mathrm{op}}\times\mathcal{A}$}; \node (T) at (2.5,-0.7) {$\mathcal{B'}^{\mathrm{op}}\times\mathcal{A'}$}; \node (R) at (5,0) {$\mathbf{SET}$.}; \draw[->, bend left=-5] (L) to node[auto,swap,labelsize]{$G^{\mathrm{op}}\times F$} (T); \draw[->, bend left=-5] (T) to node[auto,swap,labelsize]{$H'$} (R); \draw[->, bend left=20] (L) to node[auto,labelsize]{$H$} (R); \draw[2cell] (2.5,0)++(0,0.25) to node[auto,labelsize]{$\alpha$} ++(0,-0.5); \end{tikzpicture}

It is straightforward to define various compositions of these morphisms and squares. The isomorphisms \mathfrak{a},\mathfrak{l} and \mathfrak{r} are the same as those in the bicategory {\mathscr{P\!R\!O\!F}}. (Indeed, using the construction introduced in Example 5.2, {\mathscr{P\!R\!O\!F}}=\mathscr{H}{\mathbb{PROF}}.)

Definition

Definition 5.4

YCEM

Define a vertical double cone over \Phi(\mathsf{T}) to be a triple (\mathcal{A},V,v) consisting of a large category \mathcal{A}, a functor V\colon\mathcal{A}\longrightarrow\mathcal{C}, and a square v in {\mathbb{PROF}}^{\mathrm{op}} of type

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C},$}; \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto] (TL) to node[auto,labelsize] {$\mathcal{A}(-,-)$} (TR); \draw[pto] (BL) to node[auto,swap,labelsize] {$\Phi_T$} (BR); \draw[->] (TR) to node[auto,labelsize](B) {$V$} (BR); \draw[2cell] (1,0)++(0,0.25) to node[auto,labelsize]{$v$} ++(0,-0.5); \end{tikzpicture}

satisfying the following equations:

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$\mathcal{A}(-,-)$} (TR); \draw[->] (TR) to node[auto,labelsize] {$V$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto, bend left=30] (BL) to node[auto,labelsize](B) {$\Phi_T$} (BR); \draw[pto, bend right=30] (BL) to node[auto,swap,labelsize](B) {$\Phi_I$} (BR); \draw[2cell] (1,0.25)++(0,0.25) to node[auto,labelsize]{$v$} ++(0,-0.5); \draw[2cell] (1,-0.75)++(0,0.25) to node[auto,labelsize]{$\Phi_e$} ++(0,-0.5); \end{tikzpicture} \quad=\quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$\mathcal{A}(-,-)$} (TR); \draw[->] (TR) to node[auto,labelsize] {$V$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto, bend left=30] (BL) to node[auto,labelsize](B) {$\mathcal{C}(-,-)$} (BR); \draw[pto, bend right=30] (BL) to node[auto,swap,labelsize](B) {$\Phi_I$} (BR); \draw[2cell] (1,0.25)++(0,0.25) to node[auto,labelsize]{$I_{V}$} ++(0,-0.5); \draw[2cell] (1,-0.75)++(0,0.25) to node[auto,labelsize]{$\phi_\cdot$} ++(0,-0.5); \end{tikzpicture}
\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$\mathcal{A}(-,-)$} (TR); \draw[->] (TR) to node[auto,labelsize] {$V$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto, bend left=30] (BL) to node[auto,labelsize](B) {$\Phi_T$} (BR); \draw[pto, bend right=30] (BL) to node[auto,swap,labelsize](B) {$\Phi_{T\otimes T}$} (BR); \draw[2cell] (1,0.25)++(0,0.25) to node[auto,labelsize]{$v$} ++(0,-0.5); \draw[2cell] (1,-0.75)++(0,0.25) to node[auto,labelsize]{$\Phi_m$} ++(0,-0.5); \end{tikzpicture} \quad=\quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C}$}; \node (TRR) at (4,0.75) {$\mathcal{A}$}; \node (BRR) at (4,-0.75) {$\mathcal{C}$}; \node at (4.05,-0.75) {$\phantom{\mathcal{C}}$.}; \draw[pto] (TL) to node[auto,labelsize](T) {$\mathcal{A}(-,-)$} (TR); \draw[pto] (TR) to node[auto,labelsize](T2) {$\mathcal{A}(-,-)$} (TRR); \draw[->] (TR) to node[auto,labelsize] {$V$} (BR); \draw[->] (TRR) to node[auto,labelsize] {$V$} (BRR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto] (BL) to node[auto,labelsize](B) {$\Phi_T$} (BR); \draw[pto] (BR) to node[auto,labelsize](B) {$\Phi_T$} (BRR); \draw[pto, bend right=30] (BL) to node[auto,swap,labelsize](B) {$\Phi_{T\otimes T}$} (BRR); \draw[pto, bend left=30] (TL) to node[auto,labelsize](B) {$\mathcal{A}(-,-)$} (TRR); \draw[2cell] (1,0)++(0,0.25) to node[auto,labelsize]{$v$} ++(0,-0.5); \draw[2cell] (3,0)++(0,0.25) to node[auto,labelsize]{$v$} ++(0,-0.5); \draw[2cell] (2,-1.1)++(0,0.25) to node[auto,labelsize]{$\phi_{T,T}$} ++(0,-0.5); \draw[2cell] (2,1.1)++(0,0.25) to node[auto,labelsize]{$\cong$} ++(0,-0.5); \end{tikzpicture}
Theorem

Theorem 5.5

C73O

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a metatheory, \mathsf{T}=(T,e,m) be a theory in \mathcal{M}, \mathcal{C} be a large category, and \Phi=(\Phi,\phi_\cdot,\phi) be a metamodel of \mathcal{M} in \mathcal{C}. The triple ({\mathbf{Mod}(\mathsf{T},\mathcal{C})},U,u) defined above is a universal vertical double cone over \Phi(\mathsf{T}), namely:

  1. it is a vertical double cone over \Phi(\mathsf{T});

  2. for any vertical double cone (\mathcal{A},V,v) over \Phi(\mathsf{T}), there exists a unique functor K\colon\mathcal{A}\longrightarrow {\mathbf{Mod}(\mathsf{T},\mathcal{C})} such that

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$\mathcal{A}(-,-)$} (TR); \draw[->] (TR) to node[auto,labelsize] {$V$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto] (BL) to node[auto,swap,labelsize](B) {$\Phi_T$} (BR); \draw[2cell] (1,0)++(0,0.25) to node[auto,labelsize]{$v$} ++(0,-0.5); \end{tikzpicture} \quad=\quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1.5) {$\mathcal{A}$}; \node (TR) at (5,1.5) {$\mathcal{A}$}; \node (BL) at (0,0) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}$}; \node (BR) at (5,0) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}$}; \node (BBL) at (0,-1.5) {$\mathcal{C}$}; \node (BBR) at (5,-1.5) {$\mathcal{C}$}; \draw[pto] (TL) to node[auto,labelsize](T) {${\mathcal{A}}(-,-)$} (TR); \draw[->] (TR) to node[auto,labelsize] {$K$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$K$} (BL); \draw[pto] (BL) to node[auto,labelsize](B) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}(-,-)$} (BR); \draw[->] (BR) to node[auto,labelsize] {$U$} (BBR); \draw[->] (BL) to node[auto,swap,labelsize] {$U$} (BBL); \draw[pto] (BBL) to node[auto,swap,labelsize](B) {$\Phi_T$} (BBR); \draw[2cell] (2.5,0.75)++(0,0.25) to node[auto,labelsize]{$I_{K}$} ++(0,-0.5); \draw[2cell] (2.5,-0.75)++(0,0.25) to node[auto,labelsize]{$u$} ++(0,-0.5); \end{tikzpicture}

    holds;

  3. for any pair of vertical cones (\mathcal{A},V,v) and (\mathcal{A'},V',v') over \Phi(\mathsf{T}), any horizontal morphism H\colon \mathcal{A}\mathrel{\mathpalette\p@to@gets\to} \mathcal{A'} in {\mathbb{PROF}}^{\mathrm{op}} and any square

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A'}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$H$} (TR); \draw[->] (TR) to node[auto,labelsize] {$V'$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto] (BL) to node[auto,swap,labelsize](B) {$\mathcal{C}(-,-)$} (BR); \draw[2cell] (1,0)++(0,0.25) to node[auto,labelsize]{$\theta$} ++(0,-0.5); \end{tikzpicture}

    in {\mathbb{PROF}}^{\mathrm{op}} such that

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TM) at (2,0.75) {$\mathcal{A}$}; \node (TR) at (4,0.75) {$\mathcal{A'}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BM) at (2,-0.75) {$\mathcal{C}$}; \node (BR) at (4,-0.75) {$\mathcal{C}$}; \draw[pto, bend left=30] (TL) to node[auto,labelsize](T) {$H$} (TR); \draw[pto] (TL) to node[auto,labelsize](T) {$\mathcal{A}(-,-)$} (TM); \draw[pto] (TM) to node[auto,labelsize](T) {$H$} (TR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[->] (TM) to node[auto,labelsize] {$V$} (BM); \draw[->] (TR) to node[auto,labelsize] {$V'$} (BR); \draw[pto] (BL) to node[auto,swap,labelsize](B) {$\Phi_T$} (BM); \draw[pto] (BM) to node[auto,swap,labelsize](B) {$\mathcal{C}(-,-)$} (BR); \draw[pto, bend left=-30] (BL) to node[auto,swap,labelsize](T) {$\Phi_T$} (BR); \draw[2cell] (2,1.1)++(0,0.25) to node[auto,labelsize]{$\cong$} ++(0,-0.5); \draw[2cell] (1,0)++(0,0.25) to node[auto,labelsize]{$v$} ++(0,-0.5); \draw[2cell] (3,0)++(0,0.25) to node[auto,labelsize]{$\theta$} ++(0,-0.5); \draw[2cell] (2,-1.1)++(0,0.25) to node[auto,labelsize]{$\cong$} ++(0,-0.5); \end{tikzpicture} \ =\ \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TM) at (2,0.75) {$\mathcal{A'}$}; \node (TR) at (4,0.75) {$\mathcal{A'}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BM) at (2,-0.75) {$\mathcal{C}$}; \node (BR) at (4,-0.75) {$\mathcal{C}$}; \draw[pto, bend left=30] (TL) to node[auto,labelsize](T) {$H$} (TR); \draw[pto] (TL) to node[auto,labelsize](T) {$H$} (TM); \draw[pto] (TM) to node[auto,labelsize](T) {$\mathcal{A'}(-,-)$} (TR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[->] (TM) to node[auto,labelsize] {$V'$} (BM); \draw[->] (TR) to node[auto,labelsize] {$V'$} (BR); \draw[pto] (BL) to node[auto,swap,labelsize](B) {$\mathcal{C}(-,-)$} (BM); \draw[pto] (BM) to node[auto,swap,labelsize](B) {$\Phi_T$} (BR); \draw[pto, bend left=-30] (BL) to node[auto,swap,labelsize](T) {$\Phi_T$} (BR); \draw[2cell] (2,1.1)++(0,0.25) to node[auto,labelsize]{$\cong$} ++(0,-0.5); \draw[2cell] (1,0)++(0,0.25) to node[auto,labelsize]{$\theta$} ++(0,-0.5); \draw[2cell] (3,0)++(0,0.25) to node[auto,labelsize]{$v'$} ++(0,-0.5); \draw[2cell] (2,-1.1)++(0,0.25) to node[auto,labelsize]{$\cong$} ++(0,-0.5); \end{tikzpicture}

    holds, there exists a unique square

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (5,0.75) {$\mathcal{A'}$}; \node (BL) at (0,-0.75) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}$}; \node (BR) at (5,-0.75) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$H$} (TR); \draw[->] (TR) to node[auto,labelsize] {$K'$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$K$} (BL); \draw[pto] (BL) to node[auto,swap,labelsize](B) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}(-,-)$} (BR); \draw[2cell] (2.5,0)++(0,0.25) to node[auto,labelsize]{$\sigma$} ++(0,-0.5); \end{tikzpicture}

    in {\mathbb{PROF}}^{\mathrm{op}} such that

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,0.75) {$\mathcal{A}$}; \node (TR) at (2,0.75) {$\mathcal{A'}$}; \node (BL) at (0,-0.75) {$\mathcal{C}$}; \node (BR) at (2,-0.75) {$\mathcal{C}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$H$} (TR); \draw[->] (TR) to node[auto,labelsize] {$V'$} (BR); \draw[->] (TL) to node[auto,swap,labelsize] {$V$} (BL); \draw[pto] (BL) to node[auto,swap,labelsize](B) {$\mathcal{C}(-,-)$} (BR); \draw[2cell] (1,0)++(0,0.25) to node[auto,labelsize]{$\theta$} ++(0,-0.5); \end{tikzpicture} \quad =\quad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (TL) at (0,1.5) {$\mathcal{A}$}; \node (TR) at (5,1.5) {$\mathcal{A'}$}; \node (ML) at (0,0) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}$}; \node (MR) at (5,0) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}$}; \node (BL) at (0,-1.5) {${\mathcal{C}}$}; \node (BR) at (5,-1.5) {${\mathcal{C}}$}; \draw[pto] (TL) to node[auto,labelsize](T) {$H$} (TR); \draw[->] (TR) to node[auto,labelsize] {$K'$} (MR); \draw[->] (MR) to node[auto,labelsize] {$U$} (BR); \draw[->] (ML) to node[auto,swap,labelsize] {$U$} (BL); \draw[->] (TL) to node[auto,swap,labelsize] {$K$} (ML); \draw[pto] (ML) to node[auto,swap,labelsize](B) {${\mathbf{Mod}(\mathsf{T},\mathcal{C})}(-,-)$} (MR); \draw[pto] (BL) to node[auto,swap,labelsize]{${\mathcal{C}}(-,-)$} (BR); \draw[2cell] (2.5,0.75)++(0,0.25) to node[auto,labelsize]{$\sigma$} ++(0,-0.5); \draw[2cell] (2.5,-0.75)++(0,0.25) to node[auto,labelsize]{$I_{U}$} ++(0,-0.5); \end{tikzpicture}

    holds, where K and K' are the functors corresponding to (\mathcal{A},V,v) and (\mathcal{A'},V',v') respectively.

Proof (Proof of Theorem 5.5) of Theorem 5.5

First, that ({\mathbf{Mod}(\mathsf{T},\mathcal{C})},U,u) is a vertical double cone over \Phi(\mathsf{T}) follows directly from the definition of model of \mathsf{T} in \mathcal{C} with respect to \Phi (Definition 3.37).

Given a vertical double cone (\mathcal{A},V,v) over \Phi(\mathsf{T}), for each object A\in\mathcal{A}, the pair (VA,v_{A,A}({\mathrm{id}_{A}})) is a \mathsf{T}-model in \mathcal{C} with respect to \Phi, and for each morphism f\colon A\longrightarrow A' in \mathcal{A}, the morphism Vf is a \mathsf{T}-model homomorphism from (VA,v_{A,A}({\mathrm{id}_{A}})) to (VA',v_{A',A'}({\mathrm{id}_{A'}})). The functor K\colon \mathcal{A}\longrightarrow {\mathbf{Mod}(\mathsf{T},\mathcal{C})} can therefore be given as KA=(VA,v_{A,A}({\mathrm{id}_{A}})) and Kf=Vf. The uniqueness is clear.

Finally, given H and \theta as in the third clause, the equation (?) says that for each A\in\mathcal{A}, A'\in\mathcal{A'} and x\in H(A,A'), the morphism \theta_{A,A'}(x)\colon VA\longrightarrow V'A' in \mathcal{C} satisfies \Phi_T(VA,\theta_{A,A'}(x)) (v_{A,A}({\mathrm{id}_{A}}))= \Phi_T(\theta_{A,A'}(x),VA')(v'_{A',A'}({\mathrm{id}_{A'}})); in other words, that \theta_{A,A'}(x) is a \mathsf{T}-model homomorphism from KA to K'A'. The square \sigma can then be given as the natural transformation with \sigma_{A,A'}(x)=\theta_{A,A'}(x).

Definition

Definition 5.6

J4YF

We define the augmented simplex category (also known as the algebraists’ simplex category) \Delta_{a} as follows.

  • Objects are all finite ordinals \mathbf{n}=\{\,{0}<{1}<\dots <{n-1} \,\}, including the empty ordinal \mathbf{0}=\{\ \}.

  • Morphisms are all monotone functions.

Note that a morphism in \Delta_{a} is mono (resp. epi) iff it is an injective (resp. surjective) monotone function.

This category has a natural monoidal structure, given as follows.

  • The unit object is \mathbf{0}.

  • The monoidal product +\colon \Delta_{a}\times\Delta_{a}\longrightarrow\Delta_{a} maps a pair of objects \mathbf{n} and \mathbf{m} in \Delta_{a} to \mathbf{n+m}, and maps a pair of morphisms u\colon \mathbf{n}\longrightarrow \mathbf{n'} and v\colon \mathbf{m}\longrightarrow\mathbf{m'} in \Delta_{a} to u+v\colon \mathbf{n+m}\longrightarrow\mathbf{n'+m'} defined as

    (u+v) ({i}) =\begin{cases} u(i) & \text{if }i\leq n-1\\ n'+v(i) & \text{if }i\geq n. \end{cases}

In the following, whenever we talk about a monoidal structure on \Delta_{a}, we always mean this (strict) monoidal structure (\mathbf{0},+).

Proposition

Proposition 5.7

9GLE

Let \mathcal{M}=(\mathcal{M},I,\otimes) be a metatheory. There is an equivalence of categories between the category {\mathscr{M}\!on\mathscr{C\!A\!T}_{\mathrm{strong}}}(\Delta_{a},\mathcal{M}) of all strong monoidal functors \Delta_{a}\longrightarrow\mathcal{M} and monoidal natural transformations, and the category {\mathbf{Th}(\mathcal{M})}.

Proof of Proposition 5.7

Recall that a strong monoidal functor (F,f_\cdot,f)\colon \Delta_{a}\longrightarrow\mathcal{M} consists of a functor F\colon \Delta_{a}\longrightarrow\mathcal{M}, an isomorphism f_\cdot\colon I\longrightarrow F(\mathbf{0}) and a natural isomorphism

f=(f_{\mathbf{m},\mathbf{n}}\colon F(\mathbf{n})\otimes F(\mathbf{m})\longrightarrow F(\mathbf{n+m}))_{\mathbf{m},\mathbf{n}\in\Delta_{a}}

satisfying the suitable axioms. The functor

{\mathscr{M}\!on\mathscr{C\!A\!T}_{\mathrm{strong}}}(\Delta_{a},\mathcal{M})\longrightarrow {\mathbf{Th}(\mathcal{M})}

mapping an object (F,f_\cdot,f)\in{\mathscr{M}\!on\mathscr{C\!A\!T}_{\mathrm{strong}}}(\Delta_{a},\mathcal{M}) to (F(\mathbf{1}), F({!_\mathbf{0}})\circ f_\cdot, F({!_{\mathbf{2}}})\circ f_{\mathbf{1},\mathbf{1}}) and a morphism \phi\colon (F,f_\cdot,f)\longrightarrow (G,g_\cdot,g) in {\mathscr{M}\!on\mathscr{C\!A\!T}_{\mathrm{strong}}}(\Delta_{a},\mathcal{M}) to \phi_\mathbf{1} is well-defined and is an equivalence of categories.

Corollary

Corollary 5.8

27LT

Let \mathcal{M} be a metatheory, \mathsf{T} be a theory in \mathcal{M}, \mathcal{C} be a large category and \Phi be a metamodel of \mathcal{M} in \mathcal{C}. The category {\mathbf{Mod}(\mathsf{T},(\mathcal{C},\Phi))} of models of \mathsf{T} in \mathcal{C} with respect to \Phiis the apex of the double limit of the lax double functor \Phi(\mathsf{T}).

Definition

Definition 6.1 (cf. )

OE0G

A large category \mathcal{V} is extensive if and only if it admits all small coproducts and for any small set I and I-indexed family (X_i)_{i\in I} of objects of \mathcal{V}, the functor \coprod in (?) is an equivalence of categories.

Used by Proof
Definition

Definition 6.2

C95J

Let \mathcal{V} be a large category.

  1. A small \mathcal{V}-graph G consists of a small set {\mathrm{ob}(G)} together with, for each x,y\in{\mathrm{ob}(G)}, an object G(x,y)\in \mathcal{V}.

  2. A morphism of \mathcal{V}-graphs from G to G' is a function f\colon {\mathrm{ob}(G)}\longrightarrow{\mathrm{ob}(G')} together with, for each x,y\in{\mathrm{ob}(G)}, a morphism f_{x,y}\colon G(x,y)\longrightarrow G'(fx,fy) in \mathcal{V}.

Definition

Definition 6.3

RMHS

For any natural number n and any large category \mathcal{V}, the category {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} is defined as follows:

{{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(0)}=\mathcal{V};\qquad {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n+1)}= {{({{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)})}\mhyphen\mathbf{Gph}}.

An object of {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} is called an n-dimensional \mathcal{V}-graph.

Definition

Definition 6.4

FQFF

For each natural number n and any large category \mathcal{V} with finite products, the category {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)} is defined as follows (using the cartesian structure for enrichment):

{{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(0)}=\mathcal{V};\qquad {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n+1)}= {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Cat}}.

An object of {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)} is called a strict n-dimensional \mathcal{V}-category (to avoid confusion with weak n-dimensional \mathcal{V}-category which we are trying to define).

Proposition

Proposition 6.5

QEYN

If \mathcal{V} is a large category with a strict initial object 0, then {{\mathcal{V}}\mhyphen\mathbf{Gph}} is extensive.

Used by Proof
Proof of Proposition 6.5

The coproduct of a family (G_i)_{i\in I} of \mathcal{V}-graphs is given by {\mathrm{ob}(\coprod_{i\in I}G_i)}=\coprod_{i\in I}{\mathrm{ob}(G_i)} and

(\coprod_{i\in I}G_i) ((i,x), (i',x'))= \begin{cases} G_i(x,x')\quad &\text{if }i=i',\\ 0&\text{otherwise.} \end{cases}

It is easy to see that the functor \coprod\colon \prod_{i\in I}({{\mathcal{V}}\mhyphen\mathbf{Gph}}/G_i)\longrightarrow {{\mathcal{V}}\mhyphen\mathbf{Gph}}/(\coprod_{i\in I}G_i) (as in (?)) is full and faithful. For any object (f\colon H\longrightarrow \coprod_{i\in I}G_i) in {{\mathcal{V}}\mhyphen\mathbf{Gph}}/{(\coprod_{i\in I} G_i)}, define an object (f_i\colon H_i\longrightarrow G_i)_{i\in I}\in \prod_{i\in I}(\mathcal{V}/G_i) by the pullbacks of f along the coprojections \sigma_i\colon G_i\longrightarrow \coprod_{i\in I}G_i; note that these pullbacks always exist, and H_i are just the suitable “full sub” \mathcal{V}-graphs of H. Since 0 is strict, (\coprod_{i\in I}f_i \colon \coprod_{i\in I}H_i\longrightarrow \coprod_{i\in I}G_i) is isomorphic to f. Hence \coprod is also essentially surjective.

Proposition

Proposition 6.6

UCKD

If \mathcal{V} is a large category with a strict initial object and finite products, then {{\mathcal{V}}\mhyphen\mathbf{Cat}} is extensive.

Proof of Proposition 6.6

Coproducts in {{\mathcal{V}}\mhyphen\mathbf{Cat}} are formed just as in {{\mathcal{V}}\mhyphen\mathbf{Gph}}; namely, given a family (\mathcal{C}_i)_{i\in I} of \mathcal{V}-categories, we have {\mathrm{ob}(\coprod_{i\in I} \mathcal{C}_i)}=\coprod_{i\in I} {\mathrm{ob}(\mathcal{C}_i)} and

(\coprod_{i\in I}\mathcal{C}_i) ((i,x), (i',x'))= \begin{cases} \mathcal{C}_i(x,x')\quad &\text{if }i=i',\\ 0&\text{otherwise.} \end{cases}

Note that to define a composition law for \coprod_{i\in I}\mathcal{C}_i, we use the fact that for a category \mathcal{V} with a strict initial object 0, 0\times B\cong 0 for every object B\in\mathcal{V}.(In fact, for a category \mathcal{V} with an initial object 0 and finite products, 0 is strict if and only if 0\times B\cong 0 for every B\in \mathcal{V}.) The rest of the proof is identical to that of Proposition 6.5.

Proposition

Proposition 6.7

5KWS

Let \mathcal{V} have finite limits. A commutative square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$P$}; \node(1) at (2,1) {$B$}; \node(2) at (0,-1) {$A$}; \node(3) at (2,-1) {$X$}; \draw [->] (0) to node (t)[auto,labelsize] {$k$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$h$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$f$} (3); \end{tikzpicture}

in {{\mathcal{V}}\mhyphen\mathbf{Gph}} or in {{\mathcal{V}}\mhyphen\mathbf{Cat}} is a pullback if and only if the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {${\mathrm{ob}(P)}$}; \node(1) at (3,1) {${\mathrm{ob}(B)}$}; \node(2) at (0,-1) {${\mathrm{ob}(A)}$}; \node(3) at (3,-1) {${\mathrm{ob}(X)}$}; \draw [->] (0) to node (t)[auto,labelsize] {${k}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {${g}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {${h}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {${f}$} (3); \end{tikzpicture}

is a pullback in \mathbf{Set}, and for any pair p_1,p_2\in{\mathrm{ob}(P)}, writing a_i=h(p_i), b_i=k(p_i) and x_i=f(a_i)=g(b_i) for i=1,2, the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {${P}(p_1,p_2)$}; \node(1) at (3,1) {${B}(b_1,b_2)$}; \node(2) at (0,-1) {${A}(a_1,a_2)$}; \node(3) at (3,-1) {${X}(x_1,x_2)$}; \draw [->] (0) to node (t)[auto,labelsize] {$k_{p_1,p_2}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g_{b_1,b_2}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$h_{p_1,p_2}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$f_{a_1,a_2}$} (3); \end{tikzpicture}

is a pullback in \mathcal{V}.

Corollary

Corollary 6.8

FHDF

If \mathcal{V} is an extensive category with finite limits, then so are {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} and {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)}, for each natural number n.

Proposition

Proposition 6.9 (, cf. )

M3XW

A category \mathcal{V} with small coproducts is extensive if and only if it has all pullbacks along coprojections associated with small coproducts, and for any small set I, I-indexed family (X_i)_{i\in I} of objects of \mathcal{V}, morphism f\colon A\longrightarrow \coprod_{i\in I}X_i in \mathcal{V}, and I-indexed family of commutative squares

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$A_i$}; \node(1) at (2,1) {$A$}; \node(2) at (0,-1) {$X_i$}; \node(3) at (2,-1) {$\coprod_{i\in I}X_i$}; \draw [->] (0) to node (t)[auto,labelsize] {$\tau_i$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$f$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$f_i$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$\sigma_i$} (3); \end{tikzpicture}

in \mathcal{V} (in which \sigma_i is the i-th coprojection), each square (6.9) is a pullback square if and only if (\tau_i)_{i\in I} defines a coproduct (that is, A=\coprod_{i\in I} A_i with \tau_i the i-th coprojection).

Used by Proof, Proof
Proof of Proposition 6.9

If \mathcal{V} has small coproducts, then the functor (?) has a right adjoint if and only if all pullbacks along \sigma_i exists in \mathcal{V}, and in that case the right adjoint

\langle \sigma_i^\ast\rangle_{i\in I}\colon\mathcal{V}/\coprod_{i\in I}X_i\longrightarrow\prod_{i\in I}(\mathcal{V}/X_i)

has the i-th component \sigma_i^\ast\colon \mathcal{V}/\coprod_{i\in I}X_i\longrightarrow\mathcal{V}/X_i mapping (f\colon A\longrightarrow \coprod_{i\in I}X_i)\in \mathcal{V}/\coprod_{i\in I} X_i to (\sigma_i^\ast f\colon \sigma_i^\ast A\longrightarrow X_i)\in\mathcal{V}/X_i, defined by the pullback

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$\sigma_i^\ast A$}; \node(1) at (2,1) {$A$}; \node(2) at (0,-1) {$X_i$}; \node(3) at (2,-1) {$\coprod_{i\in I}X_i$}; \draw [->] (0) to node (t)[auto,labelsize] {} (1); \draw [->] (1) to node (r)[auto,labelsize] {$f$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\sigma_i^\ast f$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$\sigma_i$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture}

in \mathcal{V}.

In general, a functor is an equivalence of categories if and only if it has a right adjoint and the associated unit and counit are natural isomorphisms. Applying this fact to the functors of the form (?), we obtain the desired result.

Proposition

Proposition 6.10

1E5T

Let \mathcal{V} be an extensive category. For any small set I and I-indexed family of pullback squares in \mathcal{V} as on the left of the following diagram, the square as on the right is a pullback.

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$P_i$}; \node(1) at (2,1) {$B_i$}; \node(2) at (0,-1) {$A_i$}; \node(3) at (2,-1) {$X_i$}; \draw [->] (0) to node (t)[auto,labelsize] {$q_i$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g_i$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$p_i$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$f_i$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture} \qquad\qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$\coprod_{i\in I}P_i$}; \node(1) at (3,1) {$\coprod_{i\in I}B_i$}; \node(2) at (0,-1) {$\coprod_{i\in I}A_i$}; \node(3) at (3,-1) {$\coprod_{i\in I}X_i$}; \draw [->] (0) to node (t)[auto,labelsize] {$\coprod_{i\in I}q_i$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$\coprod_{i\in I}g_i$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\coprod_{i\in I}p_i$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$\coprod_{i\in I}f_i$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture}
Used by Proof, Proof, Proof
Proof of Proposition 6.10

By the definition of extensivity, the functor \coprod\colon \prod_{i\in I} (\mathcal{V}/X_i) \longrightarrow \mathcal{V}/(\coprod_{i\in I} X_i) is an equivalence of categories and, in particular, it preserves binary products.

Proposition

Proposition 6.11

WE1W

Let \mathcal{V} be an extensive category with finite products. For any B\in\mathcal{V}, the functor (-)\times B\colon \mathcal{V}\longrightarrow\mathcal{V} preserves small coproducts.

Used by Proof, Proof
Proof of Proposition 6.11

In any category, a square as on the left of the following diagram is always a pullback. Hence for any object B\in\mathcal{V}, small set I, and I-indexed family (X_i)_{i\in I} of objects of \mathcal{V}, for each i\in I the square as on the right is a pullback.

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$A\times B$}; \node(1) at (2,1) {$C\times B$}; \node(2) at (0,-1) {$A$}; \node(3) at (2,-1) {$C$}; \draw [->] (0) to node (t)[auto,labelsize] {$h\times B$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$\pi_1$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\pi_1$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$h$} (3); \end{tikzpicture} \qquad\qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$X_i\times B$}; \node(1) at (3,1) {$(\coprod_{i\in I}X_i)\times B$}; \node(2) at (0,-1) {$X_i$}; \node(3) at (3,-1) {$\coprod_{i\in I}X_i$}; \draw [->] (0) to node (t)[auto,labelsize] {$\sigma_i\times B$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$\pi_1$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\pi_1$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$\sigma_i$} (3); \end{tikzpicture}

Therefore by Proposition 6.9, (\coprod_{i\in I}X_i)\times B \cong \coprod_{i\in I}(X_i\times B).

Proposition

Proposition 6.12

36HS

Let \mathcal{V} be an extensive category. For any object Y\in\mathcal{V}, the slice category \mathcal{V}/Y is again extensive.

Used by Proof
Proof of Proposition 6.12

Clearly \mathcal{V}/Y has small coproducts given by \coprod_{i\in I}(f_i\colon X_i\longrightarrow Y) = ([f_i]_{i\in I}\colon \coprod_{i\in I} X_i\longrightarrow Y). Also note that for any object (f\colon X\longrightarrow Y) of \mathcal{V}/Y, the canonical functor (\mathcal{V}/Y)/f\longrightarrow \mathcal{V}/X which maps (h\colon (g\colon A\longrightarrow Y)\longrightarrow f)\in (\mathcal{V}/Y)/f to (h\colon A\longrightarrow X)\in \mathcal{V}/X is an isomorphism of categories. For any small set I and I-indexed family (f_i\colon X_i\longrightarrow Y)_{i\in I} of objects of \mathcal{V}/Y, the diagram

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1.5) {$\prod_{i\in I}((\mathcal{V}/Y)/f_i)$}; \node(1) at (5,1.5) {$(\mathcal{V}/Y)/[f_i]_{i\in I}$}; \node(2) at (0,0) {$\prod_{i\in I}(\mathcal{V}/X_i)$}; \node(3) at (5,0) {$\mathcal{V}/(\coprod_{i\in I}X_i)$}; \draw [->] (0) to node (t)[auto,labelsize] {$\coprod$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$\cong$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\cong$} (2); \draw [->] (2) to node (b)[auto,labelsize] {$\coprod$} (3); \end{tikzpicture}

(in which the vertical arrows are the canonical isomorphisms mentioned above) commutes. Since the lower \coprod is an equivalence by the assumption, so is the upper one.

Corollary

Corollary 6.13

U03X

Let \mathcal{V} be an extensive category with pullbacks.

  1. For any morphism g\colon B\longrightarrow X in \mathcal{V}, small set I, and I-indexed family of pullback squares in \mathcal{V} as on the left of the following diagram, the square as on the right is a pullback.

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$P_i$}; \node(1) at (2,1) {$B$}; \node(2) at (0,-1) {$A_i$}; \node(3) at (2,-1) {$X$}; \draw [->] (0) to node (t)[auto,labelsize] {$q_i$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$p_i$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$f_i$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture} \qquad\qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$\coprod_{i\in I}P_i$}; \node(1) at (3,1) {$B$}; \node(2) at (0,-1) {$\coprod_{i\in I}A_i$}; \node(3) at (3,-1) {$X$}; \draw [->] (0) to node (t)[auto,labelsize] {$[q_i]_{i\in I}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\coprod_{i\in I}p_i$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$[f_i]_{i\in I}$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture}
  2. For any object X\in\mathcal{V}, small set I, I-indexed family of morphisms (f_i\colon A_i\longrightarrow X)_{i\in I} in \mathcal{V}, small set J, J-indexed family of morphisms (g_j\colon B_j\longrightarrow X)_{j\in J} in \mathcal{V}, and (I\times J)-indexed family of pullback squares in \mathcal{V} as on the left of the following diagram, the square as on the right is a pullback.

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$P_{i,j}$}; \node(1) at (2,1) {$B_j$}; \node(2) at (0,-1) {$A_i$}; \node(3) at (2,-1) {$X$}; \draw [->] (0) to node (t)[auto,labelsize] {$q_{i,j}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g_j$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$p_{i,j}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$f_i$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture} \qquad\qquad \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$\coprod_{i\in I,j\in J}P_{i,j}$}; \node(1) at (4,1) {$\coprod_{j\in J}B_j$}; \node(2) at (0,-1) {$\coprod_{i\in I}A_i$}; \node(3) at (4,-1) {$X$}; \draw [->] (0) to node (t)[auto,labelsize] {$\coprod_{j\in J}([q_{i,j}]_{i\in I})$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$[g_j]_{j\in J}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\coprod_{i\in I}([p_{i,j}]_{j\in J})$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$[f_i]_{i\in I}$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture}
Used by Proof, Proof, Proof
Proof of Corollary 6.13
  1. By the assumption, the slice category \mathcal{V}/X has finite products \times_X (given by pullbacks in \mathcal{V}), and is extensive (Proposition 6.12). Hence by Proposition 6.11, binary product by (g\colon B\longrightarrow X)\in \mathcal{V}/X preserves small coproducts, that is, (\coprod_{i\in I} f_i)\times_X g \cong \coprod_{i\in I}(f_i\times_X g).

  2. Using the first clause iteratively, we obtain (\coprod_{i\in I}f_i)\times_X(\coprod_{j\in J}g_j)\cong \coprod_{i\in I,j\in J} (f_i\times_X g_j).

Proposition

Proposition 7.1

UGF5

If \mathcal{V} has finite products and small coproducts, and if for any B\in\mathcal{V} the functor (-)\times B\colon \mathcal{V}\longrightarrow \mathcal{V} preserves small coproducts, then the forgetful functor U\colon{{\mathcal{V}}\mhyphen\mathbf{Cat}}\longrightarrow{{\mathcal{V}}\mhyphen\mathbf{Gph}} admits a left adjoint F.

Proof of Proposition 7.1

Given a \mathcal{V}-graph G=({\mathrm{ob}(G)},(G(x,y))_{x,y\in{\mathrm{ob}(G)}}), the free \mathcal{V}-category FG on G has the same objects as G and the hom-object given by

(FG)(x,y)=\coprod_{n\in\mathbb{N}}\coprod_{\substack{w_0,\dots,w_n\in {\mathrm{ob}(G)}\\w_0=x,w_n=y}}G(w_{n-1},w_{n})\times\cdots\times G(w_0,w_1)

for all x,y\in {\mathrm{ob}(FG)}={\mathrm{ob}(G)}. To spell out the identity elements and composition laws in FG, let us write

(FG)(x,y)_n=\coprod_{\substack{w_0,\dots,w_n\in {\mathrm{ob}(G)}\\w_0=x,w_n=y}}G(w_{n-1},w_{n})\times\cdots\times G(w_0,w_1)

for all x,y\in{\mathrm{ob}(FG)} and n\in\mathbb{N}.

Note that (FG)(x,y)_0 is the terminal object 1 of \mathcal{V} if x=y (otherwise, it is the initial object 0 of \mathcal{V}). Hence the identity element on x\in{\mathrm{ob}(FG)} can be given as

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node (0) {$1$}; \node[right=of 0](1) {$(FG)(x,x)_0$}; \node[right=of 1](d) {$\coprod_{n\in\mathbb{N}}(FG)(x,x)_n=(FG)(x,y)$,}; \draw [->] (0) to node [auto,labelsize] {$\cong$} (1); \draw [->] (1) to node [auto,labelsize] {$\sigma_0$} (d); \end{tikzpicture}

where \sigma_0 denotes the 0-th coprojection. Given any triple x,y,z\in{\mathrm{ob}(FG)} of objects, by the assumption we have

(FG)(y,z)\times (FG)(x,y)\cong \coprod_{k,l\in\mathbb{N}}(FG)(y,z)_l\times (FG)(x,y)_k.

Using the assumption once again, we see that (FG)(y,z)_l\times (FG)(x,y)_k is isomorphic to

\coprod_{\substack{u_0,\dots,u_k,v_0,\dots,v_l\in {\mathrm{ob}(G)}\\ u_0=x,u_k=v_0=y,v_l=z}}G(v_{l-1},v_l)\times\dots\times G(v_0,v_1)\times G(u_{k-1},u_k)\times\dots\times G(u_0,u_1),

and therefore naturally embeds into (FG)(x,z)_{k+l}. The universality of coproducts induce the composition laws for FG from these embeddings.

Proposition

Proposition 7.2

DD29

If \mathcal{V} is an extensive category with finite limits, then the functor F\colon{{\mathcal{V}}\mhyphen\mathbf{Gph}}\longrightarrow{{\mathcal{V}}\mhyphen\mathbf{Cat}} given in Proposition 7.1 preserves pullbacks.

Used by Proof, Proof, Proof
Proof of Proposition 7.2

Suppose we have a pullback

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$P$}; \node(1) at (2,1) {$B$}; \node(2) at (0,-1) {$A$}; \node(3) at (2,-1) {$X$}; \draw [->] (0) to node (t)[auto,labelsize] {$k$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$h$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$f$} (3); \draw (0.2,0.4) -- (0.6,0.4) -- (0.6,0.8); \end{tikzpicture}

in {{\mathcal{V}}\mhyphen\mathbf{Gph}}. Since F does nothing on the set of objects, by Proposition 6.7 it suffices to show that for any pair p=(a,b),p'=(a',b')\in{\mathrm{ob}(P)} with f(a)=g(b)=x and f(a')=g(b')=x', the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$(FP)(p,p')$}; \node(1) at (4,1) {$(FB)(b,b')$}; \node(2) at (0,-1) {$(FA)(a,a')$}; \node(3) at (4,-1) {$(FX)(x,x')$}; \draw [->] (0) to node (t)[auto,labelsize] {$(Fk)_{p,p'}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$(Fg)_{b,b'}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$(Fh)_{p,p'}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$(Ff)_{a,a'}$} (3); \end{tikzpicture}

is a pullback in \mathcal{V}. Recall that

(FP)(p,p')= \coprod_{n\in\mathbb{N}}(FP)(x,y)_n= \coprod_{n\in\mathbb{N}}\coprod_{\substack{p_0,\dots,p_n\in{\mathrm{ob}(P)}\\ p_0=p,p_n=p'}}P(p_{n-1},p_n)\times\dots\times P(p_0,p_1),

and similarly for other objects in the above diagram. Decomposing the morphisms by (?), we may apply Proposition 6.10 and now it suffices to show that for each n\in\mathbb{N}, the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$(FP)(p,p')_n$}; \node(1) at (4,1) {$(FB)(b,b')_n$}; \node(2) at (0,-1){$(FA)(a,a')_n$}; \node(3) at (4,-1){$(FX)(x,x')_n$}; \draw [->] (0) to node (t)[auto,labelsize] {$(Fk)_{p,p',n}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$(Fg)_{b,b',n}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$(Fh)_{p,p',n}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$(Ff)_{a,a',n}$} (3); \end{tikzpicture}

is a pullback. Decomposing the morphisms by (?) and applying Proposition 6.10 once again, we see that it suffices to show that for each n\in\mathbb{N} and x_0,\dots,x_n\in{\mathrm{ob}(X)} with x_0=x and x_n=x', the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,2.5) {$\displaystyle \coprod_{\substack{p_0,\dots,p_n\in{\mathrm{ob}(P)}\\ p_0=p,p_n=p'\\f\circ h(p_i)=x_i}}P(p_{n-1},p_n)\times\dots\times P(p_0,p_1)$}; \node(1) at (6,1) {$\displaystyle \coprod_{\substack{b_0,\dots,b_n\in{\mathrm{ob}(B)}\\ b_0=b,b_n=b'\\g(b_i)=x_i}}B(b_{n-1},b_n)\times\dots\times B(b_0,b_1)$}; \node(2) at (0,-1) {$\displaystyle \coprod_{\substack{a_0,\dots,a_n\in{\mathrm{ob}(A)}\\ a_0=a,a_n=a'\\f(a_i)=x_i}}A(a_{n-1},a_n)\times\dots\times A(a_0,a_1)$}; \node(3) at (6,-2.5) {$X(x_{n-1},x_n)\times\dots\times X(x_0,x_1)$}; \draw [->,rounded corners] (0)--(6,2.5)--(1); \node [labelsize] at (6,3.2) {$\displaystyle\coprod_{\substack{b_0,\dots,b_n\in{\mathrm{ob}(B)}\\ b_0=b,b_n=b'\\g(b_i)=x_i}} (Fk)_{p,p',n,b_0,\dots,b_n}$}; \draw [->] (1) to node (r)[auto,labelsize] {$(Fg)_{b,b',n,x_0,\dots,x_n}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$\displaystyle\coprod_{\substack{a_0,\dots,a_n\in{\mathrm{ob}(A)}\\ a_0=a,a_n=a'\\f(a_i)=x_i}} (Fh)_{p,p',n,a_0,\dots,a_n}$} (2); \draw [->,rounded corners] (2)--(0,-2.5)--(3); \node [labelsize] at (0,-2.7) {$(Ff)_{a,a',n,x_0,\dots,x_n}$}; \end{tikzpicture}

is a pullback. Writing the indexing sets of the coproducts appearing in the above diagram as

\begin{aligned} I&=\{\,(a_0,\dots,a_n)\mid a_i\in{\mathrm{ob}(A)}, a_0=a,a_n=a',f(a_i)=x_i\,\},\\ J&=\{\,(b_0,\dots,b_n)\mid b_i\in{\mathrm{ob}(B)}, b_0=b,b_n=b',g(b_i)=x_i\,\},\\ K&=\{\,(p_0,\dots,p_n)\mid p_i\in{\mathrm{ob}(P)}, p_0=p,p_n=p',f\circ h(p_i)=x_i\,\}, \end{aligned}

we have I\times J\cong K by the description of {\mathrm{ob}(P)} as a pullback. Using (?) and the second clause of Corollary 6.13, it suffices to show that for any n,x_i,a_i,b_i,p_i with p_i=(a_i,b_i), f(a_i)=g(b_i)=x_i, the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$P(p_{n-1},p_n)\times\dots\times P(p_0,p_1)$}; \node(1) at (8,1) {$B(b_{n-1},b_n)\times\dots\times B(b_0,b_1)$}; \node(2) at (0,-1) {$A(a_{n-1},a_n)\times\dots\times A(a_0,a_1)$}; \node(3) at (8,-1) {$ X(x_{n-1},x_n)\times\dots\times X(x_0,x_1)$}; \draw [->] (0) to node (t)[auto,labelsize] {$k_{p_{n-1},p_n}\times\dots\times k_{p_0,p_1}$} (1); \draw [->] (1) to node (r)[midway,fill=white,labelsize] {$g_{b_{n-1},b_n}\times\dots\times g_{b_0,b_1}$} (3); \draw [->] (0) to node (l)[midway,fill=white,labelsize] {$h_{p_{n-1},p_n}\times\dots\times h_{p_0,p_1}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$f_{a_{n-1},a_n}\times\dots\times f_{a_0,a_1}$} (3); \end{tikzpicture}

is a pullback. This follows from the fact that each P(p_i,p_{i+1}) is the pullback of A(a_i,a_{i+1}) and B(b_i,b_{i+1}) over X(x_i,x_{i+1}), as pullbacks commute with products.

Proposition

Proposition 7.3

OIQD

If \mathcal{V} has a strict initial object 0 and finite products,

then the categories {{\mathcal{V}}\mhyphen\mathbf{Gph}} and {{\mathcal{V}}\mhyphen\mathbf{Cat}} admit small coproducts and the forgetful functor U\colon {{\mathcal{V}}\mhyphen\mathbf{Cat}}\longrightarrow{{\mathcal{V}}\mhyphen\mathbf{Gph}} preserves small coproducts.

Used by Proof
Proof of Proposition 7.3

In both {{\mathcal{V}}\mhyphen\mathbf{Gph}} and {{\mathcal{V}}\mhyphen\mathbf{Cat}}, small coproducts are given by taking disjoint union of objects and setting the hom-objects between objects from different components to be 0 (see the proofs of Propositions 6.5 and 6.6).

Proposition

Proposition 7.4

HB9D

If \mathcal{V} is an extensive category with finite limits, then the unit \eta\colon {\mathrm{id}_{{{\mathcal{V}}\mhyphen\mathbf{Gph}}}}\Longrightarrow UF of the adjunction F\dashv U in Proposition 7.1 is cartesian.

Used by Proof, Proof
Proof of Proposition 7.4

By Proposition 6.7, it suffices to show that for any morphism f\colon G\longrightarrow H of \mathcal{V}-graphs, and x,y\in{\mathrm{ob}(G)}, the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$G(x,y)$}; \node(1) at (4,1) {$(FG)(x,y)$}; \node(2) at (0,-1) {$H(fx,fy)$}; \node(3) at (4,-1) {$(FH)(fx,fy)$}; \draw [->] (0) to node (t)[auto,labelsize] {$\sigma_{(1,x,y)}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$(Ff)_{x,y}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$f_{x,y}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$\sigma_{(1,fx,fy)}$} (3); \end{tikzpicture}

is a pullback in \mathcal{V}. This follows from Proposition 6.9 (note that if we rewrite (Ff)_{x,y} via (?) and (?), we have (Ff)_{x,y,1,fx,fy}=f_{x,y}).

Proposition

Proposition 7.5

P3FN

If \mathcal{V} is an extensive category with finite limits, then for each natural number m, the natural transformation

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,0) {$({{\mathcal{V}}\mhyphen\mathbf{Gph}})^m$}; \node(1) at (3,0) {$({{\mathcal{V}}\mhyphen\mathbf{Cat}})^m$}; \node(2) at (6,0) {${{\mathcal{V}}\mhyphen\mathbf{Cat}}$}; \node(3) at (8,1) {${{\mathcal{V}}\mhyphen\mathbf{Gph}}$}; \node(4) at (10,0) {${{\mathcal{V}}\mhyphen\mathbf{Cat}},$}; \draw [->] (0) to node (t)[auto,labelsize] {$F^m$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$\prod$} (2); \draw [->,bend left=20] (2) to node (l)[auto,labelsize] {$U$} (3); \draw [->,bend left=20] (3) to node (b)[auto,labelsize] {$F$} (4); \draw [->] (2) to node (b)[auto,swap,labelsize] {${\mathrm{id}_{{{\mathcal{V}}\mhyphen\mathbf{Cat}}}}$} (4); \draw [2cell] (8,0.9) to node[auto,labelsize] {$\varepsilon$} (8,0.1); \end{tikzpicture}

where \varepsilon is the counit of the adjunction F\dashv U in Proposition 7.1 and \prod is the m-ary product functor, is cartesian.

Used by Proof, Proof
Proof of Proposition 7.5

Let f=(f^{(1)},\dots, f^{(m)})\colon (G^{(1)},\dots,G^{(m)})\longrightarrow (H^{(1)},\dots,H^{(m)}) be a morphism in ({{\mathcal{V}}\mhyphen\mathbf{Gph}})^m. Our aim is to show that the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$FU(FG^{(1)}\times \dots \times FG^{(m)})$}; \node(1) at (7,1) {$FG^{(1)}\times \dots \times FG^{(m)}$}; \node(2) at (0,-1) {$FU(FH^{(1)}\times \dots \times FH^{(m)})$}; \node(3) at (7,-1) {$FH^{(1)}\times \dots \times FH^{(m)}$}; \draw [->] (0) to node (t)[auto,labelsize] {${\varepsilon_{FG^{(1)}\times \dots \times FG^{(m)}}}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {${Ff^{(1)}\times \dots \times Ff^{(m)}}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {${FU(Ff^{(1)}\times \dots \times Ff^{(m)})}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {${\varepsilon_{FH^{(1)}\times \dots \times FH^{(m)}}}$} (3); \end{tikzpicture}

in {{\mathcal{V}}\mhyphen\mathbf{Cat}} is a pullback. By Proposition 6.7 it suffices to show that for every pair of objects x=(x^{(1)},\dots,x^{(m)}),y=(y^{(1)},\dots,y^{(m)})\in{\mathrm{ob}(FU(FG^{(1)}\times \dots \times FG^{(m)}))}={\mathrm{ob}(G^{(1)})}\times \dots \times {\mathrm{ob}(G^{(m)})}, the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$\big(FU\prod_{i=1}^{m}(FG^{(i)})\big)(x,y)$}; \node(1) at (6.5,1) {$\prod_{i=1}^{m}(FG^{(i)})(x^{(i)},y^{(i)})$}; \node(2) at (0,-1) {$\big(FU\prod_{i=1}^{m}(FH^{(i)})\big)(fx,fy)$}; \node(3) at (6.5,-1) {$\prod_{i=1}^{m}(FH^{(i)})(f^{(i)}x^{(i)},f^{(i)}y^{(i)})$}; \draw [->] (0) to node (t)[auto,labelsize] {$$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$$} (3); \end{tikzpicture}

in \mathcal{V} is a pullback. Using Proposition 6.11, we may rewrite the bottom right object \prod_{i=1}^{m}(FH^{(i)})(f^{(i)}x^{(i)},f^{(i)}y^{(i)}) as a coproduct of products. Precisely, we define an (indexing) set I to be

\begin{gathered} I=\{\,(n_1,v^{(1)}_0,\dots, v^{(1)}_{n_1},\dots, n_m, v^{(m)}_0,\dots,v^{(m)}_{n_m})\\ \mid n_i\in \mathbb{N}, v^{(i)}_j\in{\mathrm{ob}(H^{(i)})}, v^{(i)}_0=f^{(i)}x^{(i)}, v^{(i)}_{n_i}=f^{(i)}y^{(i)} \,\}. \end{gathered}

Then \prod_{i=1}^{m}(FH^{(i)})(f^{(i)}x^{(i)},f^{(i)}y^{(i)}) is isomorphic to

\begin{gathered} \coprod_{I} H^{(1)}(v^{(1)}_{n_1-1},v^{(1)}_{n_1})\times\dots\times H^{(1)}(v^{(1)}_{0},v^{(1)}_{1})\\ \times\dots\times H^{(m)}(v^{(m)}_{n_m-1},v^{(m)}_{n_m})\times\dots\times H^{(m)}(v^{(m)}_{0},v^{(m)}_{1}). \end{gathered}

We may now decompose the diagram (?) into coproducts over I and apply Proposition 6.10. Fix an element (n_1,v^{(1)}_0,\dots, v^{(1)}_{n_1},\dots, n_m, v^{(m)}_0,\dots,v^{(m)}_{n_m})\in I, and introduce new indexing sets

\begin{aligned} J&=\{\,(k,j^{(1)}_1,\dots,j^{(1)}_{k-1},\dots, j^{(m)}_1,\dots,j^{(m)}_{k-1})\\ &\qquad\qquad\qquad\mid k, j^{(i)}_l\in \mathbb{N}, 0\leq j^{(i)}_1\leq\dots\leq j^{(i)}_{k-1}\leq n_i\,\},\\ K&=\{\, (w^{(1)}_0,\dots,w^{(1)}_{n_1},\dots,w^{(m)}_0,\dots,w^{(m)}_{n_m})\\ &\qquad\qquad\qquad\mid w^{(i)}_j\in{\mathrm{ob}(G^{(i)})},w^{(i)}_0=x^{(i)}, w^{(i)}_{n_i}=y^{(i)}, f^{(i)}w^{(i)}_j=v^{(i)}_j\,\}. \end{aligned}

It suffices to show that the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,2.5) {$\displaystyle \coprod_J \coprod_K G^{(1)}(w^{(1)}_{n_1-1},w^{(1)}_{n_1})\times\dots\times G^{(m)}(w^{(m)}_{0},w^{(m)}_{1})$}; \node(1) at (6,1) {$\displaystyle \coprod_K G^{(1)}(w^{(1)}_{n_1-1},w^{(1)}_{n_1})\times\dots\times G^{(m)}(w^{(m)}_{0},w^{(m)}_{1})$}; \node(2) at (0,-1) {$\displaystyle \coprod_J H^{(1)}(v^{(1)}_{n_1-1},v^{(1)}_{n_1})\times\dots\times H^{(m)}(v^{(m)}_{0},v^{(m)}_{1})$}; \node(3) at (6,-2.5) {$H^{(1)}(v^{(1)}_{n_1-1},v^{(1)}_{n_1})\times\dots\times H^{(m)}(v^{(m)}_{0},v^{(m)}_{1})$}; \draw [->,rounded corners] (0)--(6,2.5)--(1); \node [labelsize] at (6,2.7) {$\coprod_K [{\mathrm{id}_{}}]_J$}; \draw [->] (1) to node (r)[midway,fill=white,labelsize,xshift={30pt}] {$[f^{(1)}_{w^{(1)}_{n_1-1},w^{(1)}_{n_1}}\times \dots \times f^{(m)}_{w^{(m)}_{0},w^{(m)}_{1}}]_K$} (3); \draw [->] (0) to node (l)[midway,fill=white,labelsize,xshift={-30pt}] {$\coprod_J[f^{(1)}_{w^{(1)}_{n_1-1},w^{(1)}_{n_1}}\times \dots \times f^{(m)}_{w^{(m)}_{0},w^{(m)}_{1}}]_K$} (2); \draw [->,rounded corners] (2)--(0,-2.5)--(3); \node [labelsize] at (0,-2.7) {$[{\mathrm{id}_{}}]_{J}$}; \end{tikzpicture}

is a pullback, which follows from the second clause of Corollary 6.13.

Theorem

Theorem 7.6

K40Y

If \mathcal{V} is an extensive category with finite limits, then the free \mathcal{V}-category monad \mathsf{T}=(T,\eta,\mu) on {{\mathcal{V}}\mhyphen\mathbf{Gph}} is cartesian.

Proof of Theorem 7.6

The functor T=UF preserves pullbacks since both U (because it is a right adjoint) and F (by Proposition 7.2) do. The unit \eta is cartesian by Proposition 7.4. The multiplication \mu=U\varepsilon F is cartesian because \varepsilon F is so by Proposition 7.5 (take m=1), and U preserves pullbacks.

Definition

Definition 7.7

NVBR

For each natural number n, we define an adjunction F^{(n)}\dashv U^{(n)}\colon {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)}\longrightarrow{{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} recursively as follows:

  1. F^{(0)}=U^{(0)}={\mathrm{id}_{\mathcal{V}}};

  2. F^{(n+1)}\dashv U^{(n+1)} is the composite:

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(1) at (10,0) {${{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Cat}}.$}; \node(2) at (5,0) {${{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Gph}}$}; \node(3) at (0,0) {${{({{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)})}\mhyphen\mathbf{Gph}}$}; \draw [transform canvas={yshift=0.5em},<-] (1) to node [auto,swap,labelsize] {$F$} (2); \node [labelsize,rotate=-90]at (2.5,0) {$\dashv$}; \draw [transform canvas={yshift=-0.5em},->] (1) to node [auto,labelsize] {$U$} (2); \draw [transform canvas={yshift=0.5em},<-] (2) to node [auto,swap,labelsize] {${{F^{(n)}}\mhyphen\mathbf{Gph}}$} (3); \node[labelsize,rotate=-90] at (7.5,0) {$\dashv$}; \draw [transform canvas={yshift=-0.5em},->] (2) to node [auto,labelsize] {${{U^{(n)}}\mhyphen\mathbf{Gph}}$} (3); \end{tikzpicture}
Proposition

Proposition 7.8

D08W

For each natural number n, F^{(n)}\colon {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}\longrightarrow{{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)} preserves pullbacks.

Used by Proof
Proof of Proposition 7.8

For n=0, the assertion is trivial.

Proceeding inductively, if F^{(n)} preserves pullbacks, so does {{F^{(n)}}\mhyphen\mathbf{Gph}} by Proposition 6.7. The functor F\colon {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Gph}}\longrightarrow {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Cat}} preserves pullbacks by Proposition 7.2.

Proposition

Proposition 7.9

3FVX

For each natural number n, U^{(n)}\colon {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)}\longrightarrow{{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} preserves small coproducts.

Used by Proof, Proof
Proof of Proposition 7.9

For n=0, the assertion is trivial. Proceeding inductively, if U^{(n)} preserves small coproducts, it preserves initial objects, and so the functor {{U^{(n)}}\mhyphen\mathbf{Gph}} preserves small coproducts. The functor U\colon {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Cat}}\longrightarrow {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Gph}} also preserves small coproducts by Proposition 7.3.

Proposition

Proposition 7.10

GA63

For each natural number n, the unit \eta^{(n)}\colon {\mathrm{id}_{{{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}}} \Longrightarrow U^{(n)}F^{(n)} of the adjunction F^{(n)}\dashv U^{(n)} is cartesian.

Used by Proof
Proof of Proposition 7.10

Observe that adjunctions whose units are cartesian are closed under composition. Proceeding inductively, if \eta^{(n)} is cartesian, so is {{\eta^{(n)}}\mhyphen\mathbf{Gph}} by Proposition 6.7. The unit of the adjunction F\dashv U\colon {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Cat}}\longrightarrow {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})}\mhyphen\mathbf{Gph}} is cartesian by Proposition 7.4.

Proposition

Proposition 7.11

96BG

For each pair of natural numbers n and m, the natural transformation

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (-0.5,0) {$({{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)})^m$}; \node(1) at (3,0) {$({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)})^m$}; \node(2) at (6,0) {${{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)}$}; \node(3) at (8,1) {${{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}$}; \node(4) at (10,0) {${{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)},$}; \draw [->] (0) to node (t)[auto,labelsize] {$(F^{(n)})^m$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$\prod$} (2); \draw [->,bend left=20] (2) to node (l)[auto,labelsize] {$U^{(n)}$} (3); \draw [->,bend left=20] (3) to node (b)[auto,labelsize] {$F^{(n)}$} (4); \draw [->] (2) to node (b)[auto,swap,labelsize] {${\mathrm{id}_{{{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(n)}}}$} (4); \draw [2cell] (8,0.8) to node[auto,labelsize] {$\varepsilon^{(n)}$} (8,0.1); \end{tikzpicture}

where \varepsilon^{(n)} is the counit of the adjunction F^{(n)}\dashv U^{(n)} and \prod is the m-ary product functor, is cartesian.

Used by Proof
Proof of Proposition 7.11

By induction on n. Suppose the claim is true for n=k and for all m. For brevity, we will write the adjunction {{F^{(k)}}\mhyphen\mathbf{Gph}}\dashv{{U^{(k)}}\mhyphen\mathbf{Gph}} as F'\dashv U', and whose counit {{\varepsilon^{(k)}}\mhyphen\mathbf{Gph}} as \varepsilon'. We aim to show that for every morphism (f^{(1)},\dots, f^{(m)})\colon (G^{(1)},\dots,G^{(m)})\longrightarrow (H^{(1)},\dots,H^{(m)}) in ({{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(k+1)})^m, the outer rectangle in the diagram

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$FF'U'U(\prod_{i=1}^{m}FF'G^{(i)})$}; \node(1) at (5.8,1) {$FU(\prod_{i=1}^{m}FF'G^{(i)})$}; \node(2) at (0,-1) {$FF'U'U(\prod_{i=1}^{m}FF'H^{(i)})$}; \node(3) at (5.8,-1) {$FU(\prod_{i=1}^{m}FF'H^{(i)})$}; \node(4) at (10.5,1) {$\prod_{i=1}^{m}FF'G^{(i)}$}; \node(5) at (10.5,-1) {$\prod_{i=1}^{m}FF'H^{(i)}$}; \draw [->] (0) to node (t)[auto,labelsize] {${F\varepsilon'_{U(\prod_{i=1}^{m}FF'G^{(i)})}}$} (1); \draw [->] (1) to node (r)[midway,fill=white,labelsize] {${FU(\prod_{i=1}^{m}FF'f^{(i)})}$} (3); \draw [->] (0) to node (l)[midway,fill=white,labelsize] {${FF'U'U(\prod_{i=1}^{m}FF'f^{(i)})}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {${F\varepsilon'_{U(\prod_{i=1}^{m}FF'H^{(i)})}}$} (3); \draw [->] (1) to node [auto,labelsize] {${\varepsilon_{\prod_{i=1}^{m}FF'G^{(i)}}}$} (4); \draw [->] (4) to node [midway,fill=white,labelsize] {${\prod_{i=1}^{m}FF'f^{(i)}}$} (5); \draw [->] (3) to node [auto,swap,labelsize] {${\varepsilon_{\prod_{i=1}^{m}FF'H^{(i)}}}$} (5); \end{tikzpicture}

in {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(k+1)} is a pullback. The right square is a pullback by Proposition 7.5, so we shall show that the left square is also a pullback. Since F preserves pullbacks by Proposition 7.2, it suffices to show that the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$F'U'U(\prod_{i=1}^{m}FF'G^{(i)})$}; \node(1) at (6,1) {$U(\prod_{i=1}^{m}FF'G^{(i)})$}; \node(2) at (0,-1) {$F'U'U(\prod_{i=1}^{m}FF'H^{(i)})$}; \node(3) at (6,-1) {$U(\prod_{i=1}^{m}FF'H^{(i)})$}; \draw [->] (0) to node (t)[auto,labelsize] {${\varepsilon'_{U(\prod_{i=1}^{m}FF'G^{(i)})}}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {${U(\prod_{i=1}^{m}FF'f^{(i)})}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {${F'U'U(\prod_{i=1}^{m}FF'f^{(i)})}$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {${\varepsilon'_{U(\prod_{i=1}^{m}FF'H^{(i)})}}$} (3); \end{tikzpicture}

in {{({{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(k)})}\mhyphen\mathbf{Gph}} is a pullback. By Proposition 6.7, it suffices to show that for every pair of objects (x^{(1)},\dots,x^{(m)}),(y^{(1)},\dots,y^{(m)})\in {\mathrm{ob}(F'U'U(\prod_{i=1}^{m}FF'G^{(i)}))}={\mathrm{ob}(G^{(1)})}\times \dots \times {\mathrm{ob}(G^{(m)})}, the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$F^{(k)}U^{(k)}(\prod_{i=1}^{m}(FF'G^{(i)})(x^{(i)},y^{(i)}))$}; \node(1) at (7.5,1) {$\prod_{i=1}^{m}(FF'G^{(i)})(x^{(i)},y^{(i)})$}; \node(2) at (0,-1) {$F^{(k)}U^{(k)}(\prod_{i=1}^{m}(FF'H^{(i)})(f^{(i)}x^{(i)},f^{(i)}y^{(i)}))$}; \node(3) at (7.5,-1) {$\prod_{i=1}^{m}(FF'H^{(i)})(f^{(i)}x^{(i)},f^{(i)}y^{(i)})$}; \draw [->] (0) to node (t)[auto,labelsize] {${}$} (1); \draw [->] (1) to node (r)[auto,labelsize] {${}$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {${}$} (3); \end{tikzpicture}

in {{\mathcal{V}}\mhyphen\mathbf{Cat}}^{(k)} is a pullback. The bottom right object may be rewritten, using the set

\begin{gathered} I=\{\,(n_1,v^{(1)}_0,\dots, v^{(1)}_{n_1},\dots, n_m, v^{(m)}_0,\dots,v^{(m)}_{n_m})\\ \mid n_i\in \mathbb{N}, v^{(i)}_j\in{\mathrm{ob}(H^{(i)})}, v^{(i)}_0=f^{(i)}x^{(i)}, v^{(i)}_{n_i}=f^{(i)}y^{(i)} \,\}, \end{gathered}

as

\begin{gathered} \coprod_{I} F^{(k)}\big(H^{(1)}(v^{(1)}_{n_1-1},v^{(1)}_{n_1})\big) \times\dots\times F^{(k)}\big(H^{(1)}(v^{(1)}_{0},v^{(1)}_{1})\big)\\ \times\dots\times F^{(k)}\big(H^{(m)}(v^{(m)}_{n_m-1},v^{(m)}_{n_m})\big)\times\dots\times F^{(k)}\big(H^{(m)}(v^{(m)}_{0},v^{(m)}_{1})\big); \end{gathered}

cf. (?). Because both F^{(k)} and U^{(k)} (by Proposition 7.9) preserve small coproducts, we may decompose (?) as the coproduct over the set I and apply Proposition 6.10. Fix an element (n_1,v^{(1)}_0,\dots, v^{(1)}_{n_1},\dots, n_m, v^{(m)}_0,\dots,v^{(m)}_{n_m})\in I and introduce the set

\begin{gathered} K=\{\, (w^{(1)}_0,\dots,w^{(1)}_{n_1},\dots,w^{(m)}_0,\dots,w^{(m)}_{n_m})\\ \mid w^{(i)}_j\in{\mathrm{ob}(G^{(i)})},w^{(i)}_0=x^{(i)}, w^{(i)}_{n_i}=y^{(i)}, f^{(i)}w^{(i)}_j=v^{(i)}_j\,\}. \end{gathered}

It suffices to show that the square

\begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0)[align=left] at (0,3) {$\displaystyle \coprod_K F^{(k)}U^{(k)}F^{(k)}G^{(1)}(w^{(1)}_{n_1-1},w^{(1)}_{n_1})\times\cdots$\\ $\qquad \cdots\times F^{(k)}U^{(k)}F^{(k)}G^{(m)}(w^{(m)}_{0},w^{(m)}_{1})$}; \node(1)[align=left] at (7,1) {$\displaystyle \coprod_K F^{(k)}G^{(1)}(w^{(1)}_{n_1-1},w^{(1)}_{n_1})\times\cdots$\\ $\qquad\cdots\times F^{(k)}G^{(m)}(w^{(m)}_{0},w^{(m)}_{1})$}; \node(2)[align=left] at (0,-1) {$ F^{(k)}U^{(k)}F^{(k)}H^{(1)}(v^{(1)}_{n_1-1},v^{(1)}_{n_1})\times\cdots$\\ $\qquad \cdots\times F^{(k)}U^{(k)}F^{(k)}H^{(m)}(v^{(m)}_{0},v^{(m)}_{1})$}; \node(3)[align=left] at (7,-3) {$F^{(k)}H^{(1)}(v^{(1)}_{n_1-1},v^{(1)}_{n_1})\times\cdots$\\ $\qquad\cdots\times F^{(k)}H^{(m)}(v^{(m)}_{0},v^{(m)}_{1})$}; \draw [->,rounded corners] (0)--(7,3)--(1); \draw [->] (1) to (3); \draw [->] (0) to (2); \draw [->,rounded corners] (2)--(0,-3)--(3); \end{tikzpicture}

is a pullback. This follows from the first clause of Corollary 6.13, and the induction hypothesis.

Definition

Definition 8.1

3TPI

Let \mathcal{C} be a category, {J} a set, and \mathcal{F}=(f_j\colon A_j\longrightarrow B_j)_{j\in {J}} a {J}-indexed family of morphisms in \mathcal{C}.

  1. A contraction (with respect to \mathcal{F}) on a morphism g\colon C\longrightarrow D in \mathcal{C} is a J-indexed family of functions (\kappa_j)_{j\in J} such that for each j\in J, \kappa_j assigns to every pair of morphisms (h,k) in \mathcal{V} which makes the perimeter of (?) commute, a morphism \kappa_j(h,k) making the whole diagram (?) commute.

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,1) {$A_j$}; \node(1) at (2,1) {$C$}; \node(2) at (0,-1) {$B_j$}; \node(3) at (2,-1) {$D$}; \draw [->] (0) to node (t)[auto,labelsize] {$h$} (1); \draw [->] (1) to node (r)[auto,labelsize] {$g$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$f_j$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$k$} (3); \draw [->] (2) to node [midway,fill=white,labelsize] {$\kappa_j(h,k)$} (1); \end{tikzpicture}
  2. A map of morphisms with contractions from (g\colon C\longrightarrow D, (\kappa)_{j\in J}) to (g'\colon C'\longrightarrow D',(\kappa'_j)_{j\in J}) is a map of morphisms (u\colon C\longrightarrow C',v\colon D\longrightarrow D') from g to g' which commutes with contractions: for each j\in J and (h,k) in the domain of \kappa_j, u\circ \kappa_j(h,k)=\kappa'_j(u\circ h, v\circ k).

    \begin{tikzpicture}[baseline=-\the\dimexpr\fontdimen22\textfont2\relax ] \node(0) at (0,2) {$A_j$}; \node(1) at (2,2) {$C$}; \node(2) at (0,0) {$B_j$}; \node(3) at (2,0) {$D$}; \node(4) at (4,2) {$C'$}; \node(5) at (4,0) {$D'$}; \draw [->] (0) to node (t)[auto,labelsize] {$h$} (1); \draw [->] (1) to node (r)[auto,near end,labelsize] {$g$} (3); \draw [->] (0) to node (l)[auto,swap,labelsize] {$f_j$} (2); \draw [->] (2) to node (b)[auto,swap,labelsize] {$k$} (3); \draw [->] (1) to node (b)[auto,labelsize] {$u$} (4); \draw [->] (3) to node (b)[auto,swap,labelsize] {$v$} (5); \draw [->] (4) to node (b)[auto,labelsize] {$g'$} (5); \draw [->] (2) to node [midway,fill=white,labelsize] {$\kappa_j(h,k)$} (1); \draw [->] (2) to node [near end,fill=white,labelsize] {$\kappa'_j(u h,v k)$} (4); \end{tikzpicture}

We write the category of morphisms in \mathcal{C} with contractions (with respect to \mathcal{F}) as {\mathbf{Contr}(\mathcal{F})}. Note that we have the evident forgetful functor V\colon{\mathbf{Contr}(\mathcal{F})}\longrightarrow\mathcal{C}^{\mathbf{2}} where \mathbf{2} denotes the arrow category (i.e., the ordinal \mathbf{2} seen as a category) and \mathcal{C}^\mathbf{2}=[\mathbf{2},\mathcal{C}] is the functor category.

Definition

Definition 8.2

SN95

Let \mathcal{V} be a category with a terminal object and finite coproducts. For each natural number n, define a family \mathcal{F}^{(n)}=(f^{(n)}_0,\dots,f^{(n)}_{n+1}) of morphisms in {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} recursively as follows.

  1. f^{(0)}_0\colon 0\longrightarrow 1 and f^{(0)}_1\colon 1+1\longrightarrow 1 are the unique morphisms in \mathcal{V} into the terminal object 1.

  2. f^{(n)}_0\colon D\emptyset \longrightarrow D\{\ast\}, where \emptyset and \{\ast\} are the empty set and a singleton respectively, is the unique morphism in {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} out of the initial object D\emptyset, and for each i\in \{1,\dots, n+1\}, f^{(n)}_i=\Sigma f^{(n-1)}_{i-1}.

Proposition

Proposition 8.3

NVAD

Let \mathcal{V} be a locally presentable category. Then for each n\in\mathbb{N} and X\in {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}, the functor V_X\colon {\mathbf{Contr}(\mathcal{F}^{(n)})}_{X}\longrightarrow {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}/X is monadic and accessible.

Used by Proof
Theorem

Theorem 8.4

WPFG

If \mathcal{V} is a locally presentable and extensive category, then for any natural number n the category {T^{(n)}}\mhyphen{\mathbf{OC}} has an initial object.

Proof of Theorem 8.4

We shall follow the argument in [Leinster_book, Appendix G] (where \mathcal{V}=\mathbf{Set} and n=\omega) and

show that {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}/T^{(n)}1 is locally presentable (hence is both complete and cocomplete), and that W and V_{T^{(n)}1} are monadic and accessible. Then by [Kelly_unified, Theorem 27.1] it follows that the forgetful functor from {\mathsf{T}^{(n)}}\mhyphen{\mathbf{OC}} to {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}/T^{(n)}1 (the composite of functors in (?)) is also monadic, thus in particular {\mathsf{T}^{(n)}}\mhyphen{\mathbf{OC}} has an initial object, given by the free algebra over the initial object in {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}/T^{(n)}1.

Because {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)} is locally presentable, so is {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}/T^{(n)}1, being its slice. The functor W is monadic because it is the forgetful functor from a category of monoids and admits a left adjoint G (which, incidentally, is of a particularly simple form GP=\coprod_{n\in\mathbb{N}}P^{\otimes n} thanks to Proposition 7.9). It is routine to show that W is accessible. The functor V_{T^{(n)}1} is monadic and accessible by Proposition 8.3.

Definition

Definition 8.5

E97E

Let \mathcal{V} be a locally presentable extensive category and n be a natural number. A weak n-dimensional \mathcal{V}-category is a model of the initial \mathsf{T}^{(n)}-operad with contraction, where \mathsf{T}^{(n)} is the free strict n-dimensional \mathcal{V}-category monad on {{\mathcal{V}}\mhyphen\mathbf{Gph}}^{(n)}.

Example

Example 8.6

7VI1

If we let \mathcal{V}=\mathbf{Set} and n=2, then weak 2-categories (weak 2-dimensional \mathbf{Set}-categories) are equivalent to unbiased bicategories, which are a variant of bicategories equipped with for each natural number m, an m-ary horizontal composition operation. See [Leinster_book, Section 9.4] for details.

Example

Example 8.7

ZCB3

If we let \mathcal{V}=\omega\mhyphen\mathbf{Cpo} and n=2, then weak 2-dimensional \omega\mhyphen\mathbf{Cpo}-categories are the unbiased version of \omega\mhyphen\mathbf{Cpo}-enriched bicategories as in [Power_Tanaka].

Source and licence

The text on this page is from arXiv:1903.07030v1 by Soichiro Fujii, 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/1903/1903.07030.jsonl.