---
abstract: |
    Esik and Maletti introduced the notion of a proper semiring and proved that some important (classes of) semirings – Noetherian semirings, natural numbers – are proper. Properness matters as the equivalence problem for weighted automata over a semiring which is proper and finitely and effectively presented is decidable. Milius generalised the notion of properness from a semiring to a functor. As a consequence, a semiring is proper if and only if its associated “cubic functor” is proper. Moreover, properness of a functor renders soundness and completeness proofs for axiomatizations of equivalent behaviour.

    In this paper we provide a method for proving properness of functors, and instantiate it to cover both the known cases and several novel ones: (1) properness of the semirings of positive rationals and positive reals, via properness of the corresponding cubic functors; and (2) properness of two functors on (positive) convex algebras. The latter functors are important for axiomatizing trace equivalence of probabilistic transition systems. Our proofs rely on results that stretch all the way back to Hilbert and Minkowski.
author:
- Ana Sokolova
- Harald Woracek
title: Proper Semirings and Proper Convex Functors
---

Introduction {#sec-Intro}
============

In this paper we deal with algebraic categories and deterministic weighted automata functors on them. Such categories are the target of generalized determinization [@silva.bonchi.bonsangue.rutten:2010; @silva.sokolova:2011; @jacobs.silva.sokolova:2015] and enable coalgebraic modelling beyond sets. For example, non-deterministic automata, weighted, or probabilistic ones are coalgebraically modelled over the categories of join-semilattices, semimodules for a semiring, and convex sets, respectively. Moreover, expressions for axiomatizing behavior semantics often live in algebraic categories.

In order to prove completeness of such axiomatizations, the common approach [@silva:2010; @bonsangue.milius.silva:2011; @silva.sokolova:2011] is to prove finality of a certain object in a category of coalgebras over an algebraic category. Proofs are significantly simplified if it suffices to verify finality only w.r.t. coalgebras carried by free finitely generated algebras, as those are the coalgebras that result from generalized determinization.

In recent work, Milius [@milius:2017] proposed the notion of a proper functor on an algebraic category that provides a sufficient condition for this purpose. This notion is an extension of the notion of a proper semiring introduced by Esik and Maletti [@esik.maletti:2010]: A semiring is proper if and only if its “cubic" functor is proper. A cubic functor is a functor $\mathbb S \times (-)^A$ where $A$ is a finite alphabet and $\mathbb S$ is a free algebra with a single generator in the algebraic category. Cubic functors model deterministic weighted automata which are models of determinizations of non-deterministic and probabilistic transition systems.

Properness is the property that for any two states that are behaviourally equivalent in coalgebras with free finitely generated carriers, there is a zig-zag of homomorphisms (called a chain of simulations in the original works on weighted automata and proper semirings) that identifies the two states and whose nodes are all carried by free finitely generated algebras.

Even though the notion of properness is relatively new for a semiring and very new for a functor, results on properness of semirings can be found in more distant literature as well. Here is a brief history, to the best of our knowledge:

-   The Boolean semiring was proven to be proper in [@bloom.esik:1993].

-   Finite commutative ordered semirings were proven to be proper in  [@esik.kuich:2001 Theorem 5.1]. Interestingly, the proof provides a zig-zag with at most seven intermediate nodes.

-   Any euclidean domain and any skew field were proven proper in [@beal.lombardy.sakarovitch:2005 Theorem 3]. In each case the zig-zag has two intermediate nodes.

-   The semiring of natural numbers $\mathbb N$, the Boolean semiring $\mathbb B$, the ring of integers $\mathbb Z$ and any skew field were proven proper in [@beal.lombardy.sakarovitch:2006 Theorem 1]. Here, all zig-zag were spans, i.e., had a single intermediate node with outgoing arrows.

-   Noetherian semirings were proven proper in [@esik.maletti:2010 Theorem 4.2], commutative rings also in [@esik.maletti:2010 Corollary 4.4], and finite semirings as well in [@esik.maletti:2010 Corollary 4.5], all with a zig-zag being a span. Moreover, the tropical semiring is not proper, as proven in [@esik.maletti:2010 Theorem 5.4].

Having properness of a semiring, together with the property of the semiring being finitely and effectively presentable, yields decidability of the equivalence problem (decidability of trace equivalence) for weighted automata.

In this paper, motivated by the wish to prove properness of a certain functor ${{\ensuremath{\widehat F}}}$ on convex algebras used for axiomatizing trace semantics of probabilistic systems in [@silva.sokolova:2011], as well as by the open questions stated in [@milius:2017 Example 3.19], we provide a framework for proving properness. We instantiate this framework on known cases like Noetherian semirings and $\mathbb N$ (with a zig-zag that is a span), and further prove new results of properness:

-   The semirings $\mathbb Q_+$ and $\mathbb R_+$ of non-negative rationals and reals, respectively, are proper. The shape of the zig-zag is a span as well.

-   The functor $[0,1] \times (-)^A$ on  is proper, again the zig-zag being a span.

-   The functor ${{\ensuremath{\widehat F}}}$ on ${{\text{\tt{PCA}}}}$ is proper. This proof is the most involved, and interestingly, provides the only case where the zig-zag is not a span: it contains three intermediate nodes of which the middle one forms a span.

Our framework requires a proof of so-called *extension* and *reduction lemmas* in each case. While the extension lemma is a generic result that covers all cubic functors of interest, the reduction lemma is in all cases a nontrivial property intrinsic to the algebras under consideration. For the semiring of natural numbers it is a consequence of a result that we trace back to Hilbert; for the case of convex algebra $[0,1]$ the result is due to Minkowski. In the case of ${{\ensuremath{\widehat F}}}$, we use Kakutani’s set-valued fixpoint theorem.

It is an interesting question for future work whether these new properness results may lead to new complete axiomatizations of expressions for certain weighted automata.

The organization of the rest of the paper is as follows. In Section \[sec-ProperFunctors\] we give some basic definitions and introduce the semirings, the categories, and the functors of interest. Section \[sec-PropernessCubic\] provides the general framework as well as proofs of properness of the cubic functors. Section \[sec-SubcubicFunctor\]–Section \[sec-PropernessSubcubic\] lead us to properness of ${{\ensuremath{\widehat F}}}$ on . For space reasons, we present the ideas of proofs and constructions in the main paper and defer all detailed proofs to the appendix.

#### Acknowledgements.

We thank the anonymous reviewers for many valuable comments, in particular for reminding us of a categorical property that shortened the proof of the extension lemma (the proofs of Lemma \[lem:ext-lem-1\] and Lemma \[lem:ext-lem-2\] in Appendix \[app:B\]).

Proper functors {#sec-ProperFunctors}
===============

We start with a brief introduction of the basic notions from algebra and coalgebra needed in the rest of the paper, as well as the important definition of proper functors [@milius:2017]. We refer the interested reader to [@Rut00:tcs; @JR96:eatcs; @jacobs:2017] for more details. We assume basic knowledge of category theory, see e.g. [@maclane:1998] or Appendix \[sec:app-basics\].

Let ${\text{\tt{C}}}$ be a category and $F$ a ${\text{\tt{C}}}$-endofunctor. The category ${{\sf Coalg}({F})}$ of *$F$-coalgebras* is the category having as objects pairs $(X,c)$ where $X$ is an object of ${\text{\tt{C}}}$ and $c$ is a ${\text{\tt{C}}}$-morphism from $X$ to $FX$, and as morphisms $f\colon(X,c)\to(Y,d)$ those ${\text{\tt{C}}}$-morphisms from $X$ to $Y$ that make the diagram on the right commute.

[r]{}[.1]{}

All base categories ${\text{\tt{C}}}$ in this paper will be *algebraic categories*, i.e., categories ${{\text{\tt{Set}}}^{T}}$ of Eilenberg-Moore algebras of a finitary monad [^1] in ${{\text{\tt{Set}}}}$. Hence, all base categories are concrete with forgetful functor that is identity on morphisms.

In such categories behavioural equivalence [@Kurz00:thesis; @Wol00:cmcs; @Staton11] can be defined as follows. Let $(X,c)$ and $(Y,d)$ be $F$-coalgebras and let $x\in X$ and $y\in Y$. Then $x$ and $y$ are *behaviourally equivalent*, and we write $x\sim y$, if there exists an $F$-coalgebra $(Z,e)$ and ${{\sf Coalg}({F})}$-morphisms $f\colon (X,c)\to(Z,e)$, $g\colon(Y,d)\to(Z,e)$, with $f(x)=g(y)$. $$\xymatrix@C=40pt{
        (X,c) \ar[r]^f
        & (Z,e) 
        \save[]+<0pt,-13pt>*\txt{$\scriptstyle f(x)=g(y)$}\restore
        & (Y,d) \ar[l]_g 
    }$$ If there exists a final coalgebra in ${{\sf Coalg}({F})}$, and all functors considered in this paper will have this property, then two elements are behaviourally equivalent if and only if they have the same image in the final coalgebra. If we have a *zig-zag diagram* in ${{\sf Coalg}({F})}$ $$\label{zig-zag}
    \xymatrix@R=0.7em@C=9pt{
        (X,c) \ar[rd]^{f_1} && (Z_2,e_2) \ar[ld]_{f_2} \ar[rd]^{f_3} && 
        \cdots \ar[ld]_{f_4} \ar[rd]^{f_{2n-1}} && (Y,d) \ar[ld]_{f_{2n}} &
        \\
        & (Z_1,e_1) 
        && (Z_3,e_1) 
        && (Z_{2n-1},e_1) 
        &
    }$$ which relates $x$ with $y$ in the sense that there exist elements $z_{2k}\in Z_{2k}$, $k=1,\ldots,n-1$, with (setting $z_0=x$ and $z_{2n}=y$) $$f_{2k}(z_{2k})=f_{2k-1}(z_{2k-2}),\quad k=1,\ldots, n
    ,$$ then $x\sim y$.

We now recall the notion of a proper functor, introduced by Milius [@milius:2017] which is central to this paper. It is very helpful for establishing completeness of regular expressions calculi, cf. [@milius:2017 Corollary 3.17].

\[Proper\] Let $T\colon{{\text{\tt{Set}}}}\to{{\text{\tt{Set}}}}$ be a finitary monad with unit $\eta$ and multiplication $\mu$. A ${{\text{\tt{Set}}}^{T}}$-endofunctor $F$ is *proper*, if the following statement holds.

For each pair $(TB_1,c_1)$ and $(TB_2,c_2)$ of $F$-coalgebras with $B_1$ and $B_2$ finite sets, and each two elements $b_1\in B_1$ and $b_2\in B_2$ with $\eta_{B_1}(b_1)\sim\eta_{B_2}(b_2)$, there exists a zig-zag in ${{\sf Coalg}({F})}$ which relates $\eta_{B_1}(b_1)$ with $\eta_{B_2}(b_2)$, and whose nodes $(Z_j,e_j)$ all have free and finitely generated carrier.

This notion generalizes the notion of a proper semiring introduced by Esik and Maletti in [@esik.maletti:2010 Definition 3.2], cf. [@milius:2017 Remark 3.10].

\[fg\] In the definition of properness the condition that intermediate nodes have free *and* finitely generated carrier is necessary for nodes with incoming arrows (the nodes $Z_{2k-1}$ in ). For the intermediate nodes with outgoing arrows ($Z_{2k}$ in ), it is enough to require that their carrier is finitely generated. This follows since every $F$-coalgebra with finitely generated carrier is the image under an $F$-coalgebra morphism of an $F$-coalgebra with free and finitely generated carrier.

Moreover, note that zig-zags which start (or end) with incoming arrows instead of outgoing ones, can also be allowed since a zig-zag of this form can be turned into one of the form by appending identity maps.

Some concrete monads and functors {#some-concrete-monads-and-functors .unnumbered}
---------------------------------

We deal with the following base categories.

-   The category ${\text{$\mathbb S$-{\text{\tt{SMOD}}}}}$ of semimodules over a semiring $\mathbb S$ induced by the monad $T_{\mathbb S}$ of finitely supported maps into $\mathbb S$, see, e.g., [@manes.mulry:2007 Example 4.2.5].

-   The category  of positively convex algebras induced by the monad of finitely supported subprobability distributions, see, e.g., [@doberkat:2006; @doberkat:2008] and [@pumpluen:1984].

For $n\in\mathbb N$, the free algebra with $n$ generators in ${\text{$\mathbb S$-{\text{\tt{SMOD}}}}}$ is the direct product $\mathbb S^n$, and in  it is the $n$-simplex $\Delta^n=\{(\xi_1,\ldots,\xi_n)\mid \xi_j\geq 0,\sum_{j=1}^n\xi_j\leq 1\}$.

Concerning semimodule-categories, we mainly deal with the semirings $\mathbb N$, $\mathbb Q_+$, and $\mathbb R_+$, and their ring completions $\mathbb Z$, $\mathbb Q$, and $\mathbb R$. For these semirings the categories of $\mathbb S$-semimodules are

-   ${{\text{\tt{CMON}}}}$ of commutative monoids for $\mathbb N$,

-   ${{\text{\tt{AB}}}}$ of abelian groups for $\mathbb Z$,

-   ${{\text{\tt{CONE}}}}$ of convex cones for $\mathbb R_+$,

-   ${\text{$\mathbb Q$-{\text{\tt{VEC}}}}}$ and ${\text{$\mathbb R$-{\text{\tt{VEC}}}}}$ of vector spaces over the field of rational and real numbers, respectively, for $\mathbb Q$ and $\mathbb R$.

We consider the following functors, where $A$ is a fixed finite alphabet. Recall that we use the term *cubic functor* for the functor $T1\times(-)^A$ where $T$ is a monad on ${{\text{\tt{Set}}}}$. We chose the name since $T1\times(-)^A$ assigns to objects $X$ a full direct product, i.e., a full cube.

-   The *cubic functor* ${{\ensuremath{F_{\,{\mathbb S}}}}}$ on ${\text{$\mathbb S$-{\text{\tt{SMOD}}}}}$, i.e., the functor acting as $$\begin{aligned}
            & {{\ensuremath{F_{\,{\mathbb S}}}}}X=\mathbb S\times X^A\text{ for }X\text{ object of }{\text{$\mathbb S$-{\text{\tt{SMOD}}}}},
            \\
            & {{\ensuremath{F_{\,{\mathbb S}}}}}f=\operatorname{id}_{\mathbb S}\times(f\circ -)
            \text{ for }f\colon X\to Y\text{ morphism of }{\text{$\mathbb S$-{\text{\tt{SMOD}}}}}.
        \end{aligned}$$ The underlying ${{\text{\tt{Set}}}}$ functors of cubic functors are also sometimes called deterministic-automata functors, see e.g. [@jacobs.silva.sokolova:2015], as their coalgebras are deterministic weighted automata with output in the semiring.

-   The *cubic functor* ${{\ensuremath{F_{\,{[0,1]}}}}}$ on ${{\text{\tt{PCA}}}}$, i.e., the functor ${{\ensuremath{F_{\,{[0,1]}}}}}X=[0,1]\times X^A$ and ${{\ensuremath{F_{\,{[0,1]}}}}}f=\operatorname{id}_{[0,1]}\times(f\circ -)$.

-   A *subcubic convex functor* ${{\ensuremath{\widehat F}}}$ on  whose action will be introduced in Definition \[Ghat-def\].[^2]  The name originates from the fact that ${{\ensuremath{\widehat F}}}X$ is a certain convex subset of ${{\ensuremath{F_{\,{[0,1]}}}}}X$ and that ${{\ensuremath{\widehat F}}}f=({{\ensuremath{F_{\,{[0,1]}}}}}f)|_{{{\ensuremath{\widehat F}}}X}$ for $f\colon X\to Y$.

Cubic functors are liftings of ${{\text{\tt{Set}}}}$-endofunctors, in particular, they preserve surjective algebra homomorphisms. It is easy to see that also the functor ${{\ensuremath{\widehat F}}}$ preserves surjectivity, cf. Lemma \[GhSurj\] (Appendix \[app:D\]) This property is needed to apply the work of Milius, cf. [@milius:2017 Assumptions 3.1].

\[ProperSemiring\] We can now formulate precisely the connection between proper semirings and proper functors mentioned after Definition \[Proper\]. A semiring $\mathbb S$ is proper in the sense of [@esik.maletti:2010], if and only if for every finite input alphabet $A$ the cubic functor ${{\ensuremath{F_{\,{\mathbb S}}}}}$ on ${\text{$\mathbb S$-{\text{\tt{SMOD}}}}}$ is proper.

We shall interchangeably think of direct products as sets of functions or as sets of tuples. Taking the viewpoint of tuples, the definition of ${{\ensuremath{F_{\,{\mathbb S}}}}}f$ reads as $$({{\ensuremath{F_{\,{\mathbb S}}}}}f)\big((o,(x_a)_{a\in A})\big)=\big(o,(f(x_a))_{a\in A}\big),\quad 
    o\in\mathbb S,\ x_a\in X\text{ for }a\in A
    .$$ A coalgebra structure $c\colon X\to{{\ensuremath{F_{\,{\mathbb S}}}}}X$ writes as $$c(x)=\big({{c}_{\text{\rm o}}}(x),({{c}_{a}}(x))_{a\in A}\big),\quad x\in X
    ,$$ and we use ${{c}_{\text{\rm o}}}:X\to\mathbb S$ and ${{c}_{a}}:X\to X$ as generic notation for the components of the map $c$. More generally, we define $c_w\colon X\to X$ for any word $w\in A^*$ inductively as ${{c}_{\varepsilon}}=\operatorname{id}_X$ and ${{c}_{wa}}={{c}_{a}}\circ{{c}_{w}},\ w\in A^*,a\in A$.

The map from a coalgebra $(X,c)$ into the final ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebra, the *trace map*, is then given as $\operatorname{tr}_c(x)=\big(({{c}_{\text{\rm o}}}\circ{{c}_{w}})(x)\big)_{w\in A^*}$ for $ x\in X$. Behavioural equivalence for cubic functors is the kernel of the trace map.

Properness of cubic functors {#sec-PropernessCubic}
============================

Our proofs of properness in this section and in Section \[sec-PropernessSubcubic\] below start from the following idea. Let $\mathbb S$ be a semiring, and assume we are given two ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebras which have free finitely generated carrier, say $(\mathbb S^{n_1},c_1)$ and $(\mathbb S^{n_2},c_2)$. Moreover, assume $x_1\in\mathbb S^{n_1}$ and $x_2\in\mathbb S^{n_2}$ are two elements having the same trace. For $j=1,2$, let $d_j\colon \mathbb S^{n_1}\times\mathbb S^{n_2}  \to  {{\ensuremath{F_{\,{\mathbb S}}}}}(\mathbb S^{n_1}\times\mathbb S^{n_2})$ be given by $$d_j(y_1, y_2) = \Big({{c_j}_{\text{\rm o}}}(y_j),(({{c_1}_{a}}(y_1),{{c_2}_{a}}(y_2)))_{a\in A}\Big).$$ Denoting by $\pi_j\colon \mathbb S^{n_1}\times\mathbb S^{n_2}\to\mathbb S^{n_j}$ the canonical projections, both sides of the following diagram separately commute. $$\xymatrix@C=15pt@R=10pt@M=7pt{
    \mathbb S^{n_1} \ar[dd]_{c_1}
    && \mathbb S^{n_1}\times\mathbb S^{n_2} \ar[ll]_{\pi_1} \ar[rr]^{\pi_2} 
        \ar@/_15pt/[dd]_{d_1} \ar@/^15pt/[dd]^{d_2} 
    && \mathbb S^{n_2} \ar[dd]_{c_2}
    \\
    && \neq &&
    \\
    {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_1} 
    && {{\ensuremath{F_{\,{\mathbb S}}}}}(\mathbb S^{n_1}\times\mathbb S^{n_2}) \ar[ll]_{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_1} \ar[rr]^{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_2}
    && {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_2}
}$$ However, in general the maps $d_1$ and $d_2$ do not coincide.

The next lemma contains a simple observation: there exists a subsemimodule $Z$ of $\mathbb S^{n_1}\times\mathbb S^{n_2}$, such that the restrictions of $d_1$ and $d_2$ to $Z$ coincide and turn $Z$ into an ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebra.

\[Prod\] Let $Z$ be the subsemimodule of $\mathbb S^{n_1}\times\mathbb S^{n_2}$ generated by the pairs $({{c_1}_{w}}(x_1),{{c_2}_{w}}(x_2))$ for $w \in A^*$. Then $d_1|_Z=d_2|_Z$ and $d_j(Z)\subseteq{{\ensuremath{F_{\,{\mathbb S}}}}}(Z)$.

The significance of Lemma \[Prod\] in the present context is that it leads to the diagram (we denote $d=d_j|_Z$) $$\xymatrix@C=15pt@R=35pt@M=7pt{
    \mathbb S^{n_1} \ar[d]_{c_1}
    && Z \ar[ll]_{\pi_1} \ar[rr]^{\pi_2} \ar[d]^d 
        \save[]+<3pt,10pt>*\txt{\begin{rotate}{90}$\subseteq$\end{rotate}}\restore
        \save[]+<2pt,27pt>*\txt{$\mathbb S^{n_1}\!\!\times\mathbb S^{n_2}$}\restore
    && \mathbb S^{n_2} \ar[d]_{c_2}
    \\
    {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_1} 
    && {{\ensuremath{F_{\,{\mathbb S}}}}}Z \ar[ll]_{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_1} \ar[rr]^{{{\ensuremath{F_{\,{\mathbb S}}}}}\pi_2}
        \save[]+<-3pt,-10pt>*\txt{\begin{rotate}{-90}$\subseteq$\end{rotate}}\restore
        \save[]+<2pt,-29pt>*\txt{$\mathbb S\!\!\times(\mathbb S^{n_1}\!\!\times\mathbb S^{n_2})^A$}\restore
    && {{\ensuremath{F_{\,{\mathbb S}}}}}\mathbb S^{n_2}
}$$ In other words, it leads to the zig-zag in [[Coalg]{}([${{\ensuremath{F_{\,{\mathbb S}}}}}$]{})]{} $$\label{ZZ}
\xymatrix@C=40pt{
    (\mathbb S^{n_1},c_1) & (Z,d) \ar[l]_{\mkern20mu\pi_1} \ar[r]^{\pi_2\mkern20mu} 
    & (\mathbb S^{n_2},c_2) 
}$$ This zig-zag relates $x_1$ with $x_2$ since $(x_1,x_2)\in Z$. If it can be shown that $Z$ is always finitely generated, it will follow that ${{\ensuremath{F_{\,{\mathbb S}}}}}$ is proper.

Let $\mathbb S$ be a Noetherian semiring, i.e., a semiring such that every $\mathbb S$-subsemimodule of some finitely generated $\mathbb S$-semimodule is itself finitely generated. Then $Z$ is, as an $\mathbb S$-subsemimodule of $\mathbb S^{n_1}\times\mathbb S^{n_2}$ finitely generated. Hence, we reobtain the result [@esik.maletti:2010 Theorem 4.2] of Esik and Maletti.

\[Noetherian\] Every Noetherian semiring is proper.

Our first main result is Theorem \[CubProp\] below, where we show properness of the cubic functors ${{\ensuremath{F_{\,{\mathbb S}}}}}$ on , for $\mathbb S$ being one of the semirings $\mathbb N$, $\mathbb Q_+$, $\mathbb R_+$, and of the cubic functor ${{\ensuremath{F_{\,{[0,1]}}}}}$ on . The case of ${{\ensuremath{F_{\,{\mathbb N}}}}}$ is known from [@beal.lombardy.sakarovitch:2006 Theorem 4] [^3], the case of ${{\ensuremath{F_{\,{[0,1]}}}}}$ is stated as an open problem in [@milius:2017 Example 3.19].

\[CubProp\] The cubic functors ${{\ensuremath{F_{\,{\mathbb N}}}}}$, ${{\ensuremath{F_{\,{\mathbb Q_+}}}}}$, ${{\ensuremath{F_{\,{\mathbb R_+}}}}}$, and ${{\ensuremath{F_{\,{[0,1]}}}}}$ are proper.

In fact, for any two coalgebras with free finitely generated carrier and any two elements having the same trace, a zig-zag with free and finitely generated nodes relating those elements can be found, which is a span (has a single intermediate node with outgoing arrows).

The proof proceeds via relating to the Noetherian case. It always follows the same scheme, which we now outline. Observe that the ring completion of each of $\mathbb N$, $\mathbb Q_+$, $\mathbb R_+$, is Noetherian (for the last two it actually is a field), and that $[0,1]$ is the positive part of the unit ball in $\mathbb R$.

*Step 1. The extension lemma:*  We use an extension of scalars process to pass from the given category to an associated category E with a Noetherian ring $\mathbb E$. This is a general categorical argument.

To unify notation, we agree that $\mathbb S$ may also take the value $[0,1]$, and that $T_{[0,1]}$ is the monad of finitely supported subprobability distributions giving rise to the category .

  $\mathbb S$   $\mathbb N$   $\mathbb Q_+$   $\mathbb R_+$   $[0,1]$
  ------------- ------------- --------------- --------------- ---------
                N ()                          ()              
  E             Z ()          Q (Q)           R (R)           R (R)

For the formulation of the extension lemma, recall that the starting category is the Eilenberg-Moore category of the monad ${T_{\mathbb{S}}}$ and the target category E is the Eilenberg-Moore category of ${T_{\mathbb{E}}}$. We write $\eta_{\mathbb S}$ and $\mu_{\mathbb S}$ for the unit and multiplication of ${T_{\mathbb{S}}}$ and analogously for ${T_{\mathbb{E}}}$. We have ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$, via the inclusion monad morphism $\iota\colon {T_{\mathbb{S}}}\Rightarrow {T_{\mathbb{E}}}$ given by $\iota_X(u) = u$, as $\eta_{\mathbb E} = \iota {\mathrel{\circ}}\eta_{\mathbb S}$ and $\mu_{\mathbb E} {\mathrel{\circ}}\iota\iota =\iota{\mathrel{\circ}}\mu_{\mathbb S}$ where $\iota\iota \stackrel{\text{def}}{=}{T_{\mathbb{E}}}\iota{\mathrel{\circ}}\iota \stackrel{\text{nat.}}{=} \iota {\mathrel{\circ}}{T_{\mathbb{S}}}\iota$. Recall that a monad morphism $\iota\colon T_\mathbb S \to T_\mathbb E$ defines a functor $M_\iota\colon {{\text{\tt{Set}}}^{T_\mathbb E}} \to {{\text{\tt{Set}}}^{T_\mathbb S}}$ which maps a $T_\mathbb E$-algebra $(X, \alpha_X)$ to $(X, \iota_X{\mathrel{\circ}}\alpha_X)$ and is identity on morphisms. Obviously, $M_\iota$ commutes with the forgetful functors $U_\mathbb S: {{\text{\tt{Set}}}^{T_\mathbb S}} \to {{\text{\tt{Set}}}}$ and $U_\mathbb E: {{\text{\tt{Set}}}^{T_\mathbb E}} \to {{\text{\tt{Set}}}}$, i.e., $U_\mathbb S {\mathrel{\circ}}M_\iota = U_\mathbb E$.

Let $(X, \alpha_X) \in {{\text{\tt{Set}}}^{{T_{\mathbb{S}}}}}$ and $(Y, \alpha_Y) \in {{\text{\tt{Set}}}^{{T_{\mathbb{E}}}}}$ where ${T_{\mathbb{S}}}$ and ${T_{\mathbb{E}}}$ are monads with ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$ via $\iota\colon {T_{\mathbb{S}}}\Rightarrow {T_{\mathbb{E}}}$. A ${{\text{\tt{Set}}}}$-arrow $h\colon X \to Y$ is a ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphism from $(X,\alpha_X)$ to $(Y,\alpha_Y)$ if and only if the following diagram commutes (in ${{\text{\tt{Set}}}}$) $$\xymatrix@R=0.7em{
    {T_{\mathbb{S}}}X \ar[rr]^{\iota h} \ar[d]_{\alpha_X}&& {T_{\mathbb{E}}}Y \ar[d]^{\alpha_Y}\\
    X \ar[rr]^{h}&& Y
    }$$ where $\iota h$ denotes the map $\iota h \stackrel{\text{def}}{=} {T_{\mathbb{E}}}h{\mathrel{\circ}}\iota_X \stackrel{\text{nat.}}{=} \iota_Y {\mathrel{\circ}}{T_{\mathbb{S}}}h$. In other words, a ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphism from $(X,\alpha_X)$ to $(Y,\alpha_Y)$ is a morphism in ${{\text{\tt{Set}}}^{T_\mathbb S}}$ from $(X,\alpha_X)$ to $M(Y,\alpha_Y)$.

Now we can formulate the extension lemma.

\[prop:ext-lem\] For every ${{\ensuremath{F_{\,{\mathbb{S}}}}}}$-coalgebra ${T_{\mathbb{S}}}B \stackrel{c}{\to} {{\ensuremath{F_{\,{\mathbb{S}}}}}}({T_{\mathbb{S}}}B)$ with free finitely generated carrier ${T_{\mathbb{S}}}B$ for a finite set $B$, there exists an ${{\ensuremath{F_{\,{\mathbb{E}}}}}}$-coalgebra ${T_{\mathbb{E}}}B \stackrel{\tilde c}{\to} {{\ensuremath{F_{\,{\mathbb{E}}}}}}({T_{\mathbb{E}}}B)$ with free finitely generated carrier ${T_{\mathbb{E}}}B$ such that $$\xymatrix@R=0.7em{
            {T_{\mathbb{S}}}B \ar[rr]^{\iota_B} \ar[d]_{c}&& {T_{\mathbb{E}}}B \ar[d]^{\tilde c}\\
            {{\ensuremath{F_{\,{\mathbb{S}}}}}}({T_{\mathbb{S}}}B) \ar[rr]^{\iota_1 \times (\iota_B)^A}&& {{\ensuremath{F_{\,{\mathbb{E}}}}}}({T_{\mathbb{E}}}B)
        }$$ where the horizontal arrows ($\iota_B$ and $\iota_1 \times \iota_B^A$) are ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphisms, and moreover they both amount to inclusion.

*Step 2. The basic diagram:*  Let $n_1,n_2\in\mathbb N$, let $B_j$ be the $n_j$-element set consisting of the canonical basis vectors of $\mathbb E^{n_j}$, and set $X_j=T_{\mathbb S}B_j$. Assume we are given ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebras $(X_1,c_1)$ and $(X_2,c_2)$, and elements $x_j\in X_j$ with $\operatorname{tr}_{c_1}x_1=\operatorname{tr}_{c_2}x_2$.

The extension lemma provides ${{\ensuremath{F_{\,{\mathbb E}}}}}$-coalgebras $(\mathbb E^{n_j},\tilde c_j)$ with $\tilde c_j|_{X_j}=c_j$. Clearly, $\operatorname{tr}_{\tilde c_1}x_1=\operatorname{tr}_{\tilde c_2}x_2$. Using the zig-zag diagram in [[Coalg]{}([$F_{\mathbb E}$]{})]{} and appending inclusion maps, we obtain what we call the *basic diagram*. In this diagram all solid arrows are arrows in E, and all dotted arrows are arrows in . The horizontal dotted arrows denote the inclusion maps, and $\pi_j$ are the restrictions to $Z$ of the canonical projections. $$\xymatrix@C=15pt@R=35pt@M=7pt{
        X_1 \ar@{.>}[r] \ar@{.>}[d]_{c_1} & \mathbb E^{n_1} \ar[d]_{\tilde c_1}
        && Z \ar[ll]_{\pi_1} \ar[rr]^{\pi_2} \ar[d]^d 
            \save[]+<3pt,10pt>*\txt{\begin{rotate}{90}$\subseteq$\end{rotate}}\restore
            \save[]+<2pt,27pt>*\txt{$\mathbb E^{n_1}\!\!\times\mathbb E^{n_2}$}\restore
        && \mathbb E^{n_2} \ar[d]_{\tilde c_2} & X_2 \ar@{.>}[l] \ar@{.>}[d]^{c_2}
        \\
        {{\ensuremath{F_{\,{\mathbb S}}}}}X_1 \ar@{.>}[r] & {{\ensuremath{F_{\,{\mathbb E}}}}}\mathbb E^{n_1} 
        && {{\ensuremath{F_{\,{\mathbb E}}}}}Z \ar[ll]_{{{\ensuremath{F_{\,{\mathbb E}}}}}\pi_1} \ar[rr]^{{{\ensuremath{F_{\,{\mathbb E}}}}}\pi_2}
            \save[]+<-3pt,-10pt>*\txt{\begin{rotate}{-90}$\subseteq$\end{rotate}}\restore
            \save[]+<2pt,-29pt>*\txt{$\mathbb E\!\!\times(\mathbb E^{n_1}\!\!\times\mathbb E^{n_2})^A$}\restore
        && {{\ensuremath{F_{\,{\mathbb E}}}}}\mathbb E^{n_2} & {{\ensuremath{F_{\,{\mathbb S}}}}}X_2 \ar@{.>}[l]
    }$$ Commutativity of this diagram yields $d\big(\pi_j^{-1}(X_j)\big)\subseteq({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_j)^{-1}\big({{\ensuremath{F_{\,{\mathbb S}}}}}X_j)$ for $j=1,2$. Now we observe the following properties of cubic functors.

\[CubProperties\] We have ${{\ensuremath{F_{\,{\mathbb E}}}}}X\cap{{\ensuremath{F_{\,{\mathbb S}}}}}Y={{\ensuremath{F_{\,{\mathbb S}}}}}(X\cap Y)$. Moreover, if $Y_j\subseteq X_j$, then $({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_1)^{-1}({{\ensuremath{F_{\,{\mathbb S}}}}}Y_1)\cap({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_2)^{-1}({{\ensuremath{F_{\,{\mathbb S}}}}}Y_2)
        ={{\ensuremath{F_{\,{\mathbb S}}}}}(Y_1\times Y_2)$.

Using this, yields $$\begin{aligned}
        d\big(Z\cap(X_1\times X_2)\big)\subseteq &\, 
        {{\ensuremath{F_{\,{\mathbb E}}}}}Z\cap({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_1)^{-1}\big({{\ensuremath{F_{\,{\mathbb S}}}}}X_1)
        \cap({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_2)^{-1}\big({{\ensuremath{F_{\,{\mathbb S}}}}}X_2)
        \\
        = &\, {{\ensuremath{F_{\,{\mathbb E}}}}}Z\cap{{\ensuremath{F_{\,{\mathbb S}}}}}(X_1\times X_2)={{\ensuremath{F_{\,{\mathbb S}}}}}\big(Z\cap(X_1\times X_2)\big)
        .
    \end{aligned}$$ This shows that $Z\cap(X_1\times X_2)$ becomes an ${{\ensuremath{F_{\,{\mathbb S}}}}}$-coalgebra with the restriction $d|_{Z\cap(X_1\times X_2)}$. Again referring to the basic diagram, we have the following zig-zag in [[Coalg]{}([$F_{\mathbb S}$]{})]{} (to shorten notation, denote the restrictions of $d,\pi_1,\pi_2$ to $Z\cap(X_1\times X_2)$ again as $d,\pi_1,\pi_2$): $$\label{4}
        \xymatrix@C=40pt{
        (X_1,c_1) & \big(Z\cap(X_1\times X_2),d\big) 
            \ar[l]_{\pi_1\mkern50mu} \ar[r]^{\mkern60mu\pi_2} 
        & (X_2,c_2)
        }$$ This zig-zag relates $x_1$ with $x_2$ since $(x_1,x_2)\in Z\cap(X_1\times X_2)$.

*Step 3. The reduction lemma:*  In view of the zig-zag , the proof of Theorem \[CubProp\] can be completed by showing that $Z\cap(X_1\times X_2)$ is finitely generated as an algebra in . Since $Z$ is a submodule of the finitely generated module $\mathbb E^{n_1}\times\mathbb E^{n_2}$ over the Noetherian ring $\mathbb E$, it is finitely generated as an $\mathbb E$-module. The task thus is to show that being finitely generated is preserved when reducing scalars.

This is done by what we call the *reduction lemma*. Contrasting the extension lemma, the reduction lemma is not a general categorical fact, and requires specific proof in each situation.

\[RedLem\] Let $n_1,n_2\in\mathbb N$, let $B_j$ be the set consisting of the $n_j$ canonical basis vectors of $\mathbb E^{n_j}$, and set $X_j=T_{\mathbb S}B_j$. Moreover, let $Z$ be an $\mathbb E$-submodule of $\mathbb E^{n_1}\times\mathbb E^{n_2}$. Then $Z\cap(X_1\times X_2)$ is finitely generated as an algebra in .

A subcubic convex functor {#sec-SubcubicFunctor}
=========================

Recall the following definition from [@silva.sokolova:2011 p.309].

\[Ghat-def\] We introduce a functor ${{\ensuremath{\widehat F}}}\colon {{\text{\tt{PCA}}}}\to{{\text{\tt{PCA}}}}$.

1.  Let $X$ be a . Then $$\begin{aligned}
                {{\ensuremath{\widehat F}}}X=\Big\{ (o,\phi)\in[0,1] & \times X^A\mid 
                \\
                & \exists\,n_a\in\mathbb N{{.\kern3pt}}\exists\,p_{a,j}\in[0,1],x_{a,j}\in X\text{ for }j=1,\ldots,n_a,a\in A{{.\kern3pt}}\\
                & o+\sum_{a\in A}\sum_{j=1}^{n_a}p_{a,j}\leq 1,\ \phi(a)=\sum_{j=1}^{n_a}p_{a,j}x_{a,j} \Big\}.
            \end{aligned}$$

2.  Let $X,Y$ be s, and $f\colon X\to Y$ a convex map. Then ${{\ensuremath{\widehat F}}}f\colon {{\ensuremath{\widehat F}}}X\to{{\ensuremath{\widehat F}}}Y$ is the map ${{\ensuremath{\widehat F}}}f=\operatorname{id}_{[0,1]}\times(f\circ -)$.

For every $X$ we have ${{\ensuremath{\widehat F}}}X\subseteq{{\ensuremath{F_{\,{[0,1]}}}}}X$, and for every $f\colon X\to Y$ we have ${{\ensuremath{\widehat F}}}f=({{\ensuremath{F_{\,{[0,1]}}}}}f)|_{{{\ensuremath{\widehat F}}}X}$. For this reason, we think of ${{\ensuremath{\widehat F}}}$ as a *subcubic functor*.

The definition of [[$\widehat F$]{}]{} can be simplified.

\[Ghat-simple\] Let $X$ be a , then $$\begin{aligned}
        {{\ensuremath{\widehat F}}}X=\Big\{ (o,f)\in[0,1]\times X^A\mid\ & 
        \exists\,p_a\in[0,1],x_a\in X\text{ for }a\in A{{.\kern3pt}}\\
        & o+\sum_{a\in A}p_a\leq 1,\ f(a)=p_ax_a \Big\}.
    \end{aligned}$$

From this representation it is obvious that [[$\widehat F$]{}]{} is monotone in the sense that

-   If $X_1\subseteq X_2$, then ${{\ensuremath{\widehat F}}}X_1\subseteq{{\ensuremath{\widehat F}}}X_2$.

-   If $f_1\colon X_1\to Y_1,f_2\colon X_2\to Y_2$ with $X_1\subseteq X_2,Y_1\subseteq Y_2$ and $f_2|_{X_1}=f_1$, then ${{\ensuremath{\widehat F}}}f_2|_{{{\ensuremath{\widehat F}}}X_1}={{\ensuremath{\widehat F}}}f_1$.

Note that [[$\widehat F$]{}]{} does not preserve direct products.

For a  $X$ whose carrier is a compact subset of a euclidean space, ${{\ensuremath{\widehat F}}}X$ can be described with help of a geometric notion, namely using the Minkowksi functional of $X$. Before we can state this fact, we have to make a brief digression to explain this notion and its properties.

\[Minko\] Let $X\subseteq\mathbb R^n$ be a . The *Minkowski functional* of $X$ is the map ${\ensuremath{\mu_{X}}}\colon \mathbb R^n\to[0,\infty]$ defined as ${\ensuremath{\mu_{X}}}(x)=\inf\{t>0\mid x\in tX\}$, where the infimum of the empty set is understood as $\infty$.

Minkowski functionals, sometimes also called *gauge*, are a central and exhaustively studied notion in convex geometry, see, e.g., [@rudin:1991 p.34] or [@rockafellar:1970 p.28].

We list some basic properties whose proof can be found in the mentioned textbooks.

1.  ${\ensuremath{\mu_{X}}}(px)=p{\ensuremath{\mu_{X}}}(x)$ for $x\in\mathbb R^n,p\geq 0$,

2.  ${\ensuremath{\mu_{X}}}(x+y)\leq {\ensuremath{\mu_{X}}}(x)+{\ensuremath{\mu_{X}}}(y)$ for $x,y\in\mathbb R^n$,

3.  ${\ensuremath{\mu_{X\cap Y}}}(x)=\max\{{\ensuremath{\mu_{X}}}(x),{\ensuremath{\mu_{Y}}}(x)\}$ for $x\in\mathbb R^n$.

4.  If $X$ is bounded, then ${\ensuremath{\mu_{X}}}(x)=0$ if and only if $x=0$.

The set $X$ can almost be recovered from ${\ensuremath{\mu_{X}}}$.

5.  ${\displaystyle\{x\in\mathbb R^n\mid{\ensuremath{\mu_{X}}}(x)<1\}\subseteq X\subseteq\{x\in\mathbb R^n\mid{\ensuremath{\mu_{X}}}(x)\leq 1\}}$.

6.  If $X$ is closed, equality holds in the second inclusion of 5.

7.  Let $X,Y$ be closed. Then $X\subseteq Y$ if and only if ${\ensuremath{\mu_{X}}}\geq{\ensuremath{\mu_{Y}}}$.

\[MinkoExa\] As two simple examples, consider the $n$-simplex $\Delta^n\subseteq\mathbb R^n$ and a convex cone $C\subseteq\mathbb R^n$. Then (here $\geq$ denotes the product order on $\mathbb R^n$) $${\ensuremath{\mu_{\Delta^n}}}(x)= 
        \begin{cases}
            \sum_{j=1}^n\xi_j &\hspace*{-3mm},\quad x=(\xi_1,\ldots,\xi_n)\geq 0,
            \\
            \infty &\hspace*{-3mm},\quad \text{otherwise}.
        \end{cases}
        \qquad 
        {\ensuremath{\mu_{C}}}(x)=
        \begin{cases}
            0 &\hspace*{-3mm},\quad x\in C,
            \\
            \infty &\hspace*{-3mm},\quad \text{otherwise}.
        \end{cases}$$ Observe that $\Delta^n=\{x\in\mathbb R^n\mid {\ensuremath{\mu_{\Delta^n}}}(x)\leq 1\}$.

Another illustrative example is given by general pyramids in a euclidean space. This example will play an important role later on.

\[Pyramid\] For $u\in\mathbb R^n$ consider the set $$X=\big\{x\in\mathbb R^n\mid x\geq 0\text{ and }(x,u)\leq 1\big\}
        ,$$ where $(\cdot,\cdot)$ denotes the euclidean scalar product on $\mathbb R^n$. The set $X$ is intersection of the cone $\mathbb R_+^n$ with the half-space given by the inequality $(x,u)\leq 1$, hence it is convex and contains $0$. Thus $X$ is a .

Let us first assume that $u$ is strictly positive, i.e., $u\geq 0$ and no component of $u$ equals zero. Then $X$ is a pyramid (in $2$-dimensional space, a triangle).

(0,0) – (0,4-5/12) – (11-12/5,0) – (0,0); (0,0) – (12,0); (0,0) – (0,5); (-1,4) – (11,-1); (0,0) – (1,1\*12/5); at (0.6,2.5) [[$u$]{}]{}; at (2.9,1.1) [[$X$]{}]{}; at (-2.4,4.5) [[$\scriptstyle(x,u)=1$]{}]{};

The $n$-simplex $\Delta^n$ is of course a particular pyramid. It is obtained using the vector $u=(1,\ldots,1)$.

The Minkowski functional of the pyramid $X$ associated with $u$ is $${\ensuremath{\mu_{X}}}(x)=
        \begin{cases}
            (x,u) &\hspace*{-3mm},\quad x\geq 0,
            \\
            \infty &\hspace*{-3mm},\quad \text{otherwise}.
        \end{cases}$$ Write $u=\sum_{j=1}^n\alpha_je_j$, where $e_j$ is the $j$-th canonical basis vector, and set $y_j=\frac 1{\alpha_j}e_j$. Clearly, $\{y_1,\ldots,y_n\}$ is linearly independent. Each vector $x=\sum_{j=1}^n\xi_je_j$ can be written as $x=\sum_{j=1}^n(\xi_j\alpha_j)y_j$, and this is a subconvex combination if and only if $\xi_j\geq 0$ and $\sum_{j=1}^n\xi_j\alpha_j\leq 1$, i.e., if and only if $x\in X$. Thus $X$ is generated by $\{y_1,\ldots,y_n\}$ as a .

The linear map given by the diagonal matrix made up of the $\alpha_j$’s induces a bijection of $X$ onto $\Delta^n$, and maps the $y_j$’s to the corner points of $\Delta^n$. Hence, $X$ is free with basis $\{y_1,\ldots,y_n\}$.

If $u$ is not strictly positive, the situation changes drastically. Then $X$ is not finitely generated as a , because it is unbounded whereas the subconvex hull of a finite set is certainly bounded.

(0,0) – (0,2) – (16,4) – (16,0) – (0,0); (0,0) – (12,0); (0,0) – (0,5); (-1,2-1/8) – (16,4); (0,0) – (-3/8,3); at (-0.8,3.2) [[$u$]{}]{}; at (9.5,1.7) [[$X$]{}]{}; at (14.8,5.0) [[$\scriptstyle(x,u)=1$]{}]{};

Now we return to the functor [[$\widehat F$]{}]{}.

\[Ghat-Minko\] Let $X\subseteq\mathbb R^n$ be a , and assume that $X$ is compact. Then $${{\ensuremath{\widehat F}}}X=\Big\{(o,\phi)\in\mathbb R\times(\mathbb R^n)^A\mid\ 
        o\geq 0,\ o+\sum_{a\in A}{\ensuremath{\mu_{X}}}(\phi(a))\leq 1 \Big\}
        .$$

In the following we use the elementary fact that every convex map has a linear extension.

\[LinExt\] Let $V_1,V_2$ be vector spaces, let $X\subseteq V_1$ be a , and let $c\colon X\to V_2$ be a convex map. Then $c$ has a linear extension $\tilde c\colon V_1\to V_2$. If $\operatorname{span}X=V_1$, this extension is unique.

Rescaling in this representation of ${{\ensuremath{\widehat F}}}X$ leads to a characterisation of [[$\widehat F$]{}]{}-coalgebra maps. We give a slightly more general statement; for the just said, use $X=Y$.

\[Ghat-Minko-Coalg\] Let $X,Y\subseteq\mathbb R^n$ be s, and assume that $X$ and $Y$ are compact. Further, let $c\colon X\to\mathbb R_+\times(\mathbb R^n)^A$ be a convex map, and let $\tilde c\colon \mathbb R^n\to\mathbb R\times(\mathbb R^n)^A$ be a linear extension of $c$.

Then $c(X)\subseteq{{\ensuremath{\widehat F}}}Y$, if and only if $$\label{2}
        {{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}{\ensuremath{\mu_{Y}}}({{\tilde c}_{a}}(x))\leq{\ensuremath{\mu_{X}}}(x),\quad x\in\mathbb R^n
        .$$

An extension theorem for ${{\ensuremath{\widehat F}}}$-coalgebras {#sec-ExtensionTheorem}
=================================================================

In this section we establish an extension theorem for ${{\ensuremath{\widehat F}}}$-coalgebras. It states that an ${{\ensuremath{\widehat F}}}$-coalgebra, whose carrier has a particular geometric form, can, under a mild additional condition, be embedded into an ${{\ensuremath{\widehat F}}}$-coalgebra whose carrier is free and finitely generated.

\[ExEx\] Let $(X,c)$ be an ${{\ensuremath{\widehat F}}}$-coalgebra whose carrier $X$ is a compact subset of a euclidean space $\mathbb R^n$ with $\Delta^n\subseteq X\subseteq\mathbb R_+^n$. Assume that the output map ${{c}_{\text{\rm o}}}$ does not vanish on invariant coordinate hyperplanes in the sense that ($e_j$ denotes again the $j$-th canonical basis vector in $\mathbb R^n$) $$\label{nv}
        \begin{aligned}
        & \nexists\,I\subseteq\{1,\ldots,n\}{{.\kern3pt}}\\
        & I\neq\emptyset,\quad 
            {{c}_{\text{\rm o}}}(e_j)=0,j\in I,
            \quad
            {{c}_{a}}(e_j)\subseteq\operatorname{span}\{e_i\mid i\in I\},a\in A,j\in I.
        \end{aligned}$$ Then there exists an ${{\ensuremath{\widehat F}}}$-coalgebra $(Y,d)$, such that $X\subseteq Y\subseteq\mathbb R_+^n$, the inclusion map $\iota\colon X\to Y$ is a ${{\sf Coalg}({{{\ensuremath{\widehat F}}}})}$-morphism, and $Y$ is the subconvex hull of $n$ linearly independent vectors (in particular, $Y$ is free with $n$ generators).

The idea of the proof can be explained by geometric intuition. Say, we have an ${{\ensuremath{\widehat F}}}$-coalgebra $(X,c)$ of the stated form, and let $\tilde c\colon \mathbb R^n\to\mathbb R\times(\mathbb R^n)^A$ be the linear extension of $c$ to all of $\mathbb R^n$, cf. Lemma \[LinExt\].

(0,0) – (0,2) to \[out=20,in=0\] (3,0) – (0,0); (0,0) – (12,0); (0,0) – (0,5); at (0,1.5) [[$\bullet$]{}]{}; at (-0.5,1.5) [[$e_2$]{}]{}; at (1.5,0) [[$\bullet$]{}]{}; at (1.5,-0.5) [[$e_1$]{}]{}; at (14,1.4) [${{\ensuremath{\widehat F}}}X$]{}; (0,2) to \[out=20,in=0\] (3,0); at (1.4,0.9) [[$X$]{}]{}; (3,1.4) to \[out=20,in=160\] (13,1.4); at (8,3) [$c=\tilde c|_X$]{};

Remembering that pyramids are free and finitely generated, we will be done if we find a pyramid $Y\supseteq X$ which is mapped into ${{\ensuremath{\widehat F}}}Y$ by $\tilde c$:

(0,0) – (0,2) to \[out=20,in=0\] (3,0) – (0,0); (0,0) – (0,4-5/12) – (11-12/5,0) – (0,0); (0,0) – (12,0); (0,0) – (0,5); at (0,1.5) [[$\bullet$]{}]{}; at (-0.5,1.5) [[$e_2$]{}]{}; at (1.5,0) [[$\bullet$]{}]{}; at (1.5,-0.5) [[$e_1$]{}]{}; at (14,1.4) [${{\ensuremath{\widehat F}}}X$]{}; (0,2) to \[out=20,in=0\] (3,0); at (1.4,0.9) [[$X$]{}]{}; (3,1.4) to \[out=20,in=160\] (13,1.4); at (8,3) [$c=\tilde c|_X$]{}; (-1,4) – (11,-1); at (4.2,1) [[$Y$]{}]{}; at (14,3.4) [${{\ensuremath{\widehat F}}}Y$]{}; at (14.1,2.15)

[90]{} $\subseteq$

; (2,3.4) to \[out=20,in=160\] (13,3.4); at (8,5) [$\tilde c|_Y$]{};

This task can be reformulated as follows: For each pyramid $Y_1$ containing $X$ let $P(Y_1)$ be the set of all pyramids $Y_2$ containing $X$, such that $\tilde c(Y_2)\subseteq{{\ensuremath{\widehat F}}}Y_1$. If we find $Y$ with $Y\in P(Y)$, we are done.

Existence of $Y$ can be established by applying a fixed point principle for set-valued maps. The result sufficient for our present level of generality is Kakutani’s generalisation [@kakutani:1941 Corollary] of Brouwers fixed point theorem.

Properness of [[$\widehat F$]{}]{} {#sec-PropernessSubcubic}
==================================

In this section we give the second main result of the paper.

\[GhatProp\] The functor ${{\ensuremath{\widehat F}}}$ is proper.

In fact, for each two given coalgebras with free finitely generated carrier and each two elements having the same trace, a zig-zag with free and finitely generated nodes relating those elements can be found, which has three intermediate nodes with the middle one forming a span.

We try to follow the proof scheme familiar from the cubic case. Assume we are given two ${{\ensuremath{\widehat F}}}$-coalgebras with free finitely generated carrier, say $(\Delta^{n_1},c_1)$ and $(\Delta^{n_2},c_2)$, and elements $x_1\in\Delta^{n_1}$ and $x_2\in\Delta^{n_2}$ having the same trace. Since ${{\ensuremath{\widehat F}}}\Delta^{n_j}\subseteq\mathbb R\times(\mathbb R^{n_j})^A$ we can apply Lemma \[LinExt\] and obtain ${{\ensuremath{F_{\,{\mathbb R}}}}}$-coalgebras $(\mathbb R^{n_j},\tilde c_j)$ with $\tilde c_j|_{\Delta^{n_j}}=c_j$. This leads to the basic diagram: $$\xymatrix@C=15pt@R=35pt@M=7pt{
    \Delta^{n_1} \ar@{.>}[r] \ar@{.>}[d]_{c_1} & \mathbb R^{n_1} \ar[d]_{\tilde c_1}
    && Z \ar[ll]_{\pi_1} \ar[rr]^{\pi_2} \ar[d]^d 
        \save[]+<3pt,10pt>*\txt{\begin{rotate}{90}$\subseteq$\end{rotate}}\restore
        \save[]+<2pt,27pt>*\txt{$\mathbb R^{n_1}\!\!\times\mathbb R^{n_2}$}\restore
    && \mathbb R^{n_2} \ar[d]_{\tilde c_2} & \Delta^{n_2} \ar@{.>}[l] \ar@{.>}[d]^{c_2}
    \\
    {{\ensuremath{\widehat F}}}\Delta^{n_1} \ar@{.>}[r] & {{\ensuremath{F_{\,{\mathbb R}}}}}\mathbb R^{n_1} 
    && {{\ensuremath{F_{\,{\mathbb R}}}}}Z \ar[ll]_{{{\ensuremath{F_{\,{\mathbb R}}}}}\pi_1} \ar[rr]^{{{\ensuremath{F_{\,{\mathbb R}}}}}\pi_2}
        \save[]+<-3pt,-10pt>*\txt{\begin{rotate}{-90}$\subseteq$\end{rotate}}\restore
        \save[]+<2pt,-29pt>*\txt{$\mathbb R\!\!\times(\mathbb R^{n_1}\!\!\times\mathbb R^{n_2})^A$}\restore
    && {{\ensuremath{F_{\,{\mathbb R}}}}}\mathbb R^{n_2} & {{\ensuremath{\widehat F}}}\Delta^{n_2} \ar@{.>}[l]
}$$ At this point the line of argument known from the cubic case breaks: it is *not* granted that $Z\cap(\Delta^{n_1}\times \Delta^{n_2})$ becomes an ${{\ensuremath{\widehat F}}}$-coalgebra with the restriction of $d$.

The substitute for $Z\cap(\Delta^{n_1}\times \Delta^{n_2})$ suitable for proceeding one step further is given by the following lemma, where we tacitly identify $\mathbb R^{n_1}\times\mathbb R^{n_2}$ with $\mathbb R^{n_1+n_2}$.

\[GhatRestr\] We have $d(Z\cap 2\Delta^{n_1+n_2})\subseteq{{\ensuremath{\widehat F}}}(Z\cap 2\Delta^{n_1+n_2})$.

This shows that $Z\cap 2\Delta^{n_1+n_2}$ becomes an ${{\ensuremath{\widehat F}}}$-coalgebra with the restriction of $d$. Still, we cannot return to the usual line of argument: it is *not* granted that $\pi_j(Z\cap 2\Delta^{n_1+n_2})\subseteq\Delta^{n_j}$. This forces us to introduce additional nodes to produce a zig-zag in ${{\sf Coalg}({{{\ensuremath{\widehat F}}}})}$. These additional nodes are given by the following lemma. There $\operatorname{co}( -)$ denotes the convex hull.

\[GhatNodes\] Set $Y_j=\operatorname{co}(\Delta^{n_j}\cup\pi_j(Z\cap 2\Delta^{n_1+n_2}))$. Then $\tilde c_j(Y_j)\subseteq{{\ensuremath{\widehat F}}}Y_j$.

This shows that $Y_j$ becomes an ${{\ensuremath{\widehat F}}}$-coalgebra with the restriction of $\tilde c_j$. We are led to a zig-zag in ${{\sf Coalg}({{{\ensuremath{\widehat F}}}})}$: $$\xymatrix@C=25pt{
    (\Delta^{n_1},c_1) \ar[r]^{\subseteq} 
    & (Y_1,\tilde c_1) & \big(Z\cap 2\Delta^{n_1+n_2},d\big) \ar[l]_{\pi_1\mkern40mu} \ar[r]^{\mkern40mu\pi_2} 
    & (Y_2,\tilde c_2) & (\Delta^{n_2},c_2) \ar[l]_{\supseteq}
}$$ This zig-zag relates $x_1$ and $x_2$ since $(x_1,x_2)\in Z\cap 2\Delta^{n_1+n_2}$.

Using Minkowski’s Theorem and the argument from Lemma \[RedLemPca\] (Appendix \[app:B\]) shows that the middle node has finitely generated carrier. The two nodes with incoming arrows are, as convex hulls of two finitely generated s, of course also finitely generated. But in general they will not be free (and this is essential, remember Remark \[fg\]). Now Theorem \[ExEx\] comes into play.

\[GhatFree\] Assume that each of $(\Delta^{n_1},c_1)$ and $(\Delta^{n_2},c_2)$ satisfies the following condition: $$\label{nv2}
        \begin{aligned}
        & \nexists\,I\subseteq\{1,\ldots,n\}{{.\kern3pt}}\\
        & I\neq\emptyset,\ 
            {{c_j}_{\text{\rm o}}}(e_k)=0,k\in I,
            \ 
            {{c_j}_{a}}(e_k)\subseteq\operatorname{co}(\{e_i\mid i\in I\}\cup\{0\}),a\in A,k\in I.
        \end{aligned}$$ Then there exist free finitely generated s $U_j$ with $Y_j\subseteq U_j\subseteq\mathbb R_+^{n_j}$ which satisfy $\tilde c_j(U_j)\subseteq{{\ensuremath{\widehat F}}}U_j$.

This shows that $U_j$, under the additional assumption on $(\Delta^{n_j},c_j)$, becomes an ${{\ensuremath{\widehat F}}}$-coalgebra with the restriction of $\tilde c_j$. Thus we have a zig-zag in ${{\sf Coalg}({{{\ensuremath{\widehat F}}}})}$ relating $x_1$ and $x_2$ whose nodes with incoming arrows are free and finitely generated, and whose node with outgoing arrows is finitely generated: $$\xymatrix@C=25pt{
    (\Delta^{n_1},c_1) \ar@{.>}[r]^{\subseteq} \ar[rd]
    & (Y_1,\tilde c_1) \ar@{.>}[d]
        \save[]+<6pt,-15pt>*\txt{\begin{rotate}{-90}$\scriptstyle\subseteq$\end{rotate}}\restore
    & \big(Z\cap 2\Delta^{n_1+n_2},d\big) \ar@{.>}[l]_{\pi_1\mkern40mu} \ar@{.>}[r]^{\mkern40mu\pi_2} \ar[ld] \ar[rd]
    & (Y_2,\tilde c_2) \ar@{.>}[d]
        \save[]+<-9pt,-15pt>*\txt{\begin{rotate}{-90}$\scriptstyle\subseteq$\end{rotate}}\restore
    & (\Delta^{n_2},c_2) \ar@{.>}[l]_{\supseteq} \ar[ld]
    \\
    & (U_1,\tilde c_1)
    && (U_2,\tilde c_2) &
}$$ Removing the additional assumption on $(\Delta^{n_j},c_j)$ is an easy exercise.

\[GhatRedLem\] Let $(\Delta^n,c)$ be an ${{\ensuremath{\widehat F}}}$-coalgebra. Assume that $I$ is a nonempty subset of $\{1,\ldots,n\}$ with $$\label{6}
        {{c}_{\text{\rm o}}}(e_k)=0,\ k\in I\quad\text{and}\quad 
        {{c}_{a}}(e_k)\in\operatorname{co}\big(\{e_i\mid i\in I\}\cup\{0\}\big),\ a\in A,k\in I.$$ Let $X$ be the free  with basis $\{e_k\mid k\in\{1,\ldots,n\}\setminus I\}$, and let $f\colon \Delta^n\to X$ be the -morphism with $$f(e_k)=
        \begin{cases}
            0 &\hspace*{-3mm},\quad k\in I,
            \\
            e_k &\hspace*{-3mm},\quad k\not\in I.
        \end{cases}$$ Further, let $g\colon X\to[0,1]\times X^A$ be the -morphism with $$g(e_k)=\Big({{c}_{\text{\rm o}}}(e_k),\big(f({{c}_{a}}(e_k))\big)_{a\in A}\Big),\quad k\in\{1,\ldots,n\}\setminus I
        .$$ Then $(X,g)$ is an ${{\ensuremath{\widehat F}}}$-coalgebra, and $f$ is an ${{\ensuremath{\widehat F}}}$-coalgebra morphism of $(\Delta^n,c)$ onto $(X,g)$.

\[GhatRedCor\] Let $(\Delta^n,c)$ be an ${{\ensuremath{\widehat F}}}$-coalgebra. Then there exists $k\leq n$, an ${{\ensuremath{\widehat F}}}$-coalgebra $(\Delta^k,g)$, such that $(\Delta^k,g)$ satisfies the assumption in Lemma \[GhatFree\] and such that there exists an ${{\ensuremath{\widehat F}}}$-coalgebra map $f$ of $(\Delta^n,c)$ onto $(\Delta^k,g)$.

The proof of Theorem \[GhatProp\] is now finished by putting together what we showed so far. Starting with ${{\ensuremath{\widehat F}}}$-coalgebras $(\Delta^{n_j},c_j)$ without any additional assumptions, and elements $x_j\in\Delta^{n_j}$ having the same trace, we first reduce by means of Corollary \[GhatRedCor\] and then apply Lemma \[GhatFree\]. This gives a zig-zag as required: $$\xymatrix@C=17pt@M=3pt{
    (\Delta^{n_1},c_1) \ar@{.>}[d]_{\psi_1} \ar[rd]
    && \big(Z\cap 2\Delta^{k_1+k_2},d\big) \ar[ld] \ar[rd] &&
    (\Delta^{n_2},c_2) \ar@{.>}[d]_{\psi_2} \ar[ld]
    \\
    (\Delta^{k_1},g_1) \ar@{.>}[r]
    & (U_1,\tilde g_1) & 
    & (U_2,\tilde g_2) & (\Delta^{k_2},g_2) \ar@{.>}[l]
}$$ and completes the proof of properness of ${{\ensuremath{\widehat F}}}$.

\#1[0=]{}

[10]{} \[1\][`#1`]{}

Bachem, A.: The theorem of [M]{}inkowski for polyhedral monoids and aggregated linear [D]{}iophantine systems. In: Optimization and operations research ([P]{}roc. [W]{}orkshop, [U]{}niv. [B]{}onn, [B]{}onn, 1977), Lecture Notes in Econom. and Math. Systems, vol. 157, pp. 1–13. Springer, Berlin-New York (1978)

B[é]{}al, M., Lombardy, S., Sakarovitch, J.: On the equivalence of [Z]{}-automata. In: Automata, Languages and Programming, 32nd International Colloquium, [ICALP]{} 2005, Lisbon, Portugal, July 11-15, 2005, Proceedings. pp. 397–409 (2005), <https://doi.org/10.1007/11523468_33>

B[é]{}al, M., Lombardy, S., Sakarovitch, J.: Conjugacy and equivalence of weighted automata and functional transducers. In: Computer Science - Theory and Applications, First International Computer Science Symposium in Russia, [CSR]{} 2006, St. Petersburg, Russia, June 8-12, 2006, Proceedings. pp. 58–69 (2006), <https://doi.org/10.1007/11753728_9>

Bloom, S.L., [É]{}sik, Z.: Iteration Theories - The Equational Logic of Iterative Processes. [EATCS]{} Monographs on Theoretical Computer Science, Springer (1993), <https://doi.org/10.1007/978-3-642-78034-9>

Bonsangue, M., Milius, S., A., S.: Sound and complete axiomatizations of coalgebraic language equivalence. CoRR abs/1104.2803 (2011)

Doberkat, E.E.: Eilenberg-[M]{}oore algebras for stochastic relations. Inform. and Comput. 204(12), 1756–1781 (2006), <http://dx.doi.org/10.1016/j.ic.2006.09.001>

Doberkat, E.E.: Erratum and addendum: [E]{}ilenberg-[M]{}oore algebras for stochastic relations \[mr2277336\]. Inform. and Comput. 206(12), 1476–1484 (2008), <http://dx.doi.org/10.1016/j.ic.2008.08.002>

sik, Z., Kuich, W.: [A Generation of Kozen’s Axiomatization of the Equational Theory of the Regular Sets]{}. In: Words, Semigroups, and Transductions - Festschrift in Honor of Gabriel Thierrin. pp. 99–114 (2001)

sik, Z., Maletti, A.: Simulation vs. equivalence. In: Proceedings of the 2010 International Conference on Foundations of Computer Science, [FCS]{} 2010, July 12-15, 2010, Las Vegas, Nevada, [USA]{}. pp. 119–124 (2010)

Hilbert, D.: [Ü]{}ber die [T]{}heorie der algebraischen [F]{}ormen. Math. Ann. 36(4), 473–534 (1890), <http://dx.doi.org/10.1007/BF01208503>

Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation, Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press (2016), <https://doi.org/10.1017/CBO9781316823187>

Jacobs, B., Silva, A., Sokolova, A.: Trace semantics via determinization. J. Comput. Syst. Sci. 81(5), 859–879 (2015)

Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS 62, 222–259 (1996)

Kakutani, S.: A generalization of [B]{}rouwer’s fixed point theorem. Duke Math. J. 8, 457–459 (1941), <http://projecteuclid.org/euclid.dmj/1077492791>

Kurz, A.: Logics for Coalgebras and Applications to Computer Science. Ph.D. thesis, Ludwig-Maximilians-Universit[ä]{}t M[ü]{}nchen (2000)

Mac Lane, S.: Categories for the working mathematician, Graduate Texts in Mathematics, vol. 5. Springer-Verlag, New York, second edn. (1998)

Manes, E., Mulry, P.: Monad compositions. [I]{}. [G]{}eneral constructions and recursive distributive laws. Theory Appl. Categ. 18, No. 7, 172–208 (2007)

Milius, S.: Proper functors and their rational fixed point. In: 7th Conference on Algebra and Coalgebra in Computer Science, [CALCO]{} 2017, June 12-16, 2017, Ljubljana, Slovenia. pp. 18:1–18:16 (2017), <https://doi.org/10.4230/LIPIcs.CALCO.2017.18>

Minkowski, H.: [Geometrie der Zahlen. In 2 Lieferungen. Lfg. 1.]{} [Leipzig: B. G. Teubner. 240 S. $8^\circ.$]{} (1896)

Pumplün, D.: Regularly ordered [B]{}anach spaces and positively convex spaces. Results Math. 7(1), 85–112 (1984), <http://dx.doi.org/10.1007/BF03322493>

Rockafellar, R.T.: Convex analysis. Princeton Mathematical Series, No. 28, Princeton University Press, Princeton, N.J. (1970)

Rudin, W.: Functional analysis. International Series in Pure and Applied Mathematics, McGraw-Hill Inc., New York, second edition edn. (1991)

Rutten, J.: Universal coalgebra: A theory of systems. Theoretical Computer Science 249, 3–80 (2000)

Silva, A.: [K]{}leene coalgebra. Ph.D. thesis, Radboud University Nijmegen (2010)

Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing the powerset construction, coalgebraically. In: Proc. FSTTCS 2010. Leibniz International Proceedings in Informatics (LIPIcs), vol. 8, pp. 272–283 (2010)

Silva, A., Sokolova, A.: Sound and complete axiomatization of trace semantics for probabilistic systems. Electr. Notes Theor. Comput. Sci. 276, 291–311 (2011), <https://doi.org/10.1016/j.entcs.2011.09.027>

Staton, S.: Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science 7(1) (2011)

Wolter, U.: On corelations, cokernels, and coequations. Electronic Notes in Theoretical Computer Science 33 (2000)

Category theory basics {#sec:app-basics}
======================

We start by recalling the basic notions of category, functor and natural transformation, so that all of the results in the paper are accessible also to non-experts.

A category ${\text{\tt{C}}}$ is a collection of objects and a collection of arrows (or morphisms) from one object to another. For every object $X \in {\text{\tt{C}}}$, there is an identity arrow $\operatorname{id}_X\colon X \to X$. For any three objects $X, Y, Z \in {\text{\tt{C}}}$, given two arrows $f\colon X \to Y$ and $g\colon Y\to Z$, there exists an arrow $g {\mathrel{\circ}}f\colon X \to Z$. Arrow composition is associative and $\operatorname{id}_X$ is neutral w.r.t. composition. The standard example is ${{\text{\tt{Set}}}}$, the category of sets and functions.

A functor $F$ from a category ${\text{\tt{C}}}$ to a category ${\text{\tt{D}}}$, notation $F\colon {\text{\tt{C}}} \to {\text{\tt{D}}}$, assigns to every object $X\in {\text{\tt{C}}}$, an object $FX \in {\text{\tt{D}}}$, and to every arrow $f\colon X \to Y$ in ${\text{\tt{C}}}$ an arrow $Ff\colon FX \to FY$ in ${\text{\tt{D}}}$ such that identity arrows and composition are preserved.

A concrete category is a category ${\text{\tt{C}}}$ equipped with a faithful functor $\mathcal U\colon {\text{\tt{C}}} \to {{\text{\tt{Set}}}}$. Intuitively, a concrete category has objects that are sets with some additional structure, e.g. algebras, and morphisms that are particular kind of functions, and $\mathcal U$ is a canonical forgetful functor. All categories that we consider are algebraic and hence concrete.

[r]{}[.1]{} @R-.5pc[ FX\^-[\_X]{}\^-[Ff]{} & FY\^-[\_Y]{}\
GX\^-[Gf]{} & GY ]{}

Let $F\colon {\text{\tt{C}}} \to {\text{\tt{D}}}$ and $G\colon {\text{\tt{C}}} \to {\text{\tt{D}}}$ be two functors. A natural transformation $\sigma\colon F \Rightarrow G$ is a family of arrows $\sigma_X\colon FX \to GX$ in ${\text{\tt{D}}}$ such that the diagram on the right commutes for all arrows $f\colon X \to Y$.

Monads and Algebras {#sec-app:monads}
-------------------

A monad is a functor $T\colon{\text{\tt{C}}} \rightarrow {\text{\tt{C}}}$ together with two natural transformations: a unit $\eta\colon \operatorname{id}_{{\text{\tt{C}}}}
\Rightarrow T$ and multiplication $\mu \colon T^{2} \Rightarrow
T$. These are required to make the following diagrams commute, for $X\in{\text{\tt{C}}}$. $$\xymatrix@C-.5pc@R-.5pc{
T X\ar[rr]^-{\eta_{T X}}\ar@{=}[drr] & & T^{2}X\ar[d]^{\mu_X} & &
   T X\ar[ll]_{T\eta_{X}}\ar@{=}[dll] 
&  & T^{3}X\ar[rr]^-{\mu_{T X}}\ar[d]_{T\mu_{X}} 
   & & T^{2}X\ar[d]^{\mu_X} \\
& & T X & &
& &
T^{2}X\ar[rr]_{\mu_X} & & T X
}$$ Given two monads $S,T$ with units and multiplications $\eta^S,\eta^T$ and $\mu^S,\mu^T$, respectively, and a natural transformation $\iota\colon S\Rightarrow T$, we say that $\iota$ is a monad morphism, and $S\leq T$ along $\iota$, if $\eta^T=\iota\circ\eta^S$ and $\iota\circ\mu^S=\mu^T\circ\iota\iota$ where $\iota\iota \stackrel{\text{def}}{=}T\iota{\mathrel{\circ}}\iota \stackrel{\text{nat.}}{=} \iota {\mathrel{\circ}}S\iota$.

We briefly describe some examples of monads on ${{\text{\tt{Set}}}}$.

-   The finitely supported subprobability distribution monad ${\mathcal{D}}$ is defined, for a set $X$ and a function $f\colon X \to Y$, as $${\mathcal{D}}X
    \,\,\, = \,\,\,
    \{\varphi\colon X \to [0,1] \mid \sum_{x \in X} \varphi(x) \le 1,\, \operatorname{supp}(\varphi) \text{~is~finite}\}$$ and $${\mathcal{D}}f(\varphi)(y)
    \,\,\, = \,\,\,
    \sum\limits_{x\in f^{-1}(\{y\})} \varphi(x).$$ Here and below $\operatorname{supp}(\varphi) = \{x \in X \mid \varphi(x) \neq 0\}$. The unit of ${\mathcal{D}}$ is given by a Dirac distribution $\eta_X(x) = \delta_x = ( x \mapsto 1)$ for $x \in X$ and the multiplication by $\mu_X(\Phi)(x) = \sum\limits_{\varphi \in \operatorname{supp}(\Phi)}
    \Phi(\varphi)\cdot \varphi(x)$ for $\Phi \in {\mathcal{D}}{\mathcal{D}}X$.

-   For a semiring $\mathbb S$ the $\mathbb S$-valuations monad ${T_{\mathbb{S}}}$ is defined as ${T_{\mathbb{S}}}X = \{\varphi\colon X \to \mathbb S \mid \operatorname{supp}(\varphi) \text{ is finite}\}$ and on functions $f\colon X \to Y$ we have ${T_{\mathbb{S}}}f(\varphi)(y) = \sum_{x \in f^{-1}(\{y\})} \varphi(x)$. Its unit is given by $\eta_X(x) = ( x \mapsto 1)$ and multiplication by $\mu_X(\Phi)(x) = \sum_{\varphi \in \operatorname{supp}\Phi} \Phi(\varphi) \cdot \varphi(x)$ for $\Phi \in {T_{\mathbb{S}}}{T_{\mathbb{S}}}X$.

-   To illustrate the connection between ${\mathcal{D}}$ and ${T_{\mathbb{S}}}$, consider yet another monad: For a semiring $\mathbb S$, and a (suitable) subset $S \subseteq \mathbb S$, the ($\mathbb S, S$)-valuations monad $T_{\mathbb S, S}$ is defined as follows. On objects it acts like $$T_{\mathbb S,S}X = \{\varphi\colon X \to \mathbb S \mid \operatorname{supp}(\varphi) \text{ is finite and } 
        \sum_{x \in X} \varphi(x) \in S\}$$ on functions it acts like ${T_{\mathbb{S}}}$. The unit and multiplication are defined as in ${T_{\mathbb{S}}}$. Note that ${\mathcal{D}}= T_{\mathbb R_+,[0,1]}$.

With a monad $T$ on a category ${\text{\tt{C}}}$ one associates the Eilenberg-Moore category ${\text{\tt{C}}}^{T}$ of Eilenberg-Moore algebras. Objects of ${\text{\tt{C}}}^{T}$ are pairs ${\mathbb{A}} = (A, \alpha)$ of an object $A \in {\text{\tt{C}}}$ and an arrow $\alpha\colon T A \rightarrow A$, making the first two diagrams below commute. $$\xymatrix@R-.5pc{
A\ar@{=}[dr]\ar[r]^-{\eta_A} & T A\ar[d]^{\alpha}
& 
T^{2}A\ar[d]_{\mu_A}\ar[r]^-{T\alpha} & T A\ar[d]^{\alpha}
& &
T A\ar[d]_{\alpha}\ar[r]^-{T h} & T B\ar[d]^{\beta} \\
& A 
&
T A\ar[r]_-{\alpha} & A
& &
A\ar[r]_-{h} & B
}$$

A homomorphism from an algebra ${\mathbb{A}} = (A, \alpha)$ to an algebra ${\mathbb{B}} = (B, b)$ is a map $h\colon
A\rightarrow B$ in ${\text{\tt{C}}}$ between the underlying objects making the diagram above on the right commute.

From now on fix ${\text{\tt{C}}}={{\text{\tt{Set}}}}$. A free Eilenberg-Moore algebra for a monad $T$ generated by $X$ is $(TX, \mu_X)$ and we will often denote it simply by $TX$. A free finitely generated Eilenberg-Moore algebra for $T$ is an algebra $TX$ with $X$ a finite set. The diagram in the middle thus says that the map $\alpha$ is a homomorphism from $T A$ to ${\mathbb{A}}$.

Indeed, $(TX,\mu_X)$ is free on $X$ as for every $T$-algebra ${\mathbb{A}} = (A, \alpha)$ and any ${{\text{\tt{Set}}}}$-morphism $f\colon X \to A$ there is a unique ${{\text{\tt{Set}}}^{T}}$-morphism $f^\#\colon (TX,\mu_X) \to \mathbb A$ such that $f^\# {\mathrel{\circ}}\eta_A = f$ — it is easy to see that this unique extension $f^\#$ is the Kleisli extension of $f$, i.e., $f^\# = \alpha {\mathrel{\circ}}Tf$. Moreover, note that $(f^\# {\mathrel{\circ}}\eta_A)^\# = f^\#$, by the uniqueness of the extension.

Proof details for properness of cubic functors {#app:B}
==============================================

Since $\operatorname{tr}_{c_1} x_1=\operatorname{tr}_{c_2} x_2$, we have $${{c_1}_{\text{\rm o}}}({{c_1}_{w}}(x_1))=[\operatorname{tr}_{c_1} x_1](w)=[\operatorname{tr}_{c_2} x_2](w)={{c_2}_{\text{\rm o}}}({{c_2}_{w}}(x_2)),\quad w\in A^*,$$ and therefore $d_1|_Z=d_2|_Z$. Moreover, $${{c_j}_{a}}({{c_j}_{w}}(x_j))={{c_j}_{wa}}(x_j),\quad w\in A^*,$$ and therefore $d_j(Z)\subseteq\mathbb S\times Z^A$.

Remembering Remark \[ProperSemiring\], we have to show that the functor ${{\ensuremath{F_{\,{\mathbb S}}}}}$ is proper. We have the zig-zag , and the $\mathbb S$-semimodule $Z$ is, as a subsemimodule of the finitely generated $\mathbb S$-semimodule $\mathbb S^{n_1}\times\mathbb S^{n_2}$, itself finitely generated.

Proof of the extension lemma
----------------------------

The proof of the extension lemma follows directly from the following two abstract properties.

\[lem:ext-lem-1\] Assume ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$ via $\iota\colon {T_{\mathbb{S}}}\Rightarrow {T_{\mathbb{E}}}$ and let $X$ be a finite set. Let ${\mathbb{Y}} \in {{\text{\tt{Set}}}^{{T_{\mathbb{S}}}}}$ and ${\mathbb{Z}} \in {{\text{\tt{Set}}}^{{T_{\mathbb{E}}}}}$ and assume we are given an arrow $a_Y\colon {T_{\mathbb{S}}}X \to {\mathbb{Y}}$ in ${{\text{\tt{Set}}}^{{T_{\mathbb{S}}}}}$ and a ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphism $h\colon {\mathbb{Y}} \to {\mathbb{Z}}$. Then there exists an arrow $a_Z\colon {T_{\mathbb{E}}}X \to {\mathbb{Z}}$ in ${{\text{\tt{Set}}}^{{T_{\mathbb{E}}}}}$ making the following diagram commute. $$\xymatrix@R=0.7em{
    {T_{\mathbb{S}}}X \ar[rr]^{\iota} \ar[d]_{a_Y}&& {T_{\mathbb{E}}}X \ar[d]^{a_Z}\\
    {\mathbb{Y}} \ar[rr]^{h}&& {\mathbb{Z}}
    }$$

Consider the map $h {\mathrel{\circ}}a_Y {\mathrel{\circ}}\eta_{\mathbb S,X}\colon X \to Z$. Let $a_Z =(h {\mathrel{\circ}}a_Y {\mathrel{\circ}}\eta_{\mathbb S,X})^{\#_{\mathbb{E}}}$.

All morphisms in the square are ${{\text{\tt{Set}}}^{{T_{\mathbb{S}}}}}$-morphisms: $\alpha_Y$ by definition; $\iota_x$ as one of the monad morphism laws shows this; $h$ as it is a ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$-homomorphism; and $\alpha_Z = M_\iota(\alpha_Z)$. Clearly, then $h {\mathrel{\circ}}\alpha_Y$ and $\alpha_Z {\mathrel{\circ}}\iota_X$ are ${{\text{\tt{Set}}}^{{T_{\mathbb{S}}}}}$-morphisms from the free algebra $({T_{\mathbb{S}}}X, \mu_X)$ to ${\mathbb{Z}}$.

Therefore, for the commutativity of the square it suffices to show that $$h {\mathrel{\circ}}\alpha_Y {\mathrel{\circ}}\eta_{\mathbb S} = \alpha_Z {\mathrel{\circ}}\iota_X {\mathrel{\circ}}\eta_{\mathbb S}$$ as then, by the uniqueness of the extension, $$h {\mathrel{\circ}}\alpha_Y = (h{\mathrel{\circ}}\alpha_Y {\mathrel{\circ}}\eta_{\mathbb S})^{\#_{\mathbb{S}}} = 
(\alpha_Z {\mathrel{\circ}}\iota_X {\mathrel{\circ}}\eta_{\mathbb S})^{\#_{\mathbb{S}}} = \alpha_Z {\mathrel{\circ}}\iota_X.$$

The last needed equality follows because ${T_{\mathbb{S}}}\le {T_{\mathbb{E}}}$ along $\iota$ and so $$(h {\mathrel{\circ}}a_Y {\mathrel{\circ}}\eta_{\mathbb S,X})^{\#_{\mathbb{E}}} {\mathrel{\circ}}\iota_X {\mathrel{\circ}}\eta_{\mathbb{S},X} = (h {\mathrel{\circ}}a_Y {\mathrel{\circ}}\eta_{\mathbb S,X})^{\#_{\mathbb{E}}} {\mathrel{\circ}}\eta_{\mathbb E,X} = h {\mathrel{\circ}}a_Y {\mathrel{\circ}}\eta_{\mathbb S,X}. \vspace*{-7mm}$$

\[lem:ext-lem-2\] The map $\iota \times \iota^A$ is a ${T_{\mathbb{S}}}\le{T_{\mathbb{E}}}$-homomorphism from ${{\ensuremath{F_{\,{\mathbb{S}}}}}}({T_{\mathbb{S}}}X)$ to ${{\ensuremath{F_{\,{\mathbb{E}}}}}}({T_{\mathbb{E}}}X)$.

Since the functor $M_\iota$ induced by the monad morphism $\iota$ satisfies $\mathcal U_\mathbb{S} {\mathrel{\circ}}M_\iota = \mathcal U_\mathbb{E}$, it preserves all limits (as $\mathcal U_\mathbb{E}$ preserves them and $\mathcal U_\mathbb{S}$ reflects them). Hence, in particular, it preserves products. Since $\iota_X\colon ({T_{\mathbb{S}}}X, \mu_{\mathbb S,X}) \to M_\iota({T_{\mathbb{E}}}X, \mu_{\mathbb E,X})$ is a ${T_{\mathbb{S}}}$-algebra homomorphism by one of the monad morphism laws, we have $$\iota_1 \times \iota_X^A \colon {T_{\mathbb{S}}}1 \times {T_{\mathbb{S}}}X^A \to M_\iota({T_{\mathbb{E}}}1) \times M_\iota({T_{\mathbb{E}}}X)^A = M_\iota({T_{\mathbb{E}}}1 \times {T_{\mathbb{E}}}X^A)$$ is one as well.

Since $\mathbb S\subseteq\mathbb E$, we have $${{\ensuremath{F_{\,{\mathbb E}}}}}X\cap{{\ensuremath{F_{\,{\mathbb S}}}}}Y=(\mathbb E\times X^A)\cap(\mathbb S\times Y^A)
        =\mathbb S\times(X\cap Y)^A={{\ensuremath{F_{\,{\mathbb S}}}}}(X\cap Y)
        .$$ Assume now that $Y_j\subseteq X_j$. We have $$({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_1)^{-1}({{\ensuremath{F_{\,{\mathbb S}}}}}Y_1)=
        \{(o,(({x_1}_a,{x_2}_a))_{a\in A})\in\mathbb E\times(X_1\times X_2)^A\mid o\in\mathbb S,{x_1}_a\in Y_1\}
        ,$$ and the analogous formula for $({{\ensuremath{F_{\,{\mathbb E}}}}}\pi_2)^{-1}({{\ensuremath{F_{\,{\mathbb S}}}}}Y_2)$. This shows that the intersection of these two inverse images is equal to $\mathbb S\times(Y_1\times Y_2)^A$.

Proof of the reduction lemma
----------------------------

 Reducing from  to  {#reducing-from-to .unnumbered}
-------------------

The reduction lemma for passing from abelian groups to commutative monoids arises from a classical result of algebra. Namely, it is a corollary of the following theorem due to D.Hilbert, cf. [@hilbert:1890 Theorem II] see also [@bachem:1978 Theorem 1.1].

\[PolyhedralZ\] Let $W$ be a $n\times m$-matrix with integer entries, and let $X$ be the commutative monoid $$X=\big\{x\in\mathbb Z^n\mid x\cdot W\geq 0\big\}
        ,$$ where the monoid operation is the usual addition on $\mathbb Z^n$. Then $X$ is finitely generated as a commutative monoid.

The reduction lemma for passing from  to  is a corollary Since every finitely generated abelian group is also finitely generated as a commutative monoid, we obtain a somewhat stronger variant.

\[RedLemN\] Let $Z$ be a finitely generated abelian group, let $m\in\mathbb N$, and let $\varphi\colon Z\to\mathbb Z^m$ be a group homomorphism. Then $\varphi^{-1}(\mathbb N^m)$ is finitely generated as a commutative monoid.

Write $Z$, up to an isomorphism, as a direct sum of cyclic abelian groups $$\label{3}
        Z=\mathbb Z^k\oplus\Big[\bigoplus_{j=1}^n\mathbb Z/a_j\mathbb Z\Big]$$ with $a_j\geq 2$. Since $\varphi$ maps into the torsionfree group $\mathbb Z^m$, we must have $$\varphi\Big(\bigoplus_{j=1}^n\mathbb Z/a_j\mathbb Z\Big)=\{0\}
        .$$ Hence, an element $x\in Z$ satisfies $\varphi(x)\geq 0$, if and only if $\varphi(x_0)\geq 0$ where $x=x_0+x_1$ is the decomposition of $x$ according to the direct sum . The action of the map $\psi=\varphi|_{\mathbb Z^k}\colon \mathbb Z^k\to\mathbb Z^m$ is described as multiplication of $x_0=(\xi_1,\ldots,\xi_k)$ with some $k\times m$-matrix $W$ having integer coefficients. Thus $$\psi^{-1}(\mathbb N^m)=\big\{x_0\in\mathbb Z^k\mid x_0\cdot W\geq 0\big\}
        ,$$ and by Hilbert’s Theorem $\psi^{-1}(\mathbb N^m)$ is finitely generated as a commutative monoid.

The set $\bigoplus_{j=1}^n\mathbb Z/a_j\mathbb Z$ also has a finite set of generators as a monoid, for example the residue classes $1/a_j\mathbb Z$, $j=1,\ldots,n$. Together we see that $\varphi^{-1}(\mathbb N^m)$ has a finite set of generators as a commutative monoid.

 Reducing from Q to  {#reducing-from-qto .unnumbered}
--------------------

The reduction lemma for passing from vector spaces over $\mathbb Q$ to $\mathbb Q_+$-semimodules is a corollary of the one passing from  to . Thus we have the corresponding stronger variant also in this case.

\[RedLemQ+\] Let $Z$ be a finite dimensional $\mathbb Q$-vector space, let $m\in\mathbb N$, and let $\varphi\colon Z\to\mathbb Q^m$ be $\mathbb Q$-linear. Then $\varphi^{-1}(\mathbb Q_+^m)$ is finitely generated as a $\mathbb Q_+$-semimodule.

Let $\{u_1,\ldots,u_k\}$ be a set of generators of $Z$ as a $\mathbb Q$-vector space. Write $$\varphi(u_j)=\Big(\frac{a_{j,1}}{b_{j,1}},\ldots,\frac{a_{j,m}}{b_{j,m}}\Big),\quad 
        j=1,\ldots,k
        ,$$ with $a_{j,i}\in\mathbb Z$ and $b_{j,i}\in\mathbb N\setminus\{0\}$. Set $b=\prod_{j=1}^k\prod_{i=1}^mb_{j,i}$, then $\varphi(bu_j)\in\mathbb Z^m$, $j=1,\ldots,k$.

Let $Z'\subseteq Z$ be the $\mathbb Z$-submodule generated by $\{bu_1,\ldots,bu_k\}$, and set $\psi=\varphi|_{Z'}$. Then $\psi$ is a $\mathbb Z$-linear map of $Z'$ into $\mathbb Z^m$. By Lemma \[RedLemN\], $\psi^{-1}(\mathbb N^m)$ is finitely generated as $\mathbb N$-semimodule, say by $\{v_1,\ldots,v_l\}\subseteq Z'$.

Given $x\in\varphi^{-1}(\mathbb Q_+^m)$, choose $\nu_1,\ldots,\nu_k\in\mathbb Q$ with $x=\sum_{j=1}^k\nu_ju_j$. Write $\nu_j=\frac{\alpha_j}{\beta_j}$ with $\alpha_j\in\mathbb Z$ and $\beta_j\in\mathbb N\setminus\{0\}$, and set $\beta=\prod_{j=1}^k\beta_j$. Then $$\beta b\cdot x=\sum_{j=1}^k(\beta\nu_j)\cdot bu_j\in Z'
        ,$$ and $$\psi(\beta b\cdot x)=\varphi(\beta b\cdot x)=\beta b\cdot\varphi(x)\in\mathbb Q_+^m\cap\mathbb Z^m=\mathbb N^m
        .$$ Thus $\beta b\cdot x$ is an $\mathbb N$-linear combination of the elements $v_1,\ldots,v_l$, and hence $x$ is a $\mathbb Q_+$-linear combination of these elements. This shows that $\varphi^{-1}(\mathbb Q_+^m)$ is generated by $\{v_1,\ldots,v_l\}$ as a $\mathbb Q_+$-semimodule.

 Reducing from R to  {#reducing-from-rto .unnumbered}
--------------------

The reduction lemma for passing from vector spaces over $\mathbb R$ to convex cones arises from a different source than the previously studied. Namely, it is a corollary of the below classical theorem of H.Minkowski, cf. [@minkowski:1896] see also [@rockafellar:1970 Theorem 19.1].

Recall that a convex subset $X$ of $\mathbb R^n$ is called *polyhedral*, if it is a finite intersection of half-spaces, i.e., if there exist $l\in\mathbb N$, $u_1,\ldots,u_l\in\mathbb R^n$, and $\nu_1,\ldots,\nu_l\in\mathbb R$, such that $$X=\big\{x\in\mathbb R^n\mid (x,u_j)\leq\nu_j,j=1,\ldots,l\big\}
    ,$$ where $(\cdot,\cdot)$ denotes the euclidean scalar product on $\mathbb R^n$. On the other hand, $X$ is said to be *generated by points $a_1,\ldots,a_{l_1}$ and directions $b_1,\ldots,b_{l_2}$*, if $$X=\Big\{\sum_{j=1}^{l_1}\alpha_ja_j+\sum_{j=1}^{l_2}\beta_jb_j\mid 
    \alpha_j\in[0,1],\sum_{j=1}^{l_1}\alpha_j=1,\ \beta_j\geq 0,j=1,\ldots,l_2\Big\}
    .$$ Note that a convex set generated by some points and directions is bounded, if and only if no (nonzero) directions are present. Further, a convex set is a cone, if and only if it allows a representation where only directions occur.

\[PolyhedralR\] Let $X$ be a convex subset of $\mathbb R^n$. Then $X$ is polyhedral, if and only if $X$ is generated by a finite set of points and directions.

The relevance of Minkowski’s Theorem in the present context is that it shows that the intersection of two finitely generated sets is finitely generated (since the intersection of two polyhedral sets is obviously polyhedral).

The reduction lemma for passing from R to  is an immediate corollary. Since every finite dimensional $\mathbb R$-vector space is also finitely generated as a convex cone, we have the corresponding stronger version.

\[RedLemR+\] Let $Z$ be a finite dimensional $\mathbb R$-vector space, let $m\in\mathbb N$, and let $\varphi\colon Z\to\mathbb R^m$ be $\mathbb R$-linear. Then $\varphi^{-1}(\mathbb R_+^m)$ is finitely generated as a convex cone.

*Step 1:*  The image $\varphi(Z)$ is a linear subspace of $\mathbb R^m$, in particular, polyhedral. The positive cone $\mathbb R_+^m$ is obviously also polyhedral. We conclude that the convex cone $\varphi(Z)\cap\mathbb R_+^m$ is generated by some finite set of directions.

*Step 2:*  The kernel $\varphi^{-1}(\{0\})$ is, as a linear subspace of the finite dimensional vector space $Z$, itself finite dimensional (generated, say, by $\{u_1,\ldots,u_k\}$). Thus it is also finitely generated as a convex cone (in fact, $\{\pm u_1,\ldots,\pm u_k\}$ is a set of generators).

Choose a finite set of directions $\{a_1,\ldots,a_l\}$ generating $\varphi(Z)\cap\mathbb R_+^m$ as a convex cone, and choose $v_j\in Z$ with $\varphi(v_j)=a_j$, $j=1,\ldots,l$. We claim that $\{\pm u_1,\ldots,\pm u_k\}\cup\{v_1,\ldots,v_l\}$ generates $\varphi^{-1}(\mathbb R_+^m)$ as a convex cone. To see this, let $x\in \varphi^{-1}(\mathbb R_+^m)$. Choose $\alpha_1,\ldots,\alpha_l\geq 0$ with $\varphi(x)=\alpha_1a_1+\ldots+\alpha_la_l$. Then $$\varphi\big(x-(\alpha_1v_1+\ldots+\alpha_lv_l)\big)=
            \varphi(x)-\big(\alpha_1\varphi(v_1)+\ldots+\alpha_l\varphi(v_l)\big)=0
            ,$$ and hence we find $\beta_1^\pm,\ldots,\beta_k^\pm\geq 0$ with $$x-(\alpha_1v_1+\ldots+\alpha_lv_l)=(\beta_1^+u_1+\ldots+\beta_k^+u_k)+(\beta_1^-(-u_1)+\ldots+\beta_k^-(-u_k))
            .$$

 Reducing from  to  {#reducing-from-to-1 .unnumbered}
-------------------

The reduction lemma for passing from vector spaces over $\mathbb R$ to positively convex algebras is again a corollary of Theorem \[PolyhedralR\]. However, in a sense the situation is more complicated. One, the corresponding strong version fails; in fact, no (nonzero) $\mathbb R$-vector space is finitely generated as a . Two, unlike in categories of semimodules, the direct product $T_{[0,1]}B_1\times T_{[0,1]}B_2$ does not coincide with $T_{[0,1]}(B_1\dot\cup B_2)$.

\[RedLemPca\] Let $n_1,n_2\in\mathbb N$, and let $Z$ be a linear subspace of $\mathbb R^{n_1}\times\mathbb R^{n_2}$. Then $Z\cap(\Delta^{n_1}\times\Delta^{n_2})$ is finitely generated as a positively convex algebra.

Obviously, $Z$ and $\Delta^{n_1}\times\Delta^{n_2}$ are both polyhedral. We conclude that $Z\cap(\Delta^{n_1}\times\Delta^{n_2})$ is generated by a finite set of points and directions. Since it is bounded, no direction can occur, and it is thus finitely generated as a .

Self-contained proof of Lemma \[RedLemN\]
=========================================

We provide a short and self-contained proof of the named reduction lemma. It proceeds via an argument very specific for $\mathbb N$; the essential ingredient is that the order of $\mathbb N$ is total and satisfies the descending chain condition. Note that the following argument also proves Hilbert’s Theorem.

First, a common fact about the product order on $\mathbb N^m$ (we provide an explicit proof since we cannot appoint a reference).

\[Incomparable\] Let $m\in\mathbb N$, and let $M\subseteq\mathbb N^m$ be a set of pairwise incomparable elements. Then $M$ is finite.

Assume that $M$ is infinite, and choose a sequence $(a_n)_{n\in\mathbb N}$ of different elements of $M$. Write $a_n=(\alpha_{n,1},\ldots,\alpha_{n,m})$. We construct, in $m$ steps, a subsequence $(b_n)_{n\in\mathbb N}$ of $(a_n)_{n\in\mathbb N}$ with the property that (we write $b_n=(\beta_{n,1},\ldots,\beta_{n,m})$) $$\label{5}
        \forall k\in\{1,\ldots,m\}{{.\kern3pt}}L_k=\sup_{n\in\mathbb N}\beta_{n,k}<\infty
        \ \vee\ 
        \beta_{0,k}<\beta_{1,k}<\beta_{2,k}<\cdots$$ In the first step, extract a subsequence of $(a_n)_{n\in\mathbb N}$ according to the behaviour of the sequence of first components $(\alpha_{n,1})_{n\in\mathbb N}$. If $\sup_{n\in\mathbb N}\alpha_{n,1}<\infty$, take the whole sequence $(a_n)_{n\in\mathbb N}$ as the subsequence. If $\sup_{n\in\mathbb N}\alpha_{n,1}=\infty$, take a subsequence $(a_{n_j})_{j\in\mathbb N}$ with $$\alpha_{n_0,1}<\alpha_{n_1,1}<\alpha_{n_2,1}<\cdots
        .$$ Repeating this step, always starting from the currently chosen subsequence, we succesively extract subsequences which after $l$ steps satisfy the property for the components up to $l$.

Denote $$I_1=\big\{k\in\{1,\ldots,m\}\mid \sup_{n\in\mathbb N}\beta_{n,k}<\infty\big\}
        ,\quad 
        I_2=\big\{k\in\{1,\ldots,m\}\mid \sup_{n\in\mathbb N}\beta_{n,k}=\infty\big\}$$ The map $n\mapsto(\beta_{n,k})_{k\in I_1}$ maps $\mathbb N$ into the finite set $\prod_{k\in I_1}\{0,\ldots,L_k\}$, and hence is not injective. Choose $n_1<n_2$ with $\beta_{n_1,k}=\beta_{n_2,k}$, $k\in I_1$. Since $\beta_{n_1,k}<\beta_{n_2,k}$, $k\in I_2$, we obtain $b_{n_1}\leq b_{n_2}$. However, by our choice of the elements $a_n$, $b_{n_1}\neq b_{n_2}$. Thus $M$ contains a pair of different but comparable elements.

If $\varphi^{-1}(\mathbb N^m)=\{0\}$, there is nothing to prove. Hence, assume that $\varphi^{-1}(\mathbb N^m)\neq\{0\}$.

*Step 1:*  We settle the case that $Z\subseteq\mathbb Z^m$ and $\varphi$ is the inclusion map. Let $M$ be the set of minimal elements of $(Z\cap\mathbb N^m)\setminus\{0\}$. From the descending chain condition we obtain $$\forall x\in(Z\cap\mathbb N^m)\setminus\{0\}{{.\kern3pt}}\exists\,y\in M{{.\kern3pt}}y\leq x$$ By Lemma \[Incomparable\], $M$ is finite, say $M=\{a_1,\ldots,a_l\}$. Now we show that $M$ generates $Z$ as commutative monoid. Let $x\in Z$, and assume that $x-\sum_{j=1}^l\alpha_ja_j\neq 0$ for all $\alpha_j\in\mathbb N$. By the descending chain condition, the set of all elements of this form contains a minimial element, say, $x-\sum_{j=1}^l\tilde\alpha_ja_j$. Choose $y\in M$ with $y\leq x-\sum_{j=1}^l\tilde\alpha_ja_j$. Since $y\neq 0$, we have $x-\sum_{j=1}^l\tilde\alpha_ja_j-y<x-\sum_{j=1}^l\tilde\alpha_ja_j$ and we reached a contradiction.

*Step 2:*  The kernel $\varphi^{-1}(\{0\})$ is, as a subgroup of the finitely generated abelian group $Z$, itself finitely generated (remember here that $\mathbb Z$ is a Noetherian ring). Let $\{u_1,\ldots,u_k\}$ be a set of generators of $\varphi^{-1}(\{0\})$ as abelian group. Then $\{\pm u_1,\ldots,\pm u_k\}$ is a set of generators of $\varphi^{-1}(\{0\})$ as a commutative monoid.

By Step 1 we find $\{a_1,\ldots,a_l\}\subseteq\mathbb Z^m$ generating $\varphi(Z)\cap\mathbb N^m$ as a commutative monoid. Choose $v_j\in Z$ with $\varphi(v_j)=a_j$, $j=1,\ldots,l$. Then we find, for each $x\in Z$, a linear combination of the $v_j$’s with nonnegative integer coefficients such that $$\varphi\Big(x-\sum_{j=1}^l\nu_jv_j\Big)=0
            .$$ Hence, $\{\pm u_1,\ldots,\pm u_k\}\cup\{v_1,\ldots,v_l\}$ generates $\varphi^{-1}(Z)$ as commutative monoid.

Properties of ${{\ensuremath{\widehat F}}}$ {#app:D}
===========================================

Here the inclusion “$\supseteq$” is obvious. For the reverse inclusion, let $(o,\phi)\in{{\ensuremath{\widehat F}}}X$ and choose $p_{a,j}$ and $x_{a,j}$ according to Definition \[Ghat-def\]. Set $p_a=\sum_{j=1}^{n_a}p_{a,j}$. If $p_a=0$, set $x_a=0$. If $p_a>0$, set $x_a=\sum_{j=1}^n\frac{p_{a,j}}{p_a}x_{a,j}$. Then $x_a\in X$ and $f(a)=\sum_{j=1}^{n_a}p_{a,j}x_{a,j}=p_ax_a$.

\[GhSurj\] The functor ${{\ensuremath{\widehat F}}}$ preserves surjective algebra homomorphisms.

Let $X,Y$ be s, and $f:X\to Y$ a surjective algebra homomorphism. Let $(o,g)\in{{\ensuremath{\widehat F}}}Y$ be given. By Lemma \[Ghat-simple\] we can choose $p_a\in[0,1]$ and $y_a\in Y$ such that $o+\sum_{a\in A}p_a\leq 1$ and $g(a)=p_ay_a$, $a\in A$. Since $f$ is surjective, we find $x_a\in X$ with $f(x_a)=y_a$. Let $h:A\to X$ be the function $h(a)=p_ax_a$. Again using Lemma \[Ghat-simple\], we see that $(o,h)\in{{\ensuremath{\widehat F}}}X$. By our choice of $x_a$, it holds that $({{\ensuremath{\widehat F}}}f)(o,h)=(o,g)$.

Let $(o,\phi)\in{{\ensuremath{\widehat F}}}X$, and choose $p_a\in[0,1]$ and $x_a\in X$ as in Lemma \[Ghat-simple\]. Then ${\ensuremath{\mu_{X}}}(\phi(a))=p_a{\ensuremath{\mu_{X}}}(x_a)\leq p_a$, and hence $o+\sum_{a\in A}{\ensuremath{\mu_{X}}}(\phi(a))\leq 1$. Further, $o\in[0,1]$, in particular $o\geq 0$.

Conversely, assume that $o\geq 0$ and $o+\sum_{a\in A}{\ensuremath{\mu_{X}}}(\phi(a))\leq 1$. Let $a\in A$. Set $p_a={\ensuremath{\mu_{X}}}(\phi(a))$, then $p_a\in[0,1]$ since $\sum_{a\in A}p_a\leq 1$. To define $x_a$ consider first the case that ${\ensuremath{\mu_{X}}}(\phi(a))=0$. In this case $\phi(a)=0$ since $X$ is bounded, and we set $x_a=0$. If ${\ensuremath{\mu_{X}}}(\phi(a))>0$, set $x_a=\frac 1{{\ensuremath{\mu_{X}}}(\phi(a))}\phi(a)$. Since $X$ is closed, we have $x_a\in X$. In both cases, we obtained a representation $\phi(a)=p_ax_a$ with $p_a\in[0,1]$ and $x_a\in X$. Clearly, $o+\sum_{a\in A}p_a\leq 1$, and we conclude that $(o,\phi)\in{{\ensuremath{\widehat F}}}X$.

We build the extension in three stages.

 We extend $c$ to the cone generated by $X$:  Set $C=\bigcup_{t>0}tX$, and define $c_1\colon C\to V_2$ by the following procedure. Given $x\in C$, choose $t>0$ with $x\in tX$, and set $c_1(x)=t\cdot c\big(\frac 1tx\big)$. By this procedure the map $c_1$ is indeed well-defined. To see this, assume $x\in tX\cap sX$ where w.l.o.g. $s\leq t$. Then $\frac 1tx=\frac st\cdot\frac 1sx$. Since $\frac st\leq 1$, it follows that $c(\frac 1tx)=\frac st c(\frac 1sx)$, and hence $t\cdot c(\frac 1tx)=s\cdot c(\frac 1sx)$. Let us check that $c_1$ is cone-morphism, i.e., that $$c_1(x+y)=c_1(x)+c_2(y),\ x,y\in C,\qquad c_1(px)=pc_1(x),\ x\in C,p\geq 0
            .$$ Given $x,y\in C$, choose $t>0$ such that $x,y,x+y\in tX$. Observe here that $C$ is a union of an increasing family of sets. Then $$\begin{aligned}
            c_1(x+y)= &\, 2t\cdot c\Big(\frac 1{2t}(x+y)\Big)
            =2t\cdot c\Big(\frac 12\cdot\frac 1tx+\frac 12\cdot\frac 1ty\Big)
            \\[2mm]
            = &\, 2t\cdot\Big[\frac 12c\big(\frac 1tx\big)+\frac 12c\big(\frac 1ty\big)\Big]
            \\[2mm]
            = &\, t\cdot c\Big(\frac 1tx\Big)+t\cdot c\Big(\frac 1ty\Big)
            =c_1(x)+c_2(y)
            .
        \end{aligned}$$ Given $x\in C$ and $p>0$, choose $t>0$ with $x\in tX$. Then $px\in(pt)X$, and we obtain $$c_1(px)=pt\cdot c\Big(\frac 1{pt}(px)\Big)=pt\cdot c\Big(\frac 1tx\Big)=pt\cdot\frac 1t c_1(x)
            =pc_1(x)
            .$$ For $p=0$, the required equality is trivial. Finally, observe that $c_1$ extends $c$, since for $x\in X$ we can choose $t=1$ in the definition of $c_1$.

 We extend $c_1$ to the linear subspace generated by $C$:  Since $C$ is a cone, we have $\operatorname{span}C=C-C$. We define $c_2\colon \operatorname{span}C\to V_2$ by the following procedure. Given $x\in\operatorname{span}C$, choose $a_+,a_-\in C$ with $x=a_+-a_-$, and $c_2(x)=c_1(a_+)-c_2(a_-)$. By this procedure the map $c_2$ is indeed well-defined. Assume $x=a_+-a_-=b_+-b_-$. Then $a_++b_-=b_++a_-$, and we obtain $$c_1(a_+)+c_1(b_-)=c_1(a_++b_-)=c_1(b_++a_-)=c_1(b_+)+c_1(a_-)
            ,$$ which yields $c_1(a_+)-c_1(a_-)=c_1(b_+)-c_1(b_-)$. Let us check that $c_2$ is linear. Given $x,y\in\operatorname{span}C$, choose representations $x=a_+-a_-$, $y=b_+-b_-$. Then $x+y=(a_++b_+)-(a_-+b_-)$, and we obtain $$\begin{aligned}
            c_2(x+y)= &\, c_1(a_++b_+)-c_1(a_-+b_-)
            =\big[c_1(a_+)+c_1(b_+)\big]-\big[c_1(a_-)+c_1(b_-)\big]
            \\
            = &\, \big[c_1(a_+)-c_1(a_-)\big]+\big[c_1(b_+)-c_1(b_-)\big]
            =c_2(x)+c_2(y)
            .
        \end{aligned}$$ Given $x\in\operatorname{span}C$ and $p\in\mathbb R$, choose a representation $x=a_+-a_-$ and distinguish cases according to the sign of $p$. If $p>0$, we have the representation $px=pa_+-pa_-$ and hence $$\begin{aligned}
            c_2(px)= &\, c_1(pa_+)-c_1(pa_-)=pc_1(a_+)-pc_1(a_-)
            \\
            = &\, p\big[c_1(a_+)-c_1(a_-)\big]=pc_2(x)
            .
        \end{aligned}$$ If $p<0$, we have the representation $px=(-p)a_--(-p)a_+$ and hence $$\begin{aligned}
            c_2(px)= &\, c_1((-p)a_-)-c_1((-p)a_+)=(-p)c_1(a_-)-(-p)c_1(a_+)
            \\
            = &\, p\big[c_1(a_+)-c_1(a_-)\big]=pc_2(x)
            .
        \end{aligned}$$ For $p=0$, the required equality is trivial. Finally, observe that $c_2$ extends $c_1$, since for $x\in C$ we can choose the representation $x=x-0$ in the definition of $c_2$.

 We extend $c_2$ to $V_1$:  By linear algebra a linear map given on a subspace can be extended to a linear map on the whole space.

The uniqueness statement is clear.

First assume that holds. Let $x\in X$. Then ${\ensuremath{\mu_{X}}}(x)\leq 1$, and we obtain $${{c}_{\text{\rm o}}}(x)+\sum_{a\in A}{\ensuremath{\mu_{Y}}}({{c}_{a}}(x))=
        {{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}{\ensuremath{\mu_{Y}}}({{\tilde c}_{a}}(x))\leq{\ensuremath{\mu_{X}}}(x)\leq 1
        .$$ Further, ${{c}_{\text{\rm o}}}(x)\geq 0$ by assumption. Now Lemma \[Ghat-Minko\] gives $c(x)\in{{\ensuremath{\widehat F}}}Y$.

Conversely, assume $c(X)\subseteq{{\ensuremath{\widehat F}}}Y$, and let $x\in\mathbb R^n$ be given. If ${\ensuremath{\mu_{X}}}(x)=\infty$, the relation trivially holds. If ${\ensuremath{\mu_{X}}}(x)=0$, then $x=0$ since $X$ is bounded. Hence, the left side of equals $0$, and again holds. Assume that ${\ensuremath{\mu_{X}}}(x)\in(0,\infty)$. Since $X$ is closed, we have ${\ensuremath{\mu_{X}}}(x)^{-1}x\in X$, and hence $c({\ensuremath{\mu_{X}}}(x)^{-1}x)\in{{\ensuremath{\widehat F}}}Y$. From Lemma \[Ghat-Minko\], we get the estimate $$\begin{aligned}
        {{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}{\ensuremath{\mu_{Y}}}({{\tilde c}_{a}}(x))= &\, {\ensuremath{\mu_{X}}}(x)
        \Big(
        {{\tilde c}_{\text{\rm o}}}\big(\frac 1{{\ensuremath{\mu_{X}}}(x)}x\big)+\sum_{a\in A}{\ensuremath{\mu_{Y}}}\big({{\tilde c}_{a}}(\frac 1{{\ensuremath{\mu_{X}}}(x)}x)\big)
        \Big)
        \\
        = &\, {\ensuremath{\mu_{X}}}(x)
        \Big(
        {{c}_{\text{\rm o}}}\big(\frac 1{{\ensuremath{\mu_{X}}}(x)}x\big)+\sum_{a\in A}{\ensuremath{\mu_{Y}}}\big({{c}_{a}}(\frac 1{{\ensuremath{\mu_{X}}}(x)}x)\big)
        \Big)
        \leq{\ensuremath{\mu_{X}}}(x)
        .
    \end{aligned}$$

Proof details of the Extension Theorem
======================================

Recall Kakutani’s theorem [@kakutani:1941 Corollary].

\[Kak\] Let $M\subseteq\mathbb R^n$ and $P\colon M\to\mathcal P(M)$. Assume

1.  $M$ is nonempty, compact, and convex,

2.  for each $x\in M$, the set $P(x)$ is nonempty, closed, and convex,

3.  the map $P$ has closed graph in the sense that, whenver $x_n\in M$, $x_n\to x$, and $y_n\in P(x_n)$, $y_n\to y$, it follows that $y\in P(x)$.

Then there exists $x\in M$ with $x\in P(x)$.

Note that $P$ having closed graph implies that $P(x)$ is closed for all $x$. To see this, let $y_n\in P(x)$, $y_n\to y$, and use the constant sequence $x_n=x$ in the closed graph property.

In the proof of Theorem \[ExEx\] we shall, as in Example \[Pyramid\], identify a pyramid $Y$ with the appropriately scaled normal vector $u$ of its inclined side. Then, for two pyramids $Y_1$ and $Y_2$ with corresponding normal vectors $u_1$ and $u_2$, the requirement that $X\subseteq Y_j$ becomes $(x,u_j)\leq{\ensuremath{\mu_{X}}}(x)$, $x\geq 0$, and the requirement $\tilde c(Y_2)\subseteq{{\ensuremath{\widehat F}}}Y_1$ becomes ${{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u_1)\leq(x,u_2)$, $x\geq 0$, cf. Corollary \[Ghat-Minko-Coalg\].

Let $M$ be the set $$M=\big\{u\in\mathbb R^n\mid u\geq 0\text{ and }(x,u)\leq{\ensuremath{\mu_{X}}}(x),x\geq 0\big\}
        .$$ We have to include vectors $u$ with possibly vanishing components into $M$ to ensure closedness. It will be a step in the proof to show that a fixed point must be strictly positive.

Let $P\colon M\to\mathcal P(M)$ be the map $$P(u)=\big\{v\in M\mid {{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u)\leq(x,v), x\geq 0\big\}
        .$$ Here we again denote by $\tilde c\colon \mathbb R^n\to\mathbb R\times(\mathbb R^n)^A$ the linear extension of $c$. Observe that $\tilde c(x)\geq 0$ for all $x\geq 0$, since $\Delta^n\subseteq X$ and $c(x)\geq 0$ for $x\in X$.

It is easy to check that $M$ and $P$ satisfy the hypothesis of Kakutani’s Theorem, the crucial point being that $P(u)\neq\emptyset$.

 $M$ is nonempty:  We have $0\in M$.

 $M$ is compact:  To show that $M$ is closed let $u_n\in M$ with $u_n\to u$. Since $u_n\geq 0$ also $u\geq 0$, and for each fixed $x\geq 0$ continuity of the scalar product yields $(x,u)=\lim_{n\to\infty}(x,u_n)\leq{\ensuremath{\mu_{X}}}(x)$. Further, $M$ is bounded since $(e_j,u)\leq{\ensuremath{\mu_{X}}}(e_j)\leq 1$, $j=1,\ldots,n$, by our assumption that $\Delta^n\subseteq X$, and hence $u\in[0,1]^n$.

 $M$ is convex:  Let $u_1,u_2\in M$ and $p\in[0,1]$. First, clearly, $pu_1+(1-p)u_2\geq 0$. Second, for each $x\geq 0$, $$\begin{aligned}
            (x,pu_1+(1-p)u_2)= &\, p(x,u_1)+(1-p)(x,u_2)
            \\
            \leq &\, p{\ensuremath{\mu_{X}}}(x)+(1-p){\ensuremath{\mu_{X}}}(x)={\ensuremath{\mu_{X}}}(x)
            .
        \end{aligned}$$

 $P(u)$ is nonempty:  Let $u\in M$ be given. The map $x\mapsto{{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u)$ is a linear functional on $\mathbb R^n$. Thus we find $v\in\mathbb R^n$ representing it as $x\mapsto(x,v)$. Since $e_j\in X$, we have $$(e_j,v)={{\tilde c}_{\text{\rm o}}}(e_j)+\sum_{a\in A}({{\tilde c}_{a}}(e_j),u)\geq 0
            .$$ Further, using that $u\in M$ and $\tilde c(X)\subseteq{{\ensuremath{\widehat F}}}X$, we obtain that for each $x\geq 0$ $$(x,v)={{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u)
            \leq{{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}{\ensuremath{\mu_{X}}}({{\tilde c}_{a}}(x))
            \leq{\ensuremath{\mu_{X}}}(x)
            .$$ Together, we see that $v\in M$. By its definition, therefore, $v\in P(u)$.

 $P(u)$ is convex:  Let $v_1,v_2\in P(u)$ and $p\in[0,1]$. First, since $M$ is convex, $pv_1+(1-p)v_2$ belongs to $M$. Second, for each $x\geq 0$, $$\begin{aligned}
            (x,pv_1+ &\, (1-p)v_2)=p(x,v_1)+(1-p)(x,v_2)
            \\
            \geq &\, p\Big({{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u)\Big)+
            (1-p)\Big({{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u)\Big)
            \\
            = &\, {{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u)
            .
        \end{aligned}$$

 $P$ has closed graph:  Let $u_n\in M$, $u_n\to u$, and $v_n\in P(u_n)$, $v_n\to v$. Then $u,v\in M$ since $M$ is closed. Now fix $x\geq 0$. Continuity of the scalar product allows to pass to the limit in the relation $${{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),v_n)\leq(x,u_n)
            ,$$ which holds for all $n\in\mathbb N$. This yields ${{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),v)\leq(x,u)$.

Having verified all necessary hypothesis, Theorem \[Kak\] can be applied and furnishes us with $u\in M$ satisfying $u\in P(u)$, explicitly, $u\in\mathbb R^n$ with $$\label{1}
        u\geq 0,\quad (x,u)\leq{\ensuremath{\mu_{X}}}(x),x\geq 0,\quad {{\tilde c}_{\text{\rm o}}}(x)+\sum_{a\in A}({{\tilde c}_{a}}(x),u)\leq(x,u),x\geq 0
        .$$ Set $Y=\{x\geq 0\mid (x,u)\leq 1\}$. Then $Y$ is a , and by definition contained in $\mathbb R_+^n$. It contains $X$ since $u\in M$, and since $u\in P(u)$ we have $\tilde c(Y)\subseteq{{\ensuremath{\widehat F}}}Y$. Thus $d=\tilde c|_Y$ turns $Y$ into an ${{\ensuremath{\widehat F}}}$-coalgebra, and since $c=\tilde c|_X=(\tilde c|_Y)|_X=d|_X$, the inclusion map $\iota\colon X\to Y$ is an ${{\ensuremath{\widehat F}}}$-coalgebra morphism.

It remains to show that $Y$ is generated by $n$ linearly independent vectors. Remembering again Example \[Pyramid\], this is equivalent to $u$ being strictly positiv. Let $I=\{j\in\{1,\ldots,n\}\mid (e_j,u)=0\}$. For each $j\in I$ the last relation in implies that ${{c}_{\text{\rm o}}}(e_j)=0$ and $({{c}_{a}}(e_j),u)=0$, $a\in A$. Since $u\geq 0$ and ${{c}_{a}}(e_j)\geq 0$, we conclude that the vector ${{c}_{a}}(e_j)$ can have nonzero components only in those coordinates where $u$ has zero component. In other words, ${{c}_{a}}(e_j)\in\operatorname{span}\{e_i\mid i\in I\}$. Now gives $I=\emptyset$.

Proof details for properness of ${{\ensuremath{\widehat F}}}$
=============================================================

We denote $v_j=(1,\ldots,1)\in\mathbb R^{n_j}$. By Example \[Pyramid\] $$\mu_{\Delta^{n_j}}(x_j)=(x_j,v_j),\ x_j\in\mathbb R_+^{n_j}
        .$$ Since $(\Delta^{n_j},c_j)$ is an ${{\ensuremath{\widehat F}}}$-coalgebra, Corollary \[Ghat-Minko-Coalg\] yields $${{\tilde c{_j}}_{\text{\rm o}}}(x_j)+\sum_{a\in A}({{\tilde c{_j}}_{a}}(x_j),v_j)\leq(x_j,v_j),\quad x_j\in\mathbb R_+^{n_j}
        ,j=1,2
        .$$ Summing up these two inequalities yields that for $x_1\in\mathbb R_+^{n_1}$ and $x_2\in\mathbb R_+^{n_2}$ $$\label{7}
        \Big[{{\tilde c{_1}}_{\text{\rm o}}}(x_1)+{{\tilde c{_2}}_{\text{\rm o}}}(x_2)\Big]+
        \sum_{a\in A}\Big[({{\tilde c{_1}}_{a}}(x_1),v_1)+({{\tilde c{_2}}_{a}}(x_2),v_2)\Big]
        \leq(x_1,v_1)+(x_2,v_2)
        .$$ Recall that $Z$ denotes the linear subspace of $\mathbb R^{n_1}\times\mathbb R^{n_2}$ constructed in the basic diagram (referring back to Lemma \[Prod\]). The definition of the map $d$ in the basic diagram ensures that for $(x_1,x_2)\in Z$ $${{d}_{\text{\rm o}}}((x_1,x_2))={{\tilde c{_1}}_{\text{\rm o}}}(x_1)={{\tilde c{_2}}_{\text{\rm o}}}(x_2),\quad 
        {{d}_{a}}((x_1,x_2))=\big({{\tilde c{_1}}_{a}}(x_2),{{\tilde c{_2}}_{a}}(x_2)\big)
        .$$ Set $v=\frac 12(1,\ldots,1)\in\mathbb R^{n_1+n_2}$. Plugging the above into and dividing by $2$ yields $${{d}_{\text{\rm o}}}((x_1,x_2))+\sum_{a\in A}\big({{d}_{a}}((x_1,x_2)),v)\leq \big((x_1,x_2),v\big)
        ,\quad (x_1,x_2)\in Z\cap\mathbb R_+^{n_1+n_2}
        .$$ We have $$\mu_{Z\cap 2\Delta^{n_1+n_2}}(x)=\max\big\{\mu_Z(x),\mu_{2\Delta^{n_1+n_2}}(x)\big\}
        =
        \begin{cases}
            (x,v) &\hspace*{-3mm},\quad x\in Z\cap\mathbb R_+^{n_1+n_2},
            \\
            \infty &\hspace*{-3mm},\quad \text{otherwise}.
        \end{cases}$$ Here the first equality holds by property 3. listed after Definition \[Minko\]. The second equality is based on Example \[MinkoExa\] and Example \[Pyramid\]: First, $2\Delta^{n_1+n_2}$ is the pyramid constructed with $v$, and hence $\mu_{2\Delta^{n_1+n_2}}(x) = (x,v)$ if $x\geq 0$, and $\infty$ otherwise. Second, $Z$ is a linear subspace, hence in particular a convex cone, and thus $\mu_Z(x) = 0$ if $x\in Z$, and $\infty$ otherwise.

The inclusion $d(Z\cap 2\Delta^{n_1+n_2})\subseteq{{\ensuremath{\widehat F}}}(Z\cap 2\Delta^{n_1+n_2})$ can now be deduced with help of Lemma \[Ghat-Minko\]. Start with $(x_1,x_2)\in Z\cap 2\Delta^{n_1+n_2}$. Then $((x_1,x_2),v)\leq 1$. Moreover, $(x_1,x_2)\geq 0$ and $(x_1,x_2)\in Z$ which allows to apply $d$. We obtain $d_o(x_1,x_2) + \sum_a (d_a(x_1,x_2),v) \leq 1$. Since $d(Z)\subseteq F_{\mathbb R}(Z)$, we have $d_a(x_1,x_2)\in Z$. Now remember the computation of $d_a(x_1,x_2)$. The map $\tilde c_j$ is the linear extension of $c_j$, hence $$\tilde c_j(\Delta^{n_j}) = c_j(\Delta^{n_j}) \subseteq \hat F(\Delta^{n_j}) \subseteq [0,1]\times [0,1]^A
        .$$ In particular, $\tilde c_j$ takes nonnegative values on $\Delta^{n_j}$, and by linearity thus on all of $(\mathbb R_+)^{n_j}$. This shows $d_a(x_1,x_2)\geq 0$ and $d_o(x_1,x_2)\geq 0$. By the above computation of the Minkowski functional $\mu_{Z\cap 2\Delta^{n_1+n_2}}$, by now we know that we are in the first case, $(d_a(x_1,x_2),v)=\mu_{Z\cap 2\Delta^{n_1+n_2}}(d_a(x_1,x_2))$, and thus $$d_o(x_1,x_2) + \sum_a \mu_{Z\cap 2\Delta^{n_1+n_2}}(d_a(x_1,x_2)) \leq 1
        .$$ Lemma 16 applies, and yields $d(x_1,x_2)\in \hat F(Z\cap 2\Delta^{n_1+n_2})$.

Using the basic diagram, we obtain $$\begin{aligned}
        & \tilde c_j(\Delta^{n_j})\subseteq{{\ensuremath{\widehat F}}}\Delta^{n_j}\subseteq{{\ensuremath{\widehat F}}}Y_j,
        \\
        & \tilde c_j(\pi_j(Z\cap 2\Delta^{n_1+n_2}))\subseteq{{\ensuremath{\widehat F}}}(\pi_j(Z\cap 2\Delta^{n_1+n_2}))\subseteq{{\ensuremath{\widehat F}}}Y_j.
    \end{aligned}$$ Since $\tilde c_j$ is linear, in particular convex, and ${{\ensuremath{\widehat F}}}Y_j$ is convex, it follows that $$\tilde c_j\big(\operatorname{co}(\Delta^{n_j}\cup\pi_j(Z\cap 2\Delta^{n_1+n_2}))\big)\subseteq{{\ensuremath{\widehat F}}}Y_j
        .$$

We check that the  $Y_j$ satisfies the hypothesis of Theorem \[ExEx\]. By its definition $\Delta^{n_j}\subseteq Y_j\subseteq\mathbb R_+^{n_j}$. Since $Y_j$ is finitely generated, recall that $Y_j$ is the convex hull of two finitely generated s, it is a compact subset of $\mathbb R^{n_j}$. Finally, since the coalgebra structure on $Y_j$ is an extension of the one on $\Delta^{n_j}$, the present assumption implies that the condition of Theorem \[ExEx\] is satisfied. Note here that $\Delta^{n_j}\cap\operatorname{span}\{e_i\mid i\in I\}=\operatorname{co}(\{e_i\mid i\in I\}\cup\{0\})$.

Applying Theorem \[ExEx\] we obtain extensions $U_j$ as required.

We show that the diagram $$\xymatrix@C=60pt{
            \Delta^n \ar[r]^f \ar[d]_c & X \ar[d]^g
            \\
            {{\ensuremath{\widehat F}}}\Delta^n \ar[r]_{\operatorname{id}\times(f\circ -)} & [0,1]\times X^A
        }$$ commutes. First, for $k\not\in I$, we have $((\operatorname{id}\times(f\circ -))\circ c)(e_k)=(g\circ f)(e_k)$ by the definition of $g$. Second, consider $k\in I$. Then $(g\circ f)(e_k)=0$ since $f(e_k)=0$. By , also $((\operatorname{id}\times(f\circ -))\circ c)(e_k)=0$.

Since ${{\ensuremath{\widehat F}}}f$ maps ${{\ensuremath{\widehat F}}}\Delta^n$ into ${{\ensuremath{\widehat F}}}X$, we have $g(X)\subseteq{{\ensuremath{\widehat F}}}X$. This says that $X$ indeed becomes an ${{\ensuremath{\widehat F}}}$-coalgebra with structure $g$. Revisiting the above diagram shows that $f$ is an ${{\ensuremath{\widehat F}}}$-coalgebra morphism.

Applying Lemma \[GhatRedLem\] repeatedly, we obtain after finitely many steps an ${{\ensuremath{\widehat F}}}$-coalgebra $(\Delta^k,g)$ such that no nonempty subset $I\subseteq\{1,\ldots,k\}$ with exists for $(\Delta^k,g)$, and that we have an ${{\ensuremath{\widehat F}}}$-coalgebra morphism $f\colon (\Delta^n,c)\to(\Delta^k,g)$. Note here that in each application of the lemma the number of generators decreases.

[^1]: The notions of monads and algebraic categories are central to this paper. We recall them in Appendix \[sec:app-basics\] to make the paper accessible to all readers.

[^2]: This functor was denoted $\hat G$ in [@silva.sokolova:2011] where it was first studied in the context of axiomatization of trace semantics.

[^3]: In [@beal.lombardy.sakarovitch:2006] only a sketch of the proof is given, cf. [@beal.lombardy.sakarovitch:2006 §3.3]. In this sketch one important point is not mentioned. Using the terminology of [@beal.lombardy.sakarovitch:2006 §3.3]: it could a priori be possible that the size of the vectors in $G$ and the size of $G$ both oscillate.
