Measuring data types

The convolution algebra [-,-]\colon \mathrm{coAlg}_k^\mathrm{op}\times \mathrm{Alg}_k \rightarrow \mathrm{Alg}_k determines \mathrm{Alg}_k as a right module over \mathrm{coAlg}_k^\mathrm{op}, in the sense that we have the following natural isomorphisms in \mathrm{Alg}_k for all coalgebras C,D and algebra A

Thus \mathrm{Alg}_k^\mathrm{op} is a left module over \mathrm{coAlg}_k via [-,-]^\mathrm{op}\colon \mathrm{coAlg}_k\times \mathrm{Alg}_k^\mathrm{op}\rightarrow \mathrm{Alg}_k^\mathrm{op}. Moreover, for any algebra B, the induced functor [-,B]^\mathrm{op}\colon \mathrm{coAlg}_k\rightarrow \mathrm{Alg}_k^\mathrm{op} has a right adjoint \underline{\mathrm{Alg}}_k(-, B)\colon \mathrm{Alg}_k^\mathrm{op}\rightarrow \mathrm{coAlg}_k as we have the natural isomorphism

By [hylandetal, 3.1], we obtain that \mathrm{Alg}_k^\mathrm{op} is enriched, tensored and cotensored over \mathrm{coAlg}_k. Thus \mathrm{Alg}_k is enriched, tensored and cotensored over \mathrm{coAlg}_k.

Since every C-indexed partial homomorphism \widetilde{\varphi}\colon C\rightarrow [A, B] is equivalent to a coalgebra homomorphism C\rightarrow \mathrm{Cof}([A,B]) that coequalizes the parallel morphisms described above, we see that the category \mathscr{M}(A,B) of measurings from A to B is equivalent to the category of cones over the aforementioned parallel morphisms. Thus they have equivalent terminal objects {\underline{\mathrm{Alg}}}(A,B).

For (1), asking that \alpha restricts to a map \alpha_Q is exactly asking that (Q, \alpha_Q) is an algebra of F and that the quotient map constitutes a total algebra homomorphism q\colon (A, \alpha) \to (Q, \alpha_Q). Since the forgetful functor \mathrm{Alg} \to \mathscr{C} is faithful, it reflects epimorphisms. The second statement (2) is immediate.

For (1), consider \iota \colon S \rightarrowtail C. Asking that \chi restricts to a morphism \chi_S means exactly that \iota constitutes a total algebra homomorphism \iota \colon (S, \chi_C) \to (C, \chi). This is a monomorphism since the forgetful functor U\colon \mathrm{Alg} \to \mathscr{C} is faithful and thus reflects monomorphisms.

For (2), consider a monomorphism \iota\colon(S, \chi_S) \rightarrowtail (C, \chi). In order to show that \iota \colon S \to C is also a monomorphism, consider two points x, y\colon1 \to S in \mathscr{C} such that \iota x = \iota y. Since \mathscr{C} is assumed to be well-pointed, it suffices to show that x = y. Note that \llbracket{x}\rrbracket = \llbracket{\iota x}\rrbracket = \llbracket{\iota y}\rrbracket = \llbracket{y}\rrbracket, and let ((I, \chi_I), \top_n) denote a coalgebra generated by a point of this index. Then we get two maps \overline x, \overline y\colon(I, \chi_I) \to (S, \chi_S) and a map \overline{\iota x} = \overline{\iota y} \colon (I, \chi_I) \to (C, \chi) such that \iota \overline x = \overline{\iota x} = \overline{\iota y} = \iota \overline y. Since \iota is a monomorphism, \overline x = \overline y, but then x = \overline x \top_n = \overline y \top_n = y\colon * \to \mathscr{C}.

We first claim that {\mathrm{Alg}}(A, [C,B]) is empty or a singleton for any coalgebra C. Since !_A\colon \mathbb N \to A is an epimorphism, the function

is an injection, and since \mathbb N is initial, {\mathrm{Alg}}(\mathbb N, [C,B]) \cong *. Thus, {\mathrm{Alg}}(A, [C,B]) is a singleton, in the case where the only map \mathbb N \to [C,B] factors through A, and otherwise is empty.

We now claim that the canonical map \llbracket{-}\rrbracket\colon{\underline{\mathrm{Alg}}}(A,B) \to {\mathbb N_\infty} is a monomorphism. Suppose there are maps a,b\colon C \to {\underline{\mathrm{Alg}}}(A,B) from a coalgebra C such that \llbracket{a}\rrbracket = \llbracket{b}\rrbracket. Recall that the coalgebra {\underline{\mathrm{Alg}}}(A,B) is defined by the following universal property for any coalgebra C

Thus, {\mathrm{coAlg}}(C,{\underline{\mathrm{Alg}}}(A,B)) is a singleton, so a = b, and \llbracket{-}\rrbracket is monic.

Suppose (C, \chi_C) and (D, \chi_D) are coalgebras. Then C\otimes D has the following coalgebra structure:

The morphism \eta\colon \mathbb I\rightarrow F(\mathbb I) provides the coalgebraic structure on \mathbb I.

To see that ({\mathrm{coAlg}}, \otimes, (\mathbb I, \eta)) is a symmetric monoidal category, we first need to check that (C, \chi_C)\otimes (\mathbb I, \eta)\cong (C, \chi_C). On objects, we have C\otimes \mathbb I\cong C as \mathbb I is a monoidal unit. The coalgebraic structures correspond as we have the following commutative diagram by unitality of (F, \nabla, \eta):

Similarly, we have a natural isomorphism (\mathbb I, \eta)\otimes (C, \chi_C)\cong (C, \chi_C) from the identification \mathbb I\otimes C\cong C. Moreover, we also have the following natural isomorphism

lifted from (C\otimes C')\otimes C''\cong C\otimes (C'\otimes C''). Lastly, the symmetry C\otimes C'\cong C'\otimes C lifts to {\mathrm{coAlg}}. Therefore as \mathscr{C} is symmetric monoidal, the above natural identifications assemble to a symmetric monoidal structure on {\mathrm{coAlg}} as the pentagon, triangle, hexagon and symmetric identities remain valid in {\mathrm{coAlg}}.

Suppose now that \mathscr{C} is locally presentable and closed, and F is accessible. Then for all objects X\in \mathscr{C}, we have that X\otimes -\colon \mathscr{C}\rightarrow \mathscr{C} is a left adjoint functor, with right adjoint given by its the internal hom [X, -]\colon \mathscr{C}\rightarrow \mathscr{C}. Since \mathrm{coAlg} is also locally presentable and colimits are computed in \mathscr{C}, we get that for all C\in \mathrm{coAlg}, the induced functor C\otimes -\colon \mathrm{coAlg}\rightarrow \mathrm{coAlg} also preserves all colimits and thus must be a left adjoint as \mathrm{coAlg} is locally presentable. We denote by \underline{\mathrm{coAlg}}(C,-)\colon \mathrm{coAlg}\rightarrow \mathrm{coAlg} its right adjoint. The construction is natural in C and thus defines the desired closed structure on \mathrm{coAlg}.

The convolution algebra functor [-,-]\colon{\mathrm{coAlg}}^\mathrm{op}\times {\mathrm{Alg}}\rightarrow {\mathrm{Alg}} presents {\mathrm{Alg}} as a right module over {\mathrm{coAlg}}^\mathrm{op}. Thus {\mathrm{Alg}}^\mathrm{op} is a left module over {\mathrm{coAlg}} via

Moreover, for any A\in {\mathrm{Alg}}, the functor [-,B]^\mathrm{op}\colon{\mathrm{coAlg}}\rightarrow {\mathrm{Alg}}^\mathrm{op} has a right adjoint {\underline{\mathrm{Alg}}}(-, B)\colon{\mathrm{Alg}}^\mathrm{op}\rightarrow {\mathrm{coAlg}} as shown in ?. Thus, by [hylandetal, 3.1], the category {\mathrm{Alg}}^\mathrm{op} is enriched over {\mathrm{coAlg}} with tensor [-,-]^\mathrm{op}. Therefore {\mathrm{Alg}} is enriched over {\mathrm{coAlg}} with power [-,-].

We obtain a convolution algebra {\mathrm{coAlg}}_F^\mathrm{op} \times {\mathrm{Alg}}_{G} \to {\mathrm{Alg}}_{G} by taking a coalgebra (C,\chi) and an algebra (A, \alpha) to the following composite

where the unmarked arrow is the adjunct of the following composite

where \mathrm{ev} denotes evaluation. The action on morphisms is given by the naturality of constituent arrows of this constructed algebra structure. The functoriality is inherited from the functoriality of [-, -].

The diagrams of [yetter, Def. 39] exactly correspond to the opposite

this functor being a left action in the sense of [hylandetal]. Since [-,A]^\mathrm{op} preserves colimits, so does [-,A]^\mathrm{op} \colon {\mathrm{coAlg}}_F \to {\mathrm{Alg}}_{G}^\mathrm{op}. Since {\mathrm{coAlg}}_F is locally presentable, and \mathrm{Alg}_G^\mathrm{op} is essentially small, the functor has a right adjoint. Thus, by [hylandetal, Prop. 3.1], we see that {\mathrm{Alg}}_{G}^\mathrm{op} is enriched, tensored and cotensored in {\mathrm{coAlg}}_F. Thus, {\mathrm{Alg}}_{G} is enriched, tensored and cotensored in {\mathrm{coAlg}}_F.

To apply previous result, we only need to show there exists an F-module structure on GF, that is, we need a certain natural map

The \mathscr{C}-enrichment of G produces a map X \otimes GY \rightarrow G(X\otimes Y) for any objects X and Y in \mathscr{C}. Indeed, this is the adjunct of

where the first map is the coevaluation of the internal hom, and the second map is induced by the \mathscr{C}-enrichment. We apply this map to FX and FY to get the following composition

One can check that this makes the diagrams of [yetter, Def. 39] commute.

We consider an object \lim^C\mathrm{id}_{\underline{\mathrm{Alg}}} with the following universal property:

(This is the limit of \mathrm{id}_{\underline{\mathrm{Alg}}} weighted by the constant functor at C.) Since the hom {\mathrm{coAlg}} (C, {\underline{\mathrm{Alg}}}(A,-)) preserves limits and \lim_{X \in {\mathrm{Alg}}} X \cong \mathbb N, we have

Thus, C^* has the universal property of \lim^C\mathrm{id}_{\underline{\mathrm{Alg}}}.

Note that for any C-initial algebra A, we have \lim_{X \in {\mathrm{Alg}}} \ {\mathrm{coAlg}} (C, {\underline{\mathrm{Alg}}}(A,X)) is the terminal object. Thus, by this universal property of C^*, there is a unique map A \to C^*.

Consider the coalgebra morphism m \colon (\mathbb{n}-1)^\circ \to \mathbb{n}^\circ, i \mapsto i. This induces a morphism

This morphism is monomorphic by definition. Since A is \mathbb{n}^\circ-initial, we know \mathbb{n} \triangleright A is an initial object. This means m\triangleright A is a monomorphism into the initial object, hence an isomorphism.

Let k\leq n. Define the coalgebra morphism

for all 0 \leq j \leq n-k. Consider the composition of measurings \varphi \circ (\mathrm{id} \times -_{A} \circ \varphi) \in \mu_{\mathbb{n}^\circ \times \mathbb{n}^\circ}(A,\mathbb N). We can precompose this measuring with the coalgebra morphism p_j to obtain a measuring

We also have the coalgebra morphism f\colon \mathbb{k}^\circ \to \mathbb{n}^\circ, i \mapsto i which we can precompose with \varphi. This gives us a measuring

Since A is also \mathbb{k}^\circ-initial, we know these measurings must coincide. Hence we can state \varphi(i,a) = \varphi(i,-_{A} \circ \varphi(i+j,a)) for all i \in \mathbb{k}^\circ and 0 \leq j \leq n-k. The only restriction placed on k was that k \leq n. Iterating over all 0 \leq k \leq n, we arrive at the desired result

for all 0 \leq i \leq n and 0 \leq j \leq n-i.

Since \varphi(i,a) = \varphi(i, (\varphi(i, a))_A) by the previous lemma, we know [0,i,a] = [0, i, (\varphi(i, a))_A] in \mathbb{n}^\circ \triangleright A. We also have [\varphi(i,a),z] = [0,i,a], and by definition of the equivalence relation \sim, we have [0, i, (\varphi(i, a))_A] = [\min(i, \varphi(i, a)), z]. From this we conclude

hence \varphi(i,a) \leq i for all i \in \mathbb{n}^\circ.

We proceed by induction over k. For k = 0, we have that \mathbb{k} \cong 1, the terminal object in the category of algebras. Hence \varphi_0 : A \to 1 is an algebra morphism. For the inductive step, assume \varphi_{k-1} : A \to \mathbb{k}-1 is an algebra morphism. We wish to show \alpha_k(\varphi_k(a)) = \varphi_k(\alpha(a)) for all a \in A. If \varphi_k(a) = 0, we know

If \varphi_k(a) \geq 0 we can make the following deduction

By ?, there exists a unique morphism A \to [\mathbb{n}^\circ, \mathbb N] for any \mathbb{n}^\circ-initial algebra A. Since \mathbb{n} is \mathbb{n}^\circ-initial we know there exists a unique morphism m \colon \mathbb{n} \rightarrowtail [\mathbb{n}^\circ, \mathbb N]. Upon closer inspection m turns out to be a monomorphism. Given any two morphisms f,g \colon A \to \mathbb{n}, we can draw the following diagram

Since the morphism A \to [\mathbb{n}^\circ, \mathbb N] is unique, we know the composites m \circ f = m \circ g, and by m being mono we conclude f = g. Hence, there can be at most one algebra morphism from a \mathbb{n}^\circ-initial algebra A to \mathbb{n}.

Given an \mathbb{n}^\circ initial algebra A, by Proposition ? we obtain an algebra morphism \varphi_n \colon A \to \mathbb{n}. By Lemma ? it is unique. We conclude \mathbb{n} is the terminal \mathbb{n}^\circ-initial algebra.

Consider the coalgebra morphism \iota\colon S_{M,n-1}^\circ \to S_{M,n}^\circ, s \mapsto s. This induces a morphism

This morphism is monomorphic by definition. Since A is S_{M,n}^\circ-initial, we know S_{M,n} \triangleright A is an initial object. This means \iota\triangleright A is a monomorphism into the initial object, hence an isomorphism.

Let k\leq n. First, we define a function which takes two trees and appends the second tree to all the roots of the first tree. We define it as

For all 0 \leq j \leq n-k, define the coalgebra morphism

where \widetilde{s} is the unique tree \widetilde{s} \in S_{\{e\}, k} such that \mathtt{shape}(\widetilde{s}) = \mathtt{shape}(s).

Consider the composition of measurings \varphi \circ (\mathrm{id} \times \mathord{\mathpalette\raised@mathinvertedexclamationmark\relax} _{A} \circ \varphi) \in \mu_{S_{M,n}^\circ \times S_{M,n}^\circ}(A,S_{M}). We can precompose this measuring with the coalgebra morphism p_j to obtain a measuring

We also have the coalgebra morphism \iota\colon S_{M,k}^\circ \to S_{M,n}^\circ, s \mapsto s which we can precompose with \varphi. This gives us a measuring

Since A is also S_{M,k}^\circ-initial, we know these measurings must coincide. Hence we can state \varphi(s,a) = \varphi(s, \mathord{\mathpalette\raised@mathinvertedexclamationmark\relax} _{A} \circ \varphi(\widetilde{s} ++ s_j,a)) for all s \in S_{M,k}^\circ and 0 \leq j \leq n-k. The only restriction placed on k was that k \leq n. Iterating over all 0 \leq k \leq n, we arrive at the desired result

for all 0 \leq i \leq n and 0 \leq j \leq n-i. In particular this holds for s = s_i, and noting s_i ++ s_j = s_{i + j} we obtain the desired result.

We will proceed by induction over i. For the base case i = 0, we have s_0 = e_S, so \varphi(s_0, a) = e_S \in S_{M,0}. For the induction step, assume \varphi(s_i, a) \in S_{M,i}. Using s_{i+1} = (e,(s_i)^{(\infty)}) and the previous lemma we can write \varphi(s_{i+1}, a) = \varphi( (e,(s_i)^{(\infty)}), \mathord{\mathpalette\raised@mathinvertedexclamationmark\relax} _{A}(\varphi(s_{i+1}, a))). Let \alpha\colon 1 + M \times (S_M)^{\leq \infty} \to S_M, then we can write (m,s) = \alpha^{-1}(\varphi(s_{i+1}, a)) where s is the list with components s_i. We then know by definition of a measuring that

where k = \mathtt{map}( \mathord{\mathpalette\raised@mathinvertedexclamationmark\relax} _{A})(s). By the induction hypothesis, we know

hence \varphi(s_{i+1}, a) \in S_{M,i + 1} by definition. This concludes the induction step and the proof.

We proceed by induction over k. For k = 0, we have that S_{M,k} \cong 1, the terminal object in \mathrm{Set}. Hence \varphi_0\colon A \to S_{M,0} is an algebra morphism. For the inductive step, assume \varphi_{k-1}\colon A \to S_{M,k-1} is an algebra morphism. We wish to show \varphi_k is an algebra morphism. In more detail, we aim to show

for all (m,\ell) \in M \times A^{\leq \infty}. First, we will write \ell = (a_i)_{i = 0}^j, where j \in {\mathbb N_\infty}. We can now write

Writing \varphi_k \circ \mathord{\mathpalette\raised@mathinvertedexclamationmark\relax} _{A} \circ \varphi_k(a_i) = t_i, we can make the case distinction

by \varphi \colon S_{M,n}^\circ \times A \to S_M being a measuring. This means

By the algebra structure of S_{M,k}, we can write this as \alpha_k(m, (t_i)_i) = (m,(r_i)_i), where

By the induction hypothesis \alpha_{k-1}(m_i, \mathtt{map}(\varphi_{k-1} \circ \mathord{\mathpalette\raised@mathinvertedexclamationmark\relax} _{A})(a_i)) = (\varphi_{k-1} \circ \mathord{\mathpalette\raised@mathinvertedexclamationmark\relax} _{A})(m_i, a_i) and we can write

using ?. Retracing our steps, we now compute

using that \varphi is a measuring twice. We conclude \varphi_k \colon A \to S_{M,k} is an algebra morphism for all 0 \leq k \leq n.

By ?, there exists a unique morphism A \to [S_{M,n}^\circ, S_{M}] for any S_{M,n}^\circ-initial algebra A. Since S_{M,n} is S_{M,n}^\circ-initial we know there exists a unique morphism \iota \colon S_{M,n} \rightarrowtail [S_{M,n}^\circ, S_{M}].

This map is given by

We can easily conclude \iota is a monomorphism by observing that \iota(s)(s_n) = s for all s \in S_{M,n}. Given any two morphisms f,g\colon A \to S_{M,n}, we can draw the following diagram

Since the morphism A \to [S_{M,n}^\circ, S_{M}] is unique, we know the composites \iota \circ f = \iota \circ g, and by \iota being mono we conclude f = g. Hence, there can be at most one algebra morphism from a S_{M,n}^\circ-initial algebra A to S_{M,n}.

Given an S_{M,n}^\circ-initial algebra A, by ?, we obtain an algebra morphism \varphi_n \colon A \to S_{M,n}. By ?, it is unique. We conclude \mathbb{n} is the terminal S_{M,n}^\circ-initial algebra.