Czech Technical University in Prague, Czech Republic and Technische
Universität<EMAIL_ADDRESS>by the grant No.
19-0092S of the Czech Grant Agency Friedrich-Alexander-Universität Erlangen-
Nürnberg,
Germanystefan.milius@fau.dehttps://orcid.org/0000-0002-2021-1644Supported by
Deutsche Forschungsgemeinschaft (DFG) under project MI 717/7-1 and as part of
the Research and Training Group 2475 “Cybercrime and Forensic Computing”
(393541319/GRK2475/1-2019)Indiana University, Bloomington IN,
<EMAIL_ADDRESS>by grant #586136 from the Simons
Foundation.Jiří Adámek, Stefan Milius, Lawrence S. Moss [500]Theory of
computation Models of computation [500]Theory of computation Logic and
verification Fabio Gadducci and Alexandra Silva 2 9th Conference on Algebra
and Coalgebra in Computer Science (CALCO 2021) CALCO 2021 CALCO 2021 August
31–September 3, 2021 Salzburg, Austria 211 6

# Initial Algebras Without Iteration

Jiří Adámek  Stefan Milius  Lawrence S. Moss

###### Abstract

The Initial Algebra Theorem by Trnková et al. states, under mild assumptions,
that an endofunctor has an initial algebra provided it has a pre-fixed point.
The proof crucially depends on transfinitely iterating the functor and in fact
shows that, equivalently, the (transfinite) initial-algebra chain stops. We
give a constructive proof of the Initial Algebra Theorem that avoids
transfinite iteration of the functor. For a given pre-fixed point $A$ of the
functor, it uses Pataraia’s theorem to obtain the least fixed point of a
monotone function on the partial order formed by all subobjects of $A$. Thanks
to properties of recursive coalgebras, this least fixed point yields an
initial algebra. We obtain new results on fixed points and initial algebras in
categories enriched over directed-complete partial orders, again without
iteration. Using transfinite iteration we equivalently obtain convergence of
the initial-algebra chain as an equivalent condition, overall yielding a
streamlined version of the original proof.

###### category:

(Co)algebraic pearls

###### keywords:

Initial algebra, Pataraia’s theorem, recursive coalgebra, initial-algebra
chain

##  1 Introduction

Owing to the importance of initial algebras in theoretical computer science,
one naturally seeks results which give the existence of initial algebras in
the widest of settings. We can distinguish two different, but related ideas
which are commonly used in such results. By Lambek’s Lemma, for every
endofunctor $F\colon\mathscr{A}\to\mathscr{A}$, every initial algebra
$\alpha\colon FA\to A$ has a structure $\alpha$ which is an isomorphism. So
one might hope to obtain an initial algebra from a _fixed point_ , viz. an
$F$-algebra with isomorphic structure. It is sometimes much easier to find a
_pre-fixed point_ , an object $A$ together with a monomorphism $m\colon
FA\rightarrowtail A$. The Initial Algebra Theorem by Trnková et al. [28]
states that, with inevitable but mild assumptions, any functor $F$ which
preserves monomorphisms and has a pre-fixed point also has an initial algebra.
The proof uses the second prominent idea in the area: iteration, potentially
into the transfinite. Indeed, transfinite iteration of $F$ seems to be an
essential feature of the proof.

The purpose of this paper is to prove the Initial Algebra Theorem in as wide a
setting as possible with no use of iteration whatsoever. Moreover, the side
conditions are mild: they apply, e.g. to the categories of complete metric
spaces and directed-complete partial orders with a least element (shortly,
dcpo with bottom). To situate our method in a larger context, recall that some
fixed point theorems are proved with iteration, and some without. On the
iterative side, we find Kleene’s Theorem: continuous functions on
$\omega$-cpos with a least element have least fixed points obtained by
iteration in countably many steps; and Zermelo’s Theorem: monotone functions
on chain-complete posets with a least element have least fixed points, using a
transfinite iteration. On the non-iterative side, we have the Knaster-Tarski
Theorem: monotone functions on complete lattices have both least and greatest
fixed points, obtained by a direct definition without iteration. A relatively
new result is Pataraia’s Theorem: monotone functions on dcpos with bottom have
a least fixed point. The latter two theorems are ordinal-free and indeed
constructive.

The initial algebra for a functor $F$ can often be constructed by iterating
the functor, starting with the initial object $0$ and obtaining a transfinite
chain $0\to F0\to FF0\cdots$ (12). The reason why fixed point theorems are
useful for the proof of the Initial Algebra Theorem is that in every category
$\mathscr{A}$, the collection $\operatorname{\mathsf{Sub}}(A)$ of subobjects
of a given object $A$ is a partial order, and the iteration of $F$ can be
reflected by a particular monotone function
$f\colon\operatorname{\mathsf{Sub}}(A)\to\operatorname{\mathsf{Sub}}(A)$ when
$\alpha\colon FA\rightarrowtail A$ is a pre-fixed point; it takes a subobject
$u\colon B\rightarrowtail A$ to $\alpha\cdot Fu$. If
$\operatorname{\mathsf{Sub}}(A)$ is sufficiently complete, then $f$ has a
least fixed point, and we show that this yields an initial algebra for $F$.

In order to make this step it is important for us that joins in
$\operatorname{\mathsf{Sub}}(A)$ are given by colimits in $\mathscr{A}$.
Therefore Pataraia’s Theorem is the best choice as a basis for the move from
the least fixed point of $f$ to the initial $F$-algebra. The reasons are that
(a) it balances the weak assumption of monotonicity on $f$ with the
comparatively weak directed-completeness of the subobject lattice; and (b) its
use yields an ordinal-free proof (in contrast to using Zermelo’s Theorem, for
which (a) is also the case). In fact, we present many examples of categories
where directed joins of subobjects are given by colimits, while this is
usually not the case for arbitrary joins, rendering the Knaster-Tarski Theorem
a bad choice for us.

We start our exposition in subsection 2.1 with a review of Pataraia’s Theorem
and also its non-constructive precursor, Zermelo’s Theorem which we use later
in section 6. The second ingredient for the proof of our main result are
recursive coalgebras, which we tersely review in subsection 2.2. We use the
fact that a recursive coalgebra which is a fixed point already is an initial
algebra. section 3 discusses the property that joins of subobjects are given
by colimits. We make the technical notion of _smoothness_ parametric in a
class $\mathcal{M}$ of monomorphisms (representing subobjects), and we prove
our results for a smooth class $\mathcal{M}$.

Our main result is the new proof of the Initial Algebra Theorem in section 4.
We apply it in section 5 to the category $\mathsf{DCPO}_{\bot}$ of dcpos with
bottom. The class of all embeddings is smooth. We derive a new result: if an
endofunctor preserves embeddings and has a fixed point, then it has an initial
algebra which coincides with the terminal coalgebra.

Finally, section 6 rounds off our paper by providing the original Initial
Algebra Theorem, which features the initial-algebra chain obtained by
transfinite iteration. Although our proof has precisely the same mathematical
content as the original one, it is slightly streamlined in that it appeals to
Zermelo’s Theorem rather than unfolding its proof.

#### Related work.

Independently and at the same time, Pitts and Steenkamp [22] have obtained a
result on the existence of initial algebras, which makes use of _sized
functors_ and is formalizable in Agda. In effect, they show that a form of
iteration using sized functors is sufficient to obtain initial algebras. Our
work, while constructive, is not aimed at formalization, and, as previously
mentioned avoids iteration.

##  2 Preliminaries

We assume that readers are familiar with standard notions from the theory of
algebras and coalgebras for an endofunctor $F$. We denote an initial algebra
for $F$, provided it exists, by

$\iota\colon F(\mu F)\to\mu F.$

Recall that Lambek’s Lemma [17] states that its structure $\iota$ is an
isomorphism. This means that $\mu F$ is a _fixed point_ of $F$, viz. an object
$A\cong FA$.

###  2.1 Fixed Point Theorems

In this subsection we present preliminaries on fixed point theorems for
ordered structures. The most well-known such results are, of course, what is
nowadays called Kleene’s fixed point theorem and the Knaster-Tarski fixed
point theorem. The former is for $\omega$-cpos, partial orders with joins of
$\omega$-chains, with a least element (_bottom_ , for short). Kleene’s Theorem
states that every endofunction which is _$\omega$ -continuous_, that is
preserving joins of $\omega$-chains, on an $\omega$-cpo has a least fixed
point. The Knaster-Tarski Theorem [16, 24], makes stronger assumptions on the
poset but relaxes the condition on the endofunction. In its most general form
it states that a monotone endofunction $f$ on a complete lattice $P$ has a
least and greatest fixed point. Moreover, the fixed points of $f$ form a
complete lattice again.

Here we are interested in fixed point theorems that still work for arbitrary
monotone functions but make do with weaker completeness assumptions on the
poset $P$. One such result pertains to chain-complete posets. It should be
attributed to Zermelo, since the mathematical content of the result appears in
his 1904 paper [31] proving the Wellordering Theorem.

An _$i$ -chain_ in a poset $P$ for an ordinal number $i$ is a sequence
$(x_{j})_{j<i}$ of elements of $P$ with $x_{j}\leq x_{k}$ for all $j\leq k<i$.
The poset $P$ is said to be _chain-complete_ if every $i$-chain in it has a
join. In particular, $P$ has a least element $\bot$ (take $i=0$).

Let $f\colon P\to P$ be a monotone map on the chain-complete poset $P$. Then
we can define an ordinal-indexed sequence $f^{i}(\bot)$ by the following
transfinite recursion:

$f^{0}(\bot)=\bot,\quad f^{j+1}(\bot)=f(f^{j}(\bot)),\quad\text{and}\quad
f^{j}(\bot)=\bigvee_{i<j}f^{i}(\bot)\quad\mbox{for limit ordinals $j$}.$ (1)

It is easy to verify that this is a chain in $P$.

######  Theorem 2.1 (Zermelo).

Let $P$ be a chain-complete poset. Every monotone map $f\colon P\to P$ has a
least fixed point $\mu f$. Moreover, for some ordinal $i$ we have $\mu
f=f^{i}(\bot).$

######  Proof 2.2.

Take $i$ to be any ordinal larger than $|P|$, the cardinality of the set $P$.
For this $i$, there must be some $j<i$ such that $f^{j}(\bot)=f^{j+1}(\bot)$.
Indeed, this follows from Hartogs’ Lemma [14], stating that for every set $P$
there exists an ordinal $i$ such that there is no injection $i\rightarrowtail
P$. Thus, $f^{j}(\bot)$ is a fixed point of $f$. Let $f(x)=x$. An easy
transfinite induction shows that $f^{i}(\bot)\leq x$ for all $i$. Hence,
$f^{j}(\bot)$ is the least fixed point of $f$.

There are also variations on Theorem 2.1, such as the result often called the
Bourbaki-Witt Theorem [6, 30]; this states that every inflationary endo-map on
a chain-complete poset has a fixed point above every element. (A map $f\colon
P\to P$ is _inflationary_ , if $x\leq f(x)$ for every $x\in P$.)

Theorem 2.1 is not constructive. Our proof relied on Hartogs’ Lemma, which in
turn builds on the standard theory of ordinals. That theory uses classical
reasoning. A related point: some prominent results depending on ordinals are
known to be unavailable in constructive set theory (see [5]). For many of the
end results, there is an alternative, Pataraia’s Theorem [21], proved without
iteration and without ordinals (see Theorem 2.5). This result is at the heart
of this paper. It uses dcpos in lieu of chain-complete posets.

Pataraia sadly never published his result in written form. But it has appeared
e.g. in work by Escardó [11], Goubault-Larrecq [13], Bauer and Lumsdane [5]
based on a preprint by Dacar [9], and Taylor [27]. We present a proof based on
Martin’s presentation [19].

First recall that a _directed subset_ of a poset $P$ is a non-empty subset
$D\subseteq P$ such that every finite subset of $D$ has an upper bound in $D$.
The poset $P$ is called a _dcpo with bottom_ if it has a least element and
every directed subset $D\subseteq P$ has a join. Note that by Markowsky’s
Theorem [18], a poset is chain-complete iff it is a dcpo.

######  Remark 1.

  1. 1.

Observe that the set of all maps on a poset $P$ form a poset using the point-
wise order: $f\leq g$ if for every $x\in P$ we have $f(x)\leq g(x)$.

  2. 2.

Hence, $f\colon P\to P$ is inflationary iff
$\operatorname{\mathsf{id}}_{P}\leq f$, where $\operatorname{\mathsf{id}}_{P}$
is the identity function on $P$.

  3. 3.

Function composition is _left-monotone_ : we clearly have $f\cdot h\leq g\cdot
h$ whenever $f\leq g$. Right-monotonicity additionally requires that the fixed
argument be a monotone map: we have $f\cdot g\leq f\cdot h$ for every $g\leq
h$ whenever $f$ is monotone.

  4. 4.

A monoid $(M,\cdot,1)$ is _partially ordered_ if $M$ carries a partial order
such that multiplication is monotone: $a\leq b$ and $a^{\prime}\leq
b^{\prime}$ implies $a\cdot a^{\prime}\leq b\cdot b^{\prime}$. It is _directed
complete_ if it is a dcpo. An element $z\in M$ is a _zero_ if $z\cdot
m=z=m\cdot z$ for every $m\in M$.

######  Theorem 2.3 ([19, Thm. 1]).

Every directed complete monoid $(M,\cdot,1)$ whose bottom is the unit $1$ has
a top element which is a zero.

######  Proof 2.4.

The set $M$ itself is directed: for $m,n\in M$ we see that $m\cdot n$ is an
upper bound since

$m=m\cdot 1\leq m\cdot n\geq n\cdot 1=n,$

using that $1$ is the bottom and multiplication is monotone. Thus $M$ has a
top element $\top=\bigvee M$. We have $\top=\top\cdot 1\leq\top\cdot m$ for
every $m\in M$, and clearly $\top\cdot m\leq\top$. Thus, $\top\cdot m=\top$
and, similarly $m\cdot\top=\top$, whence $\top$ is a zero.

######  Theorem 2.5 (Pataraia’s Theorem).

Let $P$ be a dcpo with bottom. Then every monotone map on $P$ has a least
fixed point.

######  Proof 2.6.

  1. 1.

Let $M$ the set of all monotone inflationary maps on $P$. This is a monoid
under function composition, with the unit $\operatorname{\mathsf{id}}_{P}$.
Furthermore, $M$ is a dcpo with bottom. Indeed, the order is the pointwise
order from 1, the least element is $\operatorname{\mathsf{id}}_{P}$, and
directed joins are computed pointwise in $P$. Function composition is monotone
(in both arguments) by 1.3. By Theorem 2.3, $M$ therefore has a top element
$t\colon P\to P$ which is a zero.

  2. 2.

Let $f\colon P\to P$ be inflationary and monotone. Then $f\in M$ and therefore
$f\cdot t=t$. This means that for every $x\in P$, $f(t(x))=t(x)$, whence
$t(x)$ is a fixed point of $f$.

  3. 3.

Now let $f\colon P\to P$ be just monotone. Let $\mathcal{S}$ be the collection
of all subsets $S$ of $P$ which contain $\bot$, are closed under $f$, and
under joins of directed subsets. (In more detail, we require that if $s\in S$,
then $f(s)\in S$; and if $X\subseteq S$ is directed, $\bigvee X\in S$.)
Clearly, $\mathcal{S}$ is closed under arbitrary intersections. Let
$T=\bigcap\mathcal{S}$.

The set of all post-fixed points $x\leq f(x)$ belongs to $\mathcal{S}$.
Indeed, $\bot\leq f(\bot)$, and $f(x)\leq f(f(x))$ whenever $x\leq f(x)$.
Moreover, a join $p=\bigvee D$ of a directed set $D$ of post-fixed points of
$f$ is post-fixed point: $p$ satisfies $d\leq f(d)\leq f(p)$ for every $d\in
D$ due to the monotonicity of $f$; thus, $p\leq f(p)$. By the minimality of
$T$, we therefore know that $T$ consists of post-fixed points of $f$. Thus,
$f$ restricts to a function $f\colon T\to T$. That restriction is inflationary
(and monotone, of course) and therefore has a fixed point $p$ by Item 2.

  4. 4.

We show that $p$ is a least fixed point of $f\colon P\to P$. Suppose that $x$
is any fixed point. The set $L=\\{y\in P:y\leq x\\}$ belongs to $\mathcal{S}$.
Therefore $T\subseteq L$, which implies $p\leq x$.

######  Corollary 2.7.

The collection of all fixed points of a monotone map on a dcpo with bottom
forms a sub-dcpo.

This is analogous to fixed points of a monotone map on a complete lattice
forming a complete lattice again, see Tarski [24].

######  Proof 2.8.

Let $f$ be monotone on the dcpo with bottom $P$. Put $S=\\{x\in P:x=f(x)\\}$.
Suppose that $D\subseteq S$ be a directed subset, and let $w=\bigvee D$ be its
join in $P$. Then we have $x=f(x)\leq f(w)$ for every $x\in S$ since $f$ is
monotone. Therefore $w\leq f(w)$ since $w$ is the join of $S$. We now see that
$f$ restricts to $W=\\{y\in P,w\leq y\\}$, the set of all upper bounds of $D$
in $P$: for every $y\in W$ we have $w\leq f(w)\leq f(y)$, which shows that
$f(y)\in W$. Moreover, $W$ is clearly a dcpo: it has least element $w$, and
the join of every directed set of upper bounds of $D$ is an upper bound, too.
By Theorem 2.5, the restriction of $f$ to $W$ has a least fixed point $p$,
say. In other words, $p$ is the least fixed point of $f$ among the upper
bounds of $D$ in $P$, and therefore it is the desired join of $D$ in $S$.

Here is our statement of a principle which we shall use later as a key step in
our main result. It also appears in work by Escardó [11, Thm. 2.2] and Taylor
[27].

######  Corollary 2.9 (Pataraia Induction Principle).

Let $P$ be a dcpo with bottom. If $f\colon P\to P$ is monotone, then $\mu f$
belongs to every subset $S\subseteq P$ which contains $\bot$ and is closed
under $f$ and under directed joins.

This follows from the proof of Theorem 2.5: items 3 and 4 show that $\mu f\in
S$.

We apply the above principle to prove the following result that we will use in
section 5. A monotone function $f$ on a dcpo $D$ with bottom is _continuous_
if it preserves directed joins, and _strict_ if $f(\bot)=\bot$.

######  Lemma 2.10.

Let $P,Q$ be dcpos with bottom and let $f\colon P\to P$ and $g\colon Q\to Q$
be monotone. For every strict continuous map $h\colon P\to Q$ such that
$g\cdot h=h\cdot f$ we have $h(\mu f)=\mu g$.

######  Proof 2.11.

First, $h(\mu f)$ is a fixed point of $g$: we have $g(h(\mu f))=h(f(\mu
f))=h(\mu f).$ Therefore $\mu g\leq h(\mu f)$. For the reverse, let $S=\\{x\in
P:h(x)\leq\mu g\\}$. Since $h$ is strict, we see that $\bot\in S$. Moreover,
$S$ is closed under $f$, for if $x\in S$ we obtain $h(f(x))=g(h(x))\leq g(\mu
g)=\mu g$ using monotonicity of $g$ in the second step. Finally, $S$ is closed
under directed joins: if $D\subseteq S$ is a directed set we obtain $h(\bigvee
D)=\bigvee_{x\in D}h(x)\leq\bigvee_{x\in D}\mu g=\mu g,$ whence $\bigvee D$
lies in $S$. Thus, by 2.9, $\mu f\in S$, which means that $h(\mu f)\leq\mu g$.

###  2.2 Recursive Coalgebras

A crucial ingredient for our new proof of the Initial Algebra Theorem are
recursive coalgebras. They are closely connected to well-founded coalgebras
and hence to the categorical formulation of well-founded induction. In his
work on categorical set theory, Osius [20] first studied the notions of well-
founded and recursive coalgebras (for the power-set functor on sets and, more
generally, the power-object functor on an elementary topos). He defined
recursive coalgebras as those coalgebras $\alpha\colon A\to\mathscr{P}A$ which
have a unique coalgebra-to-algebra homomorphism into every algebra (see 2).

Taylor [26, 25, 27] considered recursive coalgebras for a general endofunctor
under the name ‘coalgebras obeying the recursion scheme’, and proved the
General Recursion Theorem that all well-founded coalgebras are recursive for
more general endofunctors; a new proof with fewer assumptions appears in
recent work [2]. Recursive coalgebras were also investigated by Eppendahl
[10], who called them algebra-initial coalgebras.

Capretta, Uustalu, and Vene [8] studied recursive coalgebras, and they showed
how to construct new ones from given ones by using comonads. They also
explained nicely how recursive coalgebras allow for the semantic treatment of
recursive divide-and-conquer programs. Jeannin et al. [15] proved the general
recursion theorem for polynomial functors on the category of many-sorted sets;
they also provided many interesting examples of recursive coalgebras arising
in programming.

In this section we will just recall the definition and a few basic results on
recursive coalgebras which we will need for our proof of the initial algebra
theorem.

######  Definition 2.

A coalgebra $\gamma\colon C\to FC$ is _recursive_ if for every algebra
$\alpha\colon FA\to A$ there exists a unique coalgebra-to-algebra morphism
$h\colon C\to A$, i.e. a unique morphism $h$ such that the square below
commutes:

${C}$${A}$${FC}$${FA}$$\scriptstyle{\gamma}$$\scriptstyle{h}$$\scriptstyle{Fh}$$\scriptstyle{\alpha}$
(2)

Recursive coalgebras are regarded as a full subcategory of the category
$\mathop{\mathsf{Coalg}}F$ of all coalgebras for the functor $F$.

######  Definition 3.

A _fixed-point_ of an endofunctor is an object $C$ together with an
isomorphism $C\cong FC$. We consider $C$ both as an algebra and a coalgebra
for $F$.

######  Remark 4 ([8, Prop. 7]).

Every recursive fixed point is an initial algebra: for a coalgebra
$(C,\gamma)$ with $\gamma$ invertible, the coalgebra-to-algebra morphisms from
$(C,\gamma)$ to an algebra $(A,\alpha)$ are the same as the algebra
homomorphisms from $(C,\gamma^{-1})$ to $(A,\alpha)$.

######  Proposition 2.12 ([8, Prop. 6]).

If $(C,\gamma)$ is a recursive coalgebra, then so is $(FC,F\gamma)$.

######  Proof 2.13.

Let $(A,\alpha)$ be an algebra and denote by $h\colon C\to A$ the unique
coalgebra-to-algebra morphism. We will show that

$g=\big{(}FC\xrightarrow{\leavevmode\nobreak\ Fh\leavevmode\nobreak\
}FA\xrightarrow{\leavevmode\nobreak\ \alpha\leavevmode\nobreak\ }A\big{)}$

is the unique coalgebra-to-algebra morphism from $(FC,F\gamma)$ to
$(A,\alpha)$. First, diagram (2) for $g$ commutes as can be seen on the left
below:

${FC}$${FA}$${A}$${FFC}$${FFA}$${FA}$$\scriptstyle{Fh}$$\scriptstyle{F\gamma}$$\scriptstyle{g}$$\scriptstyle{\alpha}$$\scriptstyle{FFh}$$\scriptstyle{Fg}$$\scriptstyle{F\alpha}$$\scriptstyle{F\alpha}$$\scriptstyle{\alpha}$
${C}$${FC}$${A}$${FC}$${FFC}$${FA}$$\scriptstyle{\gamma}$$\scriptstyle{k\cdot\gamma}$$\scriptstyle{\gamma}$$\scriptstyle{k}$$\scriptstyle{F\gamma}$$\scriptstyle{F\gamma}$$\scriptstyle{F(k\cdot\gamma)}$$\scriptstyle{Fk}$$\scriptstyle{\alpha}$

To see that $g$ is unique, suppose that $k\colon FC\to A$ is a coalgebra-to-
algebra morphism from $(FC,F\gamma)$ to $(A,\alpha)$. Then $k\cdot\gamma\colon
C\to A$ is one from $(C,\gamma)$ to $(A,\alpha)$. This is shown by the diagram
on the right above. Thus, we have $h=k\cdot\gamma$, and we conclude that

$g=\alpha\cdot Fh=\alpha\cdot Fk\cdot F\gamma=k,$

where the last equation holds since $k$ is a coalgebra-to-algebra morphism.

######  Corollary 2.14.

If a terminal recursive $F$-coalgebra exists, it is a fixed point of $F$.

Indeed, the proof is the same as that for Lambek’s Lemma, using 2.12 to see
that for a terminal recursive coalgebra $(T,\tau)$, the coalgebra $(FT,F\tau)$
is recursive, too: the unique coalgebra homomorphism
$h\colon(FT,F\tau)\to(T\tau)$ satisfies
$h\cdot\tau=\operatorname{\mathsf{id}}_{T}$ since
$\tau\colon(T,\tau)\to(FT,F\tau)$ is a coalgebra homomorphism, and finally,
$\tau\cdot h=Fh\cdot
F\tau=F\operatorname{\mathsf{id}}_{T}=\operatorname{\mathsf{id}}_{FT}$.

######  Theorem 2.15 ([8, Prop. 7]).

The terminal recursive coalgebra is precisely the same as the initial algebra.

In more detail, let $F\colon\mathscr{A}\to\mathscr{A}$ be an endofunctor. Then
we have:

  1. 1.

If $(T,\tau)$ is a terminal recursive coalgebra, then $(T,\tau^{-1})$ is a
initial algebra.

  2. 2.

If $(\mu F,\iota)$ is an initial algebra, then $(\mu F,\iota^{-1})$ is a
terminal recursive coalgebra.

######  Proof 2.16.

  1. 1.

By 2.14, we know that $\tau$ is an isomorphism. By 4, $(T,\tau^{-1})$ is an
initial algebra.

  2. 2.

The coalgebra $(\mu F,\iota^{-1})$ is clearly recursive. It remains to verify
its terminality. So let $(C,\gamma)$ be a recursive coalgebra. There is a
unique coalgebra-to-algebra morphism from $(C,\gamma)$ to the algebra $(\mu
F,\iota)$ to $(A,\alpha)$, and this means that there is a unique coalgebra
homomorphism $h\colon(C,\gamma)\to(\mu F,\iota^{-1})$.

######  Proposition 2.17.

Every colimit of recursive coalgebras is recursive.

######  Proof 2.18.

We use the fact that the colimits in $\mathop{\mathsf{Coalg}}F$, the category
of coalgebras for $F$, are formed on the level of the underlying category.
Suppose that we are given a diagram of recursive coalgebras
$(C_{i},\gamma_{i})$, $i\in I$, with a colimit cocone
$c_{i}\colon(C_{i},\gamma_{i})\to(C,\gamma)$ in $\mathop{\mathsf{Coalg}}F$. We
prove that $(C,\gamma)$ is recursive, too. Indeed, given an algebra
$(A,\alpha)$ one takes for every $i$ the unique coalgebra-to-algebra morphisms
$h_{i}\colon(C_{i},\gamma_{i})\to(A,\alpha)$. Using unicity one sees that all
$h_{i}$ form a cocone of the diagram formed by all $C_{i}$ in the underlying
category. Therefore, there is a unique morphism $h\colon C\to A$ such that
$h\cdot c_{i}=h_{i}$ holds for all $i\in I$. We now verify that $h$ is the
desired unique coalgebra-to-algebra morphism using the following diagram:

${C_{i}}$${C}$${A}$${FC_{i}}$${FC}$${FA}$$\scriptstyle{c_{i}}$$\scriptstyle{\gamma_{i}}$$\scriptstyle{h_{i}}$$\scriptstyle{\gamma}$$\scriptstyle{h}$$\scriptstyle{Fc_{i}}$$\scriptstyle{Fh_{i}}$$\scriptstyle{Fh}$$\scriptstyle{\alpha}$

We know that the upper and lower parts, the left-hand square and the outside
commute. Therefore so does the right-hand square when precomposed by every
$c_{i}$. Since the colimit injections $c_{i}$ form a jointly epic family, we
thus see that the right-hand square commutes if and only if $h\cdot
c_{i}=h_{i}$ holds for all $i\in I$.

##  3 Smooth Monomorphisms

As we have just seen in 2.17, the collection of recursive coalgebras is closed
under colimits. In order to apply an order-theoretic fixed point theorem to
this collection, or to subcollections of it, we need a connection between
colimits and subobjects. We make this connection by using the definition of
_smooth class_ of monomorphisms in a category.

For an object $A$ of a category $\mathscr{A}$, a _subobject_ is represented by
a monomorphism $s\colon S\rightarrowtail A$. If $s$ and $t\colon
T\rightarrowtail A$ are monomorphisms, we write $s\leq t$ if $s$ factorizes
through $t$. If also $t\leq s$ holds, then $t$ and $s$ represent the same
subobject; in particular $S$ and $T$ are then isomorphic. Generalizing a bit,
let $\mathcal{M}$ be a class of monomorphisms. An _$\mathcal{M}$ -subobject_
of $A$ is a subobject represented by a morphism $s\colon S\to A$ in
$\mathcal{M}$. If the object $A$ has only a set of subobjects, then we write

$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$

for the poset of $\mathcal{M}$-subobjects of $A$.

If every object $A$ only has a set of $\mathcal{M}$-subobjects, then
$\mathscr{A}$ is called _$\mathcal{M}$ -well-powered_.

######  Definition 5.

Let $\mathcal{M}$ be a class of monomorphisms closed under isomorphisms and
composition.

  1. 1.

We say that an object $A$ has _smooth $\mathcal{M}$-subobjects_ provided that
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$ is a dcpo with bottom (in
particular, not a proper class) where the least element and directed joins are
given by colimits of the corresponding diagrams of subobjects.

  2. 2.

The class $\mathcal{M}$ is _smooth_ if every object of $\mathscr{A}$ has
smooth $\mathcal{M}$-subobjects.

Moreover, we say that a category has _smooth monomorphisms_ if the class of
all monomorphisms is smooth.

######  Remark 6.

  1. 1.

In more detail, let $D\subseteq\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$
be a directed set of subobjects represented by $m_{i}\colon
A_{i}\rightarrowtail A$ ($i\in D$). Then $D$ has a join $m\colon
C\rightarrowtail A$ in $\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$.
Moreover, consider the diagram of objects $(A_{i})_{i\in D}$ with connecting
morphisms $a_{i,j}\colon A_{i}\rightarrowtail A_{j}$ for $i\leq j$ in $D$
given by the unique factorizations witnessing $m_{i}\leq m_{j}$:

${A_{i}}$${A_{j}}$${A}$$\scriptstyle{a_{i,j}}$$\scriptstyle{m_{i}}$$\scriptstyle{m_{j}}$

(Note that $a_{i,j}$ need not lie in $\mathcal{M}$.) Then for every $i\in D$
there exists a monomorphism $c_{i}\colon A_{i}\rightarrowtail C$ with $m\cdot
c_{i}=m_{i}$, since $m_{i}\leq m$. The smoothness requirement is that these
monomorphisms form a colimit cocone.

  2. 2.

Requiring that the least subobject in
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}{A}$ is given by (the empty) colimit
means that $\mathscr{A}$ has an initial object $0$ and the unique morphism
$0\rightarrowtail A$ lies in $\mathcal{M}$.

  3. 3.

If $\mathcal{M}$ is a smooth class, then $\mathscr{A}$ is $\mathcal{M}$-well-
powered.

Since the above notion of smoothness is new, we discuss examples at length
now. Below we show that in a number of categories the collection of all
monomorphisms is smooth, as is the collection of all strong monomorphisms
(those having the diagonal fill-in property with respect to epimorphisms). We
also present some counterexamples and discuss other classes $\mathcal{M}$.

Recall the concept of a _locally finitely presentable_ (_lfp_ , for short)
category (e.g. [4]): it is a cocomplete category $\mathscr{A}$ with a set of
finitely presentable objects (i.e. their hom-functors preserve filtered
colimits) whose closure under filtered colimits is all of $\mathscr{A}$.
Examples are $\mathsf{Set}$, $\mathsf{Pos}$ (posets and monotone maps),
$\mathsf{Gra}$ (graphs and homomorphisms) and all varieties of finitary
algebras such as monoids, vector spaces, rings, etc.

We say that $\mathscr{A}$ has a _simple_ initial object $0$ if all the
morphisms with domain $0$ are strong monomorphisms (equivalently, $0$ has no
proper quotients).

######  Example 3.1.

Both monomorphisms and strong monomorphisms are smooth in every lfp category
with a simple initial object $0$ [4, Cor. 1.63]. This includes $\mathsf{Set}$,
$\mathsf{Pos}$, $\mathsf{Gra}$, monoids and vector spaces. But not rings: in
that category the initial object is $\mathds{Z}$, the ring of integers, and
there are non-monic ring homomorphisms with that domain (e.g. $\mathds{Z}\to
1$).

######  Example 3.2.

Let us consider the category $\mathsf{DCPO}_{\bot}$ of dcpos with bottom and
continuous maps between them, where a map is _continuous_ if it is monotone
and preserves directed joins.

  1. 1.

In section 5 we prove that the class of all embeddings (9) is smooth. (These
play a major role in Smyth and Plotkin’s solution method for recursive domain
equations [23].) This example is one of several motivations for our move from
the class of all monomorphisms to the more general situation of a class
$\mathcal{M}$ in 5.

  2. 2.

In contrast, the class of all monomorphisms is non-smooth in
$\mathsf{DCPO}_{\bot}$. For example, consider the dcpo $\mathds{N}^{\top}$ of
natural numbers with a top element $\top$. The subposets
$C_{n}=\\{0,\ldots,n\\}\cup\\{\top\\}$, $n\in\mathds{N}$, form an
$\omega$-chain in $\mathsf{DCPO}_{\bot}$. Its colimit is
$\mathds{N}^{\top}\cup\\{\infty\\}$ where $n<\infty<\top$ for all
$n\in\mathds{N}$. The cocone of inclusion maps
$C_{n}\hookrightarrow\mathds{N}^{\top}$ consists of monomorphisms. However,
the factorizing morphism from $\mathop{\mathsf{colim}}C_{n}$ to
$\mathds{N}^{\top}$ is not monic, as it merges $\infty$ and $\top$.

  3. 3.

The same example demonstrates that strong monomorphisms are not smooth in
$\mathsf{DCPO}_{\bot}$.

######  Example 3.3.

  1. 1.

Let us consider the category $\mathsf{MS}$ of metric spaces with distances at
most $1$ and _non-expanding_ maps $f\colon(X,d_{X})\to(Y,d_{Y})$ (that is
$d_{Y}(f(x),f(y))\leq d_{X}(x,y)$ for all $x,y,\in X$. Although this category
is not lfp, both monomorphisms and strong monomorphisms form smooth classes.
The proof for strong monomorphisms is easy since the strong (equivalently,
extremal) subobjects of a metric space $A$ are represented by its subspaces
(with the inherited metric). Given a directed set of subspaces $A_{d}\subseteq
A$ ($d\in D$) their join in $\operatorname{\mathsf{Sub}}(A)$ the subspace
$\bigcup_{d\in D}A_{d}$ and this is also the colimit of the corresponding
diagram in $\mathsf{MS}$. The somewhat technical proof for monomorphisms is
given in the appendix (A.1).

  2. 2.

In the full subcategory $\mathsf{CMS}$ of $\mathsf{MS}$ given by all complete
metric spaces monomorpisms are not smooth. This can be demonstrated as in
3.2.2: Let $\mathds{N}^{\top}$ be the metric space with distances
$d(n,m)=|1/2^{-n}-1/2^{-m}|$ and $d(n,\top)=1/2^{-n}$, and consider the
$\omega$-chain of spaces $C_{n}$ where $d(n,\top)=1$ and other distances are
as in $\mathds{N}^{\top}$.

  3. 3.

In contrast, strong monomorphisms are smooth in $\mathsf{CMS}$ (see A.3).

The following equivalent formulation is often used in proofs.

######  Proposition 3.4.

An object $A$ has smooth $\mathcal{M}$-subobjects if and only if for every
directed diagram $D$ of monomorphisms in $\mathscr{A}$ (not necessarily
members of $\mathcal{M}$), and every cocone $m_{i}\colon A_{i}\rightarrowtail
A$, $i\in D$, of $\mathcal{M}$-monomorphisms, the following holds:

  1. 1.

the diagram $D$ has a colimit, and

  2. 2.

the factorizing morphism induced by the cocone $(m_{i})$ is again an
$\mathcal{M}$-monomorphism.

######  Proof 3.5.

The ‘only if’ direction is obvious. For the ‘if’ direction, suppose we are
given a directed set $D\subseteq\operatorname{\mathsf{Sub}}(A)$ of
$\mathcal{M}$-subobjects $m_{i}\colon A_{i}\rightarrowtail A$ for $i\in D$ as
in 6. By Item 1, the ensuing directed diagram of monomorphisms $a_{i,j}\colon
A_{i}\rightarrowtail A_{j}$ has a colimit $c_{i}\colon A_{i}\to C$, $i\in D$,
and we will prove that this yields the join $\bigvee_{i\in D}m_{i}$. By Item
2, we have a unique $\mathcal{M}$-monomorphism $m\colon C\rightarrowtail A$
such that $m\cdot c_{i}=m_{i}$ for all $i\in D$.

Now let $s\colon S\rightarrowtail A$ be any $\mathcal{M}$-subobject with
$m_{i}\leq s$ for all $i\in D$. That is, we have morphisms $s_{i}\colon
A_{i}\to S$ with $s\cdot s_{i}=m_{i}$ for all $i\in D$. They form a cocone
because for the monomorphism $a_{i,j}\colon A_{i}\rightarrowtail A_{j}$
witnessing $m_{i}\leq m_{j}$ we have

$s\cdot s_{j}\cdot a_{i,j}=m_{j}\cdot a_{i,j}=m_{i}=s\cdot s_{i},$

whence $s_{j}\cdot a_{i,j}=s_{i}$ since $s$ is monic. We therefore obtain a
unique $t\colon C\to S$ with $t\cdot c_{i}=s_{i}$ for all $i\in D$.
Consequently, we have

$s\cdot t\cdot c_{i}=s\cdot s_{i}=m_{i}=m\cdot c_{i}\qquad\text{for all $i\in
D$.}$

Since the colimit injections $c_{i}$ form an epic family, we conclude that
$s\cdot t=m$, which means that $m\leq s$ in
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$, as desired.

######  Remark 7.

  1. 1.

Note that the conditions for $\mathcal{M}$ to be smooth are a part of the
conditions of Taylor’s notion of a _locally complete class of supports_ [25,
Def. 6.1. & 6.3] (see also [27, Assumption 4.18]).

  2. 2.

Smoothness previously appeared for joins and colimit of chains in lieu of
directed sets [2]. That formulation is related to the list of conditions for a
class of monomorphisms given by Trnková et al. [28]. Note that a class
$\mathcal{M}$ of monomorphisms containing the identities and closed under
composition can be regarded as the subcategory of $\mathscr{A}$ given by all
morphisms in $\mathcal{M}$. The list of conditions in op. cit. is equivalent
to stating that the inclusion functor $\mathcal{M}\hookrightarrow\mathscr{A}$
creates colimits of chains. Requiring that the inclusion creates directed
colimits implies that the class $\mathcal{M}$ is smooth. For the converse, we
would need to add that for every directed diagram of
$\mathcal{M}$-monomorphisms the colimit cocone consists of
$\mathcal{M}$-monomorphisms.

##  4 The Initial Algebra Theorem

We are now ready to prove the main result of this paper.

######  Assumption 4.0.

Throughout this section we assume that $\mathscr{A}$ is a category with a
class $\mathcal{M}$ of monomorphisms containing all isomorphisms and closed
under composition. We say that $F\colon\mathscr{A}\to\mathscr{A}$ _preserves
$\mathcal{M}$_ if $m\in\mathcal{M}$ implies $Fm\in\mathcal{M}$.

######  Definition 8.

An _$\mathcal{M}$ -pre-fixed point_ of $F$ is an algebra whose structure
$m\colon FA\rightarrowtail A$ lies in $\mathcal{M}$. In the case where
$\mathcal{M}$ consists of all monomorphisms we speak of a pre-fixed point.

######  Theorem 4.1 (Initial Algebra Theorem).

Let $m\colon FA\rightarrowtail A$ be an $\mathcal{M}$-pre-fixed point for an
endofuctor preserving $\mathcal{M}$. If $A$ has smooth
$\mathcal{M}$-subobjects, then $F$ has an initial algebra which is an
$\mathcal{M}$-subalgebra of $(A,m)$.

######  Proof 4.2.

We have the following endomap

$f\colon\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)\to\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)\quad\text{defined
by}\quad f\big{(}\leavevmode\hbox to41.59pt{\vbox
to10.12pt{\pgfpicture\makeatletter\hbox{\hskip 20.79338pt\lower-6.51657pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.79338pt}{-6.41664pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
7.0434pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.0434pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${B}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
7.0434pt\hfil&\hfil\hskip 26.75pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.75pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${A}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
6.75pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{-7.42662pt}{-3.91664pt}\pgfsys@lineto{9.69345pt}{-3.91664pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-7.22664pt}{-3.91664pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.89343pt}{-3.91664pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.71019pt}{-1.56387pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{u}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\big{)}=\big{(}\leavevmode\hbox
to90.73pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip
45.36284pt\lower-6.51657pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-48.36284pt}{-6.41664pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
10.95313pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.95313pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${FB}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
10.95313pt\hfil&\hfil\hskip 30.65973pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.65973pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${FA}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
10.65973pt\hfil&\hfil\hskip 26.75pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.75pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${A}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
6.75pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{-24.17662pt}{-3.91664pt}\pgfsys@lineto{-7.05655pt}{-3.91664pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-23.97664pt}{-3.91664pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-6.85657pt}{-3.91664pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.19699pt}{-1.56387pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{Fu}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{ {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{17.14284pt}{-3.91664pt}\pgfsys@lineto{34.26291pt}{-3.91664pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{17.34282pt}{-3.91664pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{34.46289pt}{-3.91664pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{21.78983pt}{-1.56387pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{m}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\big{)}.$ (3)

It is clearly monotone. We are going to apply Pataraia Induction to it. We
take the subset $S\subseteq\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$ of
all $u\colon B\rightarrowtail A$ such that $u\leq f(u)$ via some recursive
coalgebra $\beta\colon B\to FB$. More precisely,

$S=\\{u\colon B\rightarrowtail A:\text{$u=m\cdot Fu\cdot\beta$ for some
recursive coalgebra $\beta\colon B\rightarrowtail FB$}\\}.$

Note that if $\beta$ exists for $u$, then it is unique. Moreover, $u\in S$ is
a coalgebra-to-algebra morphism from $(B,\beta)$ to $(A,m)$.

The least subobject $0\rightarrowtail A$ is clearly contained in $S$. Further,
$S$ is closed under $f$ since $(FB,F\beta)$ is a recursive coalgebra by 2.12:
for $u\in S$ we have

$f(u)=m\cdot Fu=m\cdot F(m\cdot Fu\cdot\beta)=m\cdot F(f(u))\cdot F\beta.$

We continue with the verification that $S$ is closed under directed joins. Let
$D\subseteq S$ be directed. Given $u\colon B_{u}\rightarrowtail A$ in $D$ we
write $\beta_{u}\colon B_{u}\to FB_{u}$ for the recursive coalgebra witnessing
$u\leq f(u)$. We show that these recursive coalgebras form a (then
necessarily) directed diagram. To see this, we only need to prove that every
morphism $h\colon B_{u}\rightarrowtail B_{v}$ witnessing $u\leq v$ in $D$;
i.e. $v\cdot h=u$, is a coalgebra homomorphism. Consider the diagram below:

${B_{u}}$${FB_{u}}$${B_{v}}$${FB_{v}}$${A}$${FA}$$\scriptstyle{\beta_{u}}$$\scriptstyle{h}$$\scriptstyle{u}$$\scriptstyle{Fh}$$\scriptstyle{Fu}$$\scriptstyle{\beta_{v}}$$\scriptstyle{v}$$\scriptstyle{Fv}$$\scriptstyle{m}$

Since the outside, the lower square and the left-hand and right-hand parts
commute, we see that the upper square commutes when extended by the
monomorphism $m\cdot Fv$. Thus it commutes, proving that $h$ is a coalgebra
homomorphism.

Now denote by $v\colon B\rightarrowtail A$ the join $\bigvee D$ in
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$. Since $A$ has smooth
subobjects, $B$ is the colimit of the diagram formed by the $B_{u}$, $u\in D$,
in $\mathscr{A}$. Since the forgetful functor
$\mathop{\mathsf{Coalg}}F\to\mathscr{A}$ creates colimits, we have a unique
coalgebra structure $\beta\colon B\to FB$ such that the colimit injections are
coalgebra homomorphisms; moreover $(B,\beta)$ is colimit of the coalgebras
$(B_{u},\beta_{u})$, $u\in D$. Thus, $(B,\beta)$ is recursive by 2.17.
Moreover, $v\colon B\rightarrowtail A$ is the unique morphism induced by the
cocone given by all $u\colon B_{u}\rightarrowtail A$ in $D$. Since every $u\in
S$ is the unique coalgebra-to-algebra morphism from $(B_{u},\beta_{u})$ to
$(A,m)$, we know from the proof of 2.17 that $v$ is the unique coalgebra-to-
algebra morphism from $(B,\beta)$ to $(A,m)$. Thus, $v$ lies in $S$.

By Theorem 2.5, $f$ has a least fixed point, and by 2.9, $\mu f\in S$. Denote
this subobject be $u\colon I\rightarrowtail A$. Since $u\in S$, there is a
recursive coalgebra $\iota\colon I\to FI$ such that $u=m\cdot Fu\cdot\iota$.
But $u$ and $f(u)=m\cdot Fu$ represent the same subobject of $A$. So $\iota$
is an isomorphism. Thus $(I,\iota^{-1})$ is an initial algebra by 4.

######  Corollary 4.3.

Let $\mathscr{A}$ be a category with a smooth class $\mathcal{M}$ of
monomorphisms. Then the following are equivalent for every endofunctor $F$
preserving $\mathcal{M}$:

  1. 1.

an initial algebra exists,

  2. 2.

a fixed point exists,

  3. 3.

an $\mathcal{M}$-pre-fixed point exists.

Moreover, if these hold, then $\mu F$ is an $\mathcal{M}$-subalgebra of every
$\mathcal{M}$-pre-fixed point of $F$.

Indeed, Lambek’s Lemma [17] tells us that 1 implies 2. Clearly, 2 implies 3
since $\mathcal{M}$ contains all isomorphisms. Theorem 4.1 shows that that 3
implies 1, and it also yields our last statement.

######  Corollary 4.4.

Let $\mathscr{A}$ be an lfp category with a simple initial object. An
endofunctor preserving monomorphisms has an initial algebra iff it has a pre-
fixed point.

######  Example 4.5.

We present examples which show, _inter alia_ , that neither of the hypotheses
in Theorem 4.1 can be left out. In each case $\mathcal{M}$ is the class of all
monomorphisms.

  1. 1.

The assumption that $0\to A$ is monic. Let $\mathscr{A}$ be the variety of
algebras $(A,u,c)$ with unary operation $u$ and a constant $c$. Its initial
object is $(\mathds{N},s,0)$ with $s(n)=n+1$, which is not simple. We present
an endofunctor having no initial algebra even though it has a fixed point and
preserves monomorphisms. Let $\mathscr{P}_{0}$ be the non-empty power-set
functor. We obtain an analogous endofunctor $\bar{\mathscr{P}}_{0}$ on
$\mathscr{A}$ defined by
$\bar{\mathscr{P}}_{0}(A,u,c)=(\mathscr{P}_{0}A,\mathscr{P}_{0}u,\\{c\\})$. It
clearly preserves monomorphisms, and the terminal object $1$ is a fixed point
of $\bar{\mathscr{P}}_{0}$ (since $\mathscr{P}_{0}1\cong 1$). This is, up to
isomorphism, the only fixed point. However, it is not
$\mu\bar{\mathscr{P}}_{0}$ because given an algebra on $(A,u,c)$ with
$u(x)\neq x$ for all $x\in A$, no $\bar{\mathscr{P}}_{0}$-algebra homomorphism
exists from $1$ to $A$.

  2. 2.

The assumption that $\operatorname{\mathsf{Sub}}(A)$ is a set in 5.1. Let
$\mathsf{Ord}$ be the totally ordered class of all ordinals taken as a
category. In the opposite category $\mathsf{Ord}^{\mathsf{op}}$, all morphisms
are monic, so every endofunctor preserves monomorphisms. For the functor $F$
on $\mathsf{Ord}^{\mathsf{op}}$ given by $F(i)=i+1$, every object is a pre-
fixed point, and there are no fixed points. For each object $i$,
$\operatorname{\mathsf{Sub}}(i)$ has all the properties requested in 5.1
except that it is a proper class.

  3. 3.

Preservation of monomorphisms. Here we use the category
$\mathsf{Set}\times\mathsf{Set}$ which satisfies all assumptions of Theorem
6.3. We define an endofunctor $F$ by $F(X,Y)=(\emptyset,1)$ if
$X\neq\emptyset$ and $F(X,Y)=(\emptyset,\mathscr{P}Y)$ else. It is defined on
morphisms as expected, using $\mathscr{P}$ in the case where $X=\emptyset$.
This functor has many pre-fixed points, e.g.
$F(1,1)=(\emptyset,1)\rightarrowtail(1,1)$. But it has no fixed points (thus
no initial algebra): first, $(\emptyset,Y)$ and $(\emptyset,\mathscr{P}Y)$ are
never isomorphic, by Cantor’s Theorem [7]. Second, if $X\neq\emptyset$, then
there exists no morphism from $(X,Y)$ to $F(X,Y)=(\emptyset,1)$.

##  5 Initial Algebras in $\mathsf{DCPO}_{\bot}$-enriched Categories

It follows from the seminal paper by Smyth and Plotkin [23] that every locally
continuous functor $F$ on a category $\mathscr{A}$ enriched over $\omega$-cpos
(i.e. partial orders with a least element and joins of $\omega$-chains) has an
initial algebra $(\mu F,\iota)$ which is also a terminal coalgebra by
inverting its structure. Local continuity means that the corresponding
mappings $\mathscr{A}(A,B)\to\mathscr{A}(FA,FB)$ preserve (pointwise) directed
joins. Here we assume the weaker property that $F$ is locally monotone; for
example, the endofunctor assigning to a dcpo its ideal completion is locally
monotone, whence preserves embeddings, but not locally continuous. We apply
4.3 to derive that such an endofunctor has a pre-fixed point given by an
embedding iff it has an initial algebra (being also the terminal coalgebra).

######  Definition 9.

  1. 1.

A category $\mathscr{A}$ is _$\mathsf{DCPO}_{\bot}$ -enriched_ provided that
each hom-set is equipped with the structure of a dcpo with bottom, and
composition preserves bottom and directed joins: for every morphism $f$ and
appropriate directed sets of morphisms $g_{i}$ ($i\in D$) we have

$\textstyle f\cdot\bot=\bot,\quad\bot\cdot f=\bot,\quad f\cdot\bigvee_{i\in
D}g_{i}=\bigvee_{i\in D}f\cdot g_{i},\quad\big{(}\bigvee_{i\in
D}g_{i}\big{)}\cdot f=\bigvee_{i\in D}g_{i}\cdot f.$ (4)

  2. 2.

A functor on $\mathscr{A}$ is _locally monotone_ if its restrictions
$\mathscr{A}(A,B)\to\mathscr{A}(FA,FB)$ to the hom-sets are monotone.

  3. 3.

A morphism $e\colon A\to B$ is called an _embedding_ if there exists a
morphism $\widehat{e}\colon B\to A$ such that $\widehat{e}\cdot
e=\operatorname{\mathsf{id}}_{A}$ and
$e\cdot\widehat{e}\sqsubseteq\operatorname{\mathsf{id}}_{B}$.

It is easy to see that the morphism $\widehat{e}$ is unique for $e$; it is
called its _projection_.

The following result is a slight variation of a result by Smyth and Plotkin
for $\omega$-cpos [23]. We include the proof in the appendix for the
convenience of the reader.

######  Theorem 5.1.

Let $D$ be a directed diagram of embeddings in a
$\mathsf{DCPO}_{\bot}$-enriched category. For every cocone $(c_{i}\colon
D_{i}\to C)$ of $D$, the following are equivalent:

  1. 1.

The cocone $(c_{i})$ is a colimit.

  2. 2.

Each $c_{i}$ is an embedding, the composites $c_{i}\cdot\widehat{c}_{i}$ form
a directed set in $\mathscr{A}(C,C)$, and

$\textstyle\bigsqcup_{i}c_{i}\cdot\widehat{c}_{i}=\operatorname{\mathsf{id}}_{C}.$
(5)

######  Remark 10.

A $\mathsf{DCPO}_{\bot}$-enriched category $\mathscr{A}$ is
$\mathcal{M}$-well-powered for the class $\mathcal{M}$ of all embeddings. The
reason is that, given an object $A$, a subobject represented by an embedding
$e\colon S\to A$ is determined by the endomorphism $e\cdot\widehat{e}$ on $A$.
Indeed, let $f\colon T\to A$ be an embedding with
$e\cdot\widehat{e}=f\cdot\widehat{f}$. Then $e=e\cdot\widehat{e}\cdot
e=f\cdot\widehat{f}\cdot e$. Therefore, $e\leq f$ in
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$. By symmetry $f\leq e$. Since
$\mathscr{A}(A,A)$ is a set, $\mathcal{M}$-well-poweredness follows.

######  Theorem 5.2.

Let $\mathscr{A}$ be a $\mathsf{DCPO}_{\bot}$-enriched category with directed
colimits. Then the class of all embeddings is smooth.

The proof is presented in subsection A.3.

######  Corollary 5.3.

Let $\mathscr{A}$ be a $\mathsf{DCPO}_{\bot}$-enriched category with directed
colimits. For a locally monotone endofunctor $F$ the following are equivalent:

  1. 1.

an initial algebra exists,

  2. 2.

a terminal coalgebra exists,

  3. 3.

a fixed point exists.

Moreover, if $(\mu F,\iota)$ is an initial algebra, then $(\mu F,\iota^{-1})$
is a terminal coalgebra.

Item 3 can be strengthened to state existence of a pre-fixed point carried by
an embedding.

######  Proof 5.4.

The dual category $\mathscr{A}^{\mathsf{op}}$ is
$\mathsf{DCPO}_{\bot}$-enriched w.r.t. the same order on hom-sets. But the
embeddings in $\mathscr{A}^{\mathsf{op}}$ are precisely the projections in
$\mathscr{A}$. Every locally monotone endofunctor $F$ on $\mathscr{A}$ clearly
preserves embeddings and projections. Thus, the dual functor $F^{\mathsf{op}}$
on $\mathscr{A}^{\mathsf{op}}$ preserves embeddings. Now 1 $\Leftrightarrow$ 3
follows from an application of 4.3 to $\mathscr{A}$ and $F$, and 2
$\Leftrightarrow$ 3 is an application to $\mathscr{A}^{\mathsf{op}}$ and
$F^{\mathsf{op}}$. In each case the class $\mathcal{M}$ consists of all
embeddings in $\mathscr{A}$ and $\mathscr{A}^{\mathsf{op}}$, respectively.

Finally, we prove that the initial algebra and terminal coalgebra coincide.
Let $\iota\colon FI\to I$ be an initial algebra. Then we know that a terminal
coalgebra $\tau\colon T\to FT$ exists. Moreover, from the last statement in
4.3 applied to $F$ and its fixed point $(T,\tau^{-1})$ we see that the unique
$F$-algebra homomorphism $e\colon(I,\iota)\to(T,\tau^{-1})$ is an embedding.
Another application of 4.3 to $F^{\mathsf{op}}$ and its fixed point
$(I,\iota^{-1})$ yields that the unique $F^{\mathsf{op}}$-algebra homomorphism
$f\colon\mu F^{\mathsf{op}}=(T,\tau)\to(I,\iota^{-1})$ is an embedding in
$\mathscr{A}^{\mathsf{op}}$. This means that this an $F$-coalgebra
homomorphism $f\colon(I,\iota^{-1})\to(T,\tau)$ which is a projection in
$\mathscr{A}$. By the universal properties of $(I,\iota)$ and $(T,\tau)$,
$e=f$, and this morphism is both an embedding and a projections, whence an
isomorphism.

The requirement of local monotonicity of $F$ can be weakened: the theorem
holds for any endofunctor $F$ which fulfils
$Ff\sqsubseteq\operatorname{\mathsf{id}}_{FA}$ whenever
$f\sqsubseteq\operatorname{\mathsf{id}}_{A}$. Indeed, a functor satisfying
that property preserves embedding-projection pairs; in categories with split
idempotents the converse holds, too [3, Obs. 6.6.5].

We close this section with a proposition on locally monotone functors which
gives a version of a result for $\omega$-cpo-enriched categories proved by
Freyd [12] for locally continuous functors. He used Kleene’s Theorem in lieu
of Pataraia’s.

######  Proposition 5.5.

Let $\mathscr{A}$ be a $\mathsf{DCPO}_{\bot}$-enriched category. If a locally
monotone functor $F$ has an initial algebra $(\mu F,\iota)$, then $(\mu
F,\iota^{-1})$ is a terminal coalgebra.

We shall see in the proof that it is enough to assume that composition is
left-strict: $\bot\cdot f=\bot$ holds for every morphism $f$ of $\mathscr{A}$
(but $f\cdot\bot=\bot$ in (4) need not hold). This holds in categories
typically used in semantics of programming languages, such as the category of
dcpos with bottom and (non-strict) continuous maps, where composition is not
(right-) strict.

######  Proof 5.6.

Let $\iota\colon FI\to I$ be an initial algebra. For every coalgebra
$\alpha\colon A\to FA$, we prove that a unique homomorphism into
$(I,\iota^{-1})$ exists.

  1. 1.

Existence. The endomap $g$ on $\mathscr{A}(A,I)$ given by $h\mapsto\iota\cdot
Fh\cdot\alpha$ is monotone since $F$ is locally monotone. Hence, it has a
least fixed point $h\colon A\to I$ with $\iota^{-1}\cdot h=Fh\cdot\alpha$ by
Pataraia’s Theorem 2.5. This is a coalgebra homomorphism.

  2. 2.

Uniqueness. First notice that for $\mathscr{A}(I,I)$ we have an the analogous
endomap $f$ given by $k\mapsto\iota\cdot Fk\cdot\iota^{-1}$. Since $I$ is
initial, the only fixed point of $f$ is $k=\operatorname{\mathsf{id}}_{I}$.
Thus $\operatorname{\mathsf{id}}_{I}=\mu f$. Now suppose that
$h^{\prime}\colon(A,\alpha)\to(I,\iota^{-1})$ is any coalgebra homomorphism.
We know that
$\mathscr{A}(h^{\prime},I)\colon\mathscr{A}(I,I)\to\mathscr{A}(A,I)$ is a
strict continuous map; strictness follows from left-strictness of composition:
$\bot_{I,I}\cdot h^{\prime}=\bot_{A,I}$. We now show that
$g\cdot\mathscr{A}(h^{\prime},I)=\mathscr{A}(h^{\prime},I)\cdot f$. Indeed,
unfolding the definitions, we have for every $k\colon I\to I$:

$\displaystyle g\cdot\mathscr{A}(h^{\prime},I)(k)$ $\displaystyle=g(k\cdot
h^{\prime})=\iota\cdot F(k\cdot h^{\prime})\cdot\alpha=\iota\cdot Fk\cdot
Fh^{\prime}\cdot\alpha=\iota\cdot Fk\cdot\iota^{-1}\cdot h^{\prime}$
$\displaystyle=f(k)\cdot h^{\prime}=\mathscr{A}(h^{\prime},I)(f(k)).$

Therefore, by 2.10, $\mathscr{A}(h^{\prime},I)(\mu f)=\mu g$, which means that
$h^{\prime}=\operatorname{\mathsf{id}}_{I}\cdot h^{\prime}=h$.

We leave as an open problem to find an endofunctor on $\mathsf{DCPO}_{\bot}$
which has a fixed point but not an initial algebra.

##  6 The Initial-Algebra Chain

The proof of Theorem 4.1, relying on Pataraia’s Theorem 2.5, is constructive.
However, if one admits non-constructive reasoning and ordinals, then we can
add another equivalent characterization to 4.3 in terms of the convergence of
the initial-algebra chain, which we now recall.

######  Remark 11.

  1. 1.

Recall that an ordinal $i$ is the (linearly ordered) set of all ordinals
smaller than $i$. As such it is also a category.

  2. 2.

By an _$i$ -chain_ in a category $\mathscr{C}$ is meant a functor $C\colon
i\to\mathscr{C}$. It consists of objects $C_{j}$ for all ordinals $j<i$ and
(connecting) morphisms $c_{j,j^{\prime}}\colon C_{j}\to C_{j^{\prime}}$ for
all pairs $j\leq j^{\prime}<i$. Analogously, an _$\mathsf{Ord}$ -chain_ in
$\mathscr{C}$ is a functor from the totally ordered class $\mathsf{Ord}$ of
all ordinals to $\mathscr{C}$. In both cases we will speak of a (transfinite)
_chain_ whenever confusion is unlikely.

  3. 3.

A category $\mathscr{C}$ _has colimits of chains_ if for every ordinal $i$ a
colimit of every $i$-chain exists in $\mathscr{C}$. (This does _not_ include
$\mathsf{Ord}$-chains.) In particular, $\mathscr{C}$ has an initial object
since the ordinal $0$ is the empty set.

######  Definition 12 ([1]).

Let $\mathscr{A}$ be a category with colimits of chains. For an endofunctor
$F$ we define the _initial-algebra chain_ $W\colon\mathsf{Ord}\to\mathscr{A}$.
Its objects are denoted by $W_{i}$ and its connecting morphisms by
$w_{ij}\colon W_{i}\to W_{j}$, $i\leq j\in\mathsf{Ord}$. They are defined by
transfinite recursion as follows

$\begin{array}[]{@{}l}W_{0}=0,\quad\text{$W_{j+1}=FW_{j}$ for all ordinals
$j$},\quad\text{$\textstyle W_{j}=\mathop{\mathsf{colim}}_{i<j}W_{i}$ for all
limit ordinals $j$},\\\ \text{$w_{0,1}\colon 0\to W_{1}$ is unique},\qquad
w_{j+1,k+1}=Fw_{j,k}\colon FW_{j}\to FW_{k},\\\ \text{$w_{i,j}$ ($i<j$) is the
colimit cocone for limit ordinals $j$}\end{array}$

######  Remark 13.

  1. 1.

There exists, up to natural isomorphism, precisely one $\mathsf{Ord}$-chain
satisfying the above equations. For example, $w_{\omega,\omega+1}\colon
W_{\omega}\to FW_{\omega}$ is determined by the universal property of
$W_{\omega}=\mathop{\mathsf{colim}}_{n<\omega}W_{n}=\mathop{\mathsf{colim}}_{n<\omega}W_{n+1}$
as the unique morphism with $w_{\omega,\omega+1}\cdot
w_{n+1,\omega}=w_{n+1,\omega+1}=Fw_{n,\omega}$ for every $n<\omega$.

  2. 2.

Every algebra $\alpha\colon FA\to A$ induces a canonical cocone
$\alpha_{i}\colon W_{i}\to A$ ($i\in\mathsf{Ord}$) on the initial-algebra
chain; it is the unique cocone with
$\alpha_{i+1}=(W_{i+1}=FW_{i}\xrightarrow{\leavevmode\nobreak\
F\alpha_{i}\leavevmode\nobreak\ }FA\xrightarrow{\leavevmode\nobreak\
\alpha\leavevmode\nobreak\ }A)$ for all ordinals $i$. This is easy to see
using transfinite induction.

######  Definition 14.

We say that the initial-algebra chain of a functor $F$ _converges in $\lambda$
steps_ if $w_{\lambda,\lambda+1}$ is an isomorphism, and we simply say that it
_converges_ , if it converges in $\lambda$ steps for some ordinal $\lambda$.

If $w_{i,i+1}$ is an isomorphism, then so is $w_{i,j}$, for all $j>\lambda$.
This is easy to prove by transfinite induction.

Convergence of the initial-algebra chain yields an initial algebra [1]. We
obtain this as a consequence of results from subsection 2.2 on recursive
coalgebras:

######  Theorem 6.1.

Let $\mathscr{A}$ be a category with colimits of chains. If the initial-
algebra chain of an endofunctor $F$ converges in $\lambda$ steps, then
$W_{\lambda}$ is the initial algebra with the algebra structure
$w^{-1}_{\lambda,\lambda+1}\colon FW_{\lambda}\to W_{\lambda}.$

######  Proof 6.2.

An easy transfinite induction shows that every coalgebra $w_{i,i+1}\colon
W_{i}\to FW_{i}$ is recursive: the coalgebra $0\to F0$ is trivially recursive,
for the isolated step use 2.12, and 2.17 yields the limit step. If
$w_{\lambda,\lambda+1}$ is an isomorphism, then
$(W_{\lambda},w_{\lambda,\lambda+1}^{-1})$ is the initial algebra by 4.

The existence of an $\mathcal{M}$-pre-fixed point implies that the initial-
algebra chain converges. The proof below is somewhat similar to the proof of
Theorem 4.1. The difference is that one only uses the recursive coalgebras
$W_{i}\to FW_{i}$ in the initial-algebra chain and applies Zermelo’s Theorem
2.1 in lieu of Pataraia’s Theorem. For this we work again under section 4.

######  Theorem 6.3.

Let $F$ preserve $\mathcal{M}$ and $m\colon FA\rightarrowtail A$ be an
$\mathcal{M}$-pre-fixed point. If $A$ has smooth $\mathcal{M}$-subobjects,
then the initial-algebra chain for $F$ converges.

######  Proof 6.4.

Again, we use the monotone endomap
$f\colon\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)\to\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$
in (3). Theorem 2.1 applies since
$\operatorname{\mathsf{Sub}}_{\mathcal{M}}(A)$ is a dcpo by assumption, and
therefore it is a chain-complete poset. Thus, $f$ has the least fixed point
$\mu f=f^{i}(\bot)$ for some ordinal $i$. The cocone $m_{j}\colon W_{j}\to A$
of 13.2 satisfies $m_{j}=f^{j}(\bot)$ for all $j\in\mathsf{Ord}$. This is
easily verified by transfinite induction. Hence, from
$f(f^{i}(\bot))=f^{i}(\bot)$ we conclude that $m_{i}$ and $m_{i+1}$ represent
the same subobject of $A$. Since $m_{i}=m_{i+1}\cdot w_{i,i+1}$, it follows
that $w_{i,i+1}$ is invertible, which means that the initial-algebra chain
converges.

We now obtain the original initial-algebra theorem by Trnková et al. [28]:

######  Corollary 6.5.

Let $\mathscr{A}$ be a category with colimits of chains and with a smooth
class $\mathcal{M}$ of monomorphisms. Then the following are equivalent for an
endofunctor $F$ preserving $\mathcal{M}$:

  1. 1.

the initial-algebra chain converges,

  2. 2.

an initial algebra exists,

  3. 3.

a fixed point exists,

  4. 4.

an $\mathcal{M}$-pre-fixed point exists.

Moreover, if these hold, then $\mu F$ is an $\mathcal{M}$-subalgebra of every
$\mathcal{M}$-pre-fixed point of $F$.

Indeed, 4 implies 1 by Theorem 6.3, and 1 implies 2 is shown as in Theorem
6.1. The remaining implications are as for 4.3.

######  Remark 15.

Note that in lieu of assuming that $\mathscr{A}$ has colimits of _all_ chains,
it suffices that the initial-algebra chain exists (i.e. the colimits in 12
exist). This weaker condition enables more applications, e.g. the category of
relations with $\mathcal{M}$ the class of injective maps and functors $F$
which are lifted from $\mathsf{Set}$.

######  Remark 16.

For a set functor $F$ no side condition is needed: if $F$ has a pre-fixed
point, then it has an initial algebra. This is clear if
$F\emptyset=\emptyset$. If not, there is a set functor $G$ with
$G\emptyset\neq\emptyset$ which preserves monomorphisms and agrees with $F$ on
all nonempty sets and maps [29]. Since every pre-fixed point of $F$ must be
nonempty, it is also a pre-fixed point of $G$. Hence $G$ has an initial
algebra, which clearly is an initial algebra for $F$, too.

######  Corollary 6.6.

An endofunctor on one of the categories $\mathsf{Set}$, $\mathsf{Pfn}$, or
$K\text{-}\mathsf{Vec}$ has an initial algebra iff it has a pre-fixed point.

######  Proof 6.7.

For $\mathsf{Set}$, use 16. For $\mathsf{Pfn}$ and $K\text{-}\mathsf{Vec}$,
apply 6.5 with $\mathcal{M}$ the class of all monomorphisms (which are split
and therefore preserved by every endofunctor).

## References

  * [1] Jiří Adámek.  Free algebras and automata realizations in the language of categories.  Comment. Math. Univ. Carolin., 15:589–602, 1974.
  * [2] Jiří Adámek, Stefan Milius, and Lawrence S. Moss.  On well-founded and recursive coalgebras.  In Barbara König and Jean Goubault-Larrecq, editors, Proc. Foundations of Software Science and Computation Structures (FoSSaCS), volume 12077 of Lecture Notes Comput. Sci. (ARCoSS), pages 17–36. Springer, 2020.
  * [3] Jiří Adámek, Stefan Milius, and Lawrence S. Moss.  Initial algebras, terminal coalgebras, and the theory of fixed points of functors.  draft book, available at https://www8.cs.fau.de/ext/milius/publications/files/CoalgebraBook.pdf, 2021\.
  * [4] Jiří Adámek and Jiří Rosický.  Locally Presentable and Accessible Categories.  Cambridge University Press, 1994.
  * [5] Andrej Bauer and Peter Lefanu Lumsdane.  On the Bourbaki-Witt principle in toposes.  Math. Structures Comput. Sci., 155(1):87–99, 2013.
  * [6] Nicolas Bourbaki.  Sur le théorème de Zorn.  Arch. Math., 2:434–437, 1949.
  * [7] Georg Cantor.  Über eine elementare frage der Mannigfaltigkeitslehre.  Jahresbericht der Deutschen Mathematiker-Vereinigung, 1:75–78, 1891\.
  * [8] Venanzio Capretta, Tarmo Uustalu, and Varmo Vene.  Recursive coalgebras from comonads.  Inform. and Comput., 204:437–468, 2006.
  * [9] France Dacar.  The join-induction principle for closure operators on dcpos.  Available from http://dis.ijs.si/France/, January 2009.
  * [10] Adam Eppendahl.  Coalgebra-to-algebra morphisms.  In Proc. Category Theory and Computer Science (CTCS), volume 29 of Electron. Notes Theor. Comput. Sci., pages 42–49, 1999.
  * [11] Martín Escardó.  Joins in the complete Heyting algebra of nuclei.  Appl. Categ. Structures, 11:117–124, 2003.
  * [12] Peter Freyd.  Remarks on algebraically compact categories.  In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of category theory in computer science: Proceedings of the London Mathematical Society Symposium, Durham 1991, volume 177 of London Mathematical Society Lecture Note Series, pages 95–106. Cambridge University Press, 1992.
  * [13] Jean Goubault-Larrecq.  Bourbaki, Witt, and Dito Pataraia.  available at https://projects.lsv.ens-cachan.fr/topology/?page_id=176, June 2021.
  * [14] Friedrich Hartogs.  Über das Problem der Wohlordnung.  Math. Ann., 76(4):438–443, 1915.
  * [15] Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva.  Well-founded coalgebras, revisited.  Math. Structures Comput. Sci., 27:1111–1131, 2017.
  * [16] Bronislav Knaster.  Un theéorème sur les fonctions d’ensembles.  Ann. Soc. Pol. Math., 6:133–134, 1928.
  * [17] Joachim Lambek.  A fixpoint theorem for complete categories.  Math. Z., 103:151–161, 1968.
  * [18] George Markowsky.  Chain-complete posets and directed sets with applications.  Algebra Universalis, 6(1):53–68, 1976.
  * [19] Keye Martin.  Nothing can be fixed.  In Computation, logic, games, and quantum foundations, volume 7860 of Lecture Notes in Comput. Sci., pages 195–196. Springer, Heidelberg, 2013.
  * [20] G. Osius.  Categorical set theory: a characterization of the category of sets.  J. Pure Appl. Algebra, 4(79–119), 1974.
  * [21] Dito Pataraia.  A constructive proof of Tarski’s fixed-point theorem for dcpo’s.  Presented at the 65th Peripatetic Seminar on Sheaves and Logic, Aarhus, November 1997.
  * [22] Andrew M. Pitts and S. C. Steenkamp.  Constructing initial algebras using inflationary iteration, 2021.  arXiv:2105.03252.
  * [23] M. B. Smyth and G. D. Plotkin.  The category-theoretic solution of recursive domain equations.  SIAM J. Comput., 11(4):761–783, 1982.
  * [24] Alfred Tarski.  A lattice-theoretical fixpoint theorem and its applications.  Pacific J. Math., 5(2):285–309, 1955.
  * [25] Paul Taylor.  Towards a unified treatment of induction I: the general recursion theorem.  preprint, available at www.paultaylor.eu/ordinals/#towuti, 1995–6.
  * [26] Paul Taylor.  Practical Foundations of Mathematics.  Cambridge University Press, 1999.
  * [27] Paul Taylor.  Well founded coalgebras and recursion.  available at https://www.paultaylor.eu/ordinals/welfcr.pdf, April 2021.
  * [28] V. Trnková, J. Adámek, V. Koubek, and J. Reiterman.  Free algebras, input processes and free monads.  Comment. Math. Univ. Carolin., 16:339–351, 1975.
  * [29] Věra Trnková.  On a descriptive classification of set functors I.  Comment. Math. Univ. Carolin., 12:143–174, 1971.
  * [30] Ernst Witt.  Beweisstudien zum Satz von M. Zorn.  Math. Nachr., 4:434–438, 1951.
  * [31] Ernst Zermelo.  Beweis, daß jede Menge wohlgeordnet werden kann.  Math. Ann., 59:514–516, 1904.

##  Appendix A Further Technical Details

###  A.1 Details for 3.3

######  Lemma A.1.

Monomorphisms are smooth in $\mathsf{MS}$.

######  Proof A.2.

Fix a space $(A,d)$, and consider a directed set $D$ of subobjects
$m_{i}\colon(A_{i},d_{i})\rightarrowtail(A,d)$ ($i\in D$) with monomorphisms
$a_{i,j}\colon A_{i}\rightarrowtail A_{j}$ witnessing $i\leq j$ in $D$. Let
$B=\bigcup_{i\in D}m_{i}[A_{i}]$, and let $d^{\prime}\colon B\to[0,1]$ be
defined as follows:

$d^{\prime}(x,y)=\inf\\{d_{i}(x^{\prime},y^{\prime}):\text{$i\in
D,x^{\prime},y^{\prime}\in A_{i}$, $m_{i}(x^{\prime})=x$ and
$m_{i}(y^{\prime})=y$}\\}.$ (6)

We show that $d^{\prime}$ is a metric. It is clearly symmetric and fulfils
$D^{\prime}(x,x)=0$. We verify that distinct points $x,y$ in $B$ have non-zero
distance. For each $i$, $x^{\prime}$, and $y^{\prime}$ as in (6),
$d_{i}(x^{\prime},y^{\prime})\geq d(x,y)$, since $m_{i}$ is non-expanding.
Thus $d^{\prime}(x,y)\geq d(x,y)>0$.

Finally, we verify that $d^{\prime}$ satisfies the triangle inequality. To
this end it suffices to show that for all $x,y,z\in B$ and every
$\varepsilon>0$ we have $d^{\prime}(x,z)\leq
d^{\prime}(x,y)+d^{\prime}(y,z)+\varepsilon$.

Let $x,y,z\in B$ and fix $\varepsilon>0$. We can choose $i$, $x^{\prime}$,
$y^{\prime}$ as in (6) such that
$d_{i}(x^{\prime},y^{\prime})<d^{\prime}(x,y)+\varepsilon/2$. Analogously, let
$j$, $y^{\prime\prime}$, $z^{\prime\prime}$ be such that
$d_{j}(y^{\prime\prime},z^{\prime\prime})<d^{\prime}(x,y)+\varepsilon/2$.
Since the collection $m_{i}[A_{i}]$ is directed, we can assume $i\leq j$ in
$D$. Using that the connecting map $a_{i,j}$ is non-expanding we obtain
$d_{j}(a_{i,j}(x^{\prime}),a_{i,j}(y^{\prime}))<d^{\prime}(x,y)+\varepsilon/2$.
Since $m_{j}$ is injective, $a_{i,j}(y^{\prime})=y^{\prime\prime}$. Let
$x^{\prime\prime}=a_{i,j}(x^{\prime})$, and note that
$m_{j}(x^{\prime\prime})=x$. By the triangle inequality in $A_{j}$,

$d_{j}(x^{\prime\prime},z^{\prime\prime})\leq
d_{j}(x^{\prime\prime},y^{\prime\prime})+d_{j}(y^{\prime\prime},z^{\prime\prime})<d^{\prime}(x,y)+d^{\prime}(y,z)+\varepsilon.$

It follows that $d^{\prime}(x,z)\leq
d^{\prime}(x,y)+d^{\prime}(y,z)+\varepsilon$, as desired.

It is obvious that the inclusion $m\colon B\rightarrowtail A$ is non-
expanding. It is also easy to check that $(B,d^{\prime})$ is the join in
$\operatorname{\mathsf{Sub}}(A,d)$ of the directed diagram corresponding to
given directed set $D$.

Finally, for every $i\in D$, we have the codomain restriction
$m_{i}^{\prime}\colon A_{i}\rightarrowtail B$ of $m_{i}$, which is non-
expanding. We verify that the family of all $m^{\prime}_{i}$ ($i\in D$) forms
a colimit cocone. It clearly is a cocone. Consider any cocone
$f_{i}\colon(A_{i},d_{i})\to(A^{*},d^{*})$, $i\in D$. Clearly, the union $B$
is the colimit in $\mathsf{Set}$. Therefore, we have a unique map $f\colon
B\to A^{*}$ such that $f_{i}=f\cdot m_{i}^{\prime}$ for all $i\in D$. This is
given by $f(x)=f_{i}(x)$ whenever $x\in m_{i}[A_{i}]$. We check that $f$ is
non-expanding, and this will conclude our verification. Let $x,y\in B$, and
choose $i,x^{\prime},y^{\prime}$ as in (6). Since $f_{i}$ is non-expanding,

$d^{*}(f(x),f(y))=d^{*}(f_{i}(x^{\prime}),f_{i}(y^{\prime}))\leq
d_{i}(x^{\prime},y^{\prime})\leq d^{\prime}(x,y).$

######  Lemma A.3.

Strong monomorphisms are smooth in $\mathsf{CMS}$.

######  Proof A.4.

Fix a complete metric space $(A,d)$, and consider a directed set $D$ of closed
subspaces $A_{i}\hookrightarrow A$. Their join $B\hookrightarrow A$ is the
closure of their union

$B=\overline{\bigcup_{i<\lambda}A_{i}}.$

We know from A.1 that the union is the colimit of the directed diagram
corresponding to $D$ in $\mathsf{MS}$. Moreover, the colimit of a diagram in
$\mathsf{CMS}$ is given by forming the Cauchy completion of the colimit of
that diagram in $\mathsf{MS}$. (This follows from the fact that $\mathsf{CMS}$
is a reflective subcategory of $\mathsf{MS}$ with Cauchy completions as
reflections.) Since $B$ is complete and $\bigcup_{i\in D}A_{i}$ is dense in
it, $B$ is the Cauchy completion of that union, whence it is desired colimit
in $\mathsf{CMS}$.

###  A.2 Proof of Theorem 5.1

######  Proof A.5.

1 $\Rightarrow$ 2: Let $D$ have objects $D_{i}$ and connecting morphisms
$e_{i,j}\colon D_{i}\to D_{j}$. Write $\widehat{e}_{i,j}$ for the projection
of $e_{i,j}$. We verify that for $i\leq j\leq k$,
$\widehat{e}_{i,k}=\widehat{e}_{i,j}\cdot e_{j,k}$. In fact,
$\widehat{e}_{i,j}$ is unique with $\widehat{e}_{i,j}\cdot
e_{i,j}=\operatorname{\mathsf{id}}_{D_{i}}$ and
$e_{i,j}\cdot\widehat{e}_{i,j}\sqsubseteq\operatorname{\mathsf{id}}_{D_{j}}$.
But $\widehat{e}_{i,k}\cdot e_{j,k}$ also has these properties, since

$\begin{aligned} (\widehat{e}_{i,k}\cdot e_{j,k})\cdot
e_{i,j}&=\widehat{e}_{i,k}\cdot e_{i,k}\\\
&=\operatorname{\mathsf{id}}_{D_{i}},\end{aligned}\quad\qquad\text{and}\quad\qquad\begin{aligned}
e_{i,j}\cdot(\widehat{e}_{i,k}\cdot
e_{j,k})&=e_{i,j}\cdot\widehat{e}_{i,j}\cdot\widehat{e}_{j,k}\cdot e_{j,k}\\\
&=e_{i,j}\cdot\widehat{e}_{i,j}\cdot\operatorname{\mathsf{id}}_{D_{k}}\\\
&\sqsubseteq\operatorname{\mathsf{id}}_{D_{k}}.\end{aligned}$

This shows that indeed $\widehat{e}_{i,k}=\widehat{e}_{i,j}\cdot e_{j,k}$ for
$i\leq j\leq k$.

For each $i$ form the subdiagram $D^{i}$ of all $D_{j}$ for $j\geq i$, with
connecting maps $e_{j,k}$ for $i\leq j\leq k$ inherited from $D$. Since $I$ is
directed, the colimit of $D^{i}$ is $(c_{j})_{j\geq i}$. Our observation at
the outset shows that we have a cocone of $D^{i}$:

$\widehat{e}_{i,j}=\big{(}D_{j}\xrightarrow{\leavevmode\nobreak\
e_{j,k}\leavevmode\nobreak\ }D_{k}\xrightarrow{\leavevmode\nobreak\
\hat{e}_{i,k}\leavevmode\nobreak\ }D_{i}\big{)}.$

Thus, there is a unique factorization $\widehat{c}_{i}\colon C\to D_{i}$
through the colimit cocone:

$\widehat{e}_{i,j}=\widehat{c}_{i}\cdot c_{j}\quad\text{for $j\geq i$}.$ (6)

In particular, for $i=j$, we see that $\widehat{c}_{i}\cdot
c_{i}=\operatorname{\mathsf{id}}_{D_{i}}$. We will verify below the equation
$\bigsqcup_{j}c_{j}\cdot\widehat{c}_{j}=\operatorname{\mathsf{id}}_{C}$, and
this of course implies that
$c_{i}\cdot\widehat{c}_{i}\sqsubseteq\operatorname{\mathsf{id}}_{C}$. (This
justifies our use of the projection notation $\widehat{c}_{j}$ and shows the
first point in Item 2, that $c_{i}$ is an embedding.)

Next, we show that for each $j$, the morphisms $\widehat{c}_{i}$ for $i\leq j$
form a cone of $D^{j}$:

$\widehat{c}_{i}=\big{(}C\xrightarrow{\leavevmode\nobreak\
\hat{c}_{j}\leavevmode\nobreak\ }D_{j}\xrightarrow{\leavevmode\nobreak\
\hat{e}_{i,j}\leavevmode\nobreak\ }D_{i}\big{)}.$

Indeed, the colimit cocone $(c_{k})_{k\geq j}$ is collectively epic, so we
need only establish this after precomposing with each $c_{k}$. We apply (6)
twice to obtain: $\widehat{c}_{i}\cdot
c_{k}=\widehat{e}_{i,k}=\widehat{e}_{i,j}\cdot\widehat{e}_{j,k}=\widehat{e}_{i,j}\cdot\widehat{c}_{j}\cdot
c_{k}.$

We are ready to argue for 2. The maps $c_{i}\cdot\widehat{c}_{i}$ form a
directed subset of $\mathscr{A}(C,C)$ because for $i\leq
j$,$c_{i}\cdot\widehat{c}_{i}=(c_{j}\cdot
e_{i,j})\cdot(\widehat{e}_{i,j}\cdot\widehat{c}_{j})\sqsubseteq
c_{j}\cdot\widehat{c}_{j}.$ Thus, $\bigsqcup_{j}c_{j}\cdot\widehat{c}_{j}$
exists. We use that the family $(c_{i})$ is collectively epic, and verify that
$\textstyle\bigsqcup_{j}c_{j}\cdot\widehat{c}_{j}\cdot c_{i}=c_{i}\text{ for
every $i$}.$ Fix $i$, and consider the join above. Since it is over a directed
set, we need only consider $\bigsqcup_{j\geq i}c_{j}\cdot\widehat{c}_{j}\cdot
c_{i}$. In addition, for $j\geq i$ we obtain $c_{j}\cdot\widehat{c}_{j}\cdot
c_{i}=c_{j}\cdot\widehat{c}_{j}\cdot(c_{j}\cdot e_{i,j})=c_{j}\cdot
e_{i,j}=c_{i}.$

2 $\Rightarrow$ 1: Let $(b_{i}\colon D_{i}\to B)$ be a cocone. For all $i\leq
j$ we have $b_{i}=b_{j}\cdot e_{i,j}$. We also have a cocone $(c_{i})$, and so
$c_{i}=c_{j}\cdot e_{i,j}$, and thus
$\widehat{c}_{i}=\widehat{e}_{i,j}\cdot\widehat{c}_{j}$. From this we have

$b_{i}\cdot\widehat{c}_{i}=(b_{j}\cdot
e_{i,j})\cdot(\widehat{e}_{i,j}\cdot\widehat{c}_{j})\sqsubseteq b_{j}\cdot
e_{j}.$

Thus, the following join exists in $\mathscr{A}(C,B)$: $\textstyle
b=\bigsqcup_{j}b_{j}\cdot\widehat{c}_{j}.$ To prove that $b_{i}=b\cdot c_{i}$
for all $i$, we fix one $i$ and consider the join above with $j\geq i$:

$b_{j}\cdot\widehat{c}_{j}\cdot
c_{i}=(b_{j}\cdot\widehat{c}_{j})\cdot(c_{j}\cdot e_{i,j})=b_{j}\cdot
e_{i,j}=b_{i}.$

Thus $b\cdot c_{i}=\bigsqcup_{j\geq i}(b_{j}\cdot\widehat{c}_{j}\cdot
c_{i})=\bigsqcup_{j\geq i}b_{i}=b_{i}.$ This shows that $b$ is the desired
factorization of $(b_{i})$. For its uniqueness, let $b^{\prime}\colon C\to B$
be a morphism with $b^{\prime}\cdot c_{i}=b_{i}$ for all $i$. Since
$\bigsqcup_{i}c_{i}\cdot\widehat{c}_{i}=\operatorname{\mathsf{id}}_{C}$, we
have $\textstyle
b^{\prime}=b^{\prime}\cdot\big{(}\bigsqcup_{i}c_{i}\cdot\widehat{c}_{i}\big{)}=\bigsqcup_{i}b^{\prime}\cdot
c_{i}\cdot\widehat{c}_{i}=\bigsqcup_{i}b_{i}\cdot\widehat{c}_{i}=b.$ This
completes the proof.

###  A.3 Proof of Theorem 5.2

######  Proof A.6.

We use 3.4. Fix an object $A$ in $\mathscr{A}$. Let $\mathcal{E}$ be the class
of embeddings, so that $\operatorname{\mathsf{Sub}}_{\mathcal{E}}(A)$ denotes
the poset of subobjects of $A$ represented by embeddings. Let $D$ be a
directed diagram of monomorphisms in $\mathscr{A}$, not necessarily
embeddings, and let $m_{i}\colon A_{i}\rightarrowtail A$, $i\in D$, be a
cocone of morphisms in $\operatorname{\mathsf{Sub}}_{\mathcal{E}}(A)$. By
hypothesis, $D$ has a colimit cocone, say $c_{i}\colon A_{i}\to B$. We have a
unique morphism $m\colon B\to A$ such that for all $i$, $m_{i}=m\cdot c_{i}$.
Our task is to show that $m$ is an embedding, and that $m=\bigsqcup_{i\in
A}m_{i}$ in $\operatorname{\mathsf{Sub}}_{\mathcal{E}}(A)$.

For $i\leq j$ in $A$, we have a morphism $e_{i,j}$ such that $m_{i}=m_{j}\cdot
e_{i,j}$. Let us verify that $e_{i,j}$ is an embedding and that
$\widehat{e}_{i,j}=\widehat{m}_{i}\cdot m_{j}$. To see this, we use the
characterization of projections. First, $(\widehat{m}_{i}\cdot m_{j})\cdot
e_{i,j}=\widehat{m}_{i}\cdot m_{i}=\operatorname{\mathsf{id}}$. Second, we
verify $e_{i,j}\cdot(\widehat{m}_{i}\cdot
m_{j})\sqsubseteq\operatorname{\mathsf{id}}$:

$\displaystyle e_{i,j}\cdot(\widehat{m}_{i}\cdot m_{j})$
$\displaystyle=(\widehat{m}_{j}\cdot m_{j})\cdot
e_{i,j}\cdot\widehat{m}_{i}\cdot m_{j}$ since $\widehat{m}_{j}\cdot
m_{j}=\operatorname{\mathsf{id}}$ $\displaystyle=\widehat{m}_{j}\cdot
m_{i}\cdot\widehat{m}_{i}\cdot m_{j}$ since $m_{i}=e_{i,j}\cdot m_{j}$
$\displaystyle\sqsubseteq\widehat{m}_{j}\cdot m_{j}$ since
$m_{i}\cdot\widehat{m}_{i}=\operatorname{\mathsf{id}}$
$\displaystyle=\operatorname{\mathsf{id}}.$

We next show that for $i\leq j$, $c_{i}\cdot\widehat{m}_{i}\sqsubseteq
c_{j}\cdot\widehat{m}_{j}$. Once this is done, we put
$\widehat{m}=\bigsqcup_{i}c_{i}\cdot\widehat{m}_{i}$ and show that it is a
projection for $m$. We thus calculate:

$\displaystyle c_{i}\cdot\widehat{m}_{i}$ $\displaystyle=c_{j}\cdot
e_{i,j}\cdot\widehat{m}_{i}$ $\displaystyle=c_{j}\cdot
e_{i,j}\cdot\\!\\!\widehat{\leavevmode\nobreak\ m_{j}\cdot e_{i,j}}$
$\displaystyle=c_{j}\cdot e_{i,j}\cdot\widehat{e}_{i,j}\cdot\widehat{m}_{j}$
$\displaystyle\sqsubseteq c_{j}\cdot\widehat{m}_{j}$

To prove that $\widehat{m}\cdot m=\operatorname{\mathsf{id}}$, we use that the
family $(c_{i})$ is collectively epic. Thus, we show that for all $i$,
$\widehat{m}\cdot m\cdot c_{i}=c_{i}$. We again consider $\bigsqcup_{j\geq
i}c_{j}$ only:

$\displaystyle\textstyle\widehat{m}\cdot m\cdot c_{i}$
$\displaystyle\textstyle=\big{(}\bigsqcup_{j\geq
i}c_{j}\cdot\widehat{m}_{j}\big{)}\cdot m\cdot c_{i}$
$\displaystyle\textstyle=\bigsqcup_{j\geq i}c_{j}\cdot\widehat{m}_{j}\cdot
m_{i}$ $\displaystyle\textstyle=\bigsqcup_{j\geq
i}c_{j}\cdot\widehat{m}_{j}\cdot m_{j}\cdot e_{i,j}$
$\displaystyle\textstyle=\bigsqcup_{j\geq i}c_{j}\cdot e_{i,j}$
$\displaystyle\textstyle=\bigsqcup_{j\geq i}c_{i}$ $\displaystyle=c_{i}.$

In the other direction, we show that
$m\cdot\widehat{m}\sqsubseteq\operatorname{\mathsf{id}}$:

$\textstyle
m\cdot\big{(}\bigsqcup_{i}c_{i}\cdot\widehat{m}_{i}\big{)}=\bigsqcup_{i}m\cdot
c_{i}\cdot\widehat{m}_{i}=\bigsqcup_{i}m_{i}\cdot\widehat{m}_{i}\sqsubseteq\operatorname{\mathsf{id}}.$

Our last order of business is to show that $m=\bigsqcup_{i\in A}m_{i}$ in
$\operatorname{\mathsf{Sub}}_{\mathcal{E}}(A)$. Since $m\cdot c_{i}=m_{i}$, we
see that $m_{i}\sqsubseteq m$ for all $i$. Let $u\colon U\rightarrowtail A$ be
an embedding with $m_{i}\sqsubseteq u$ for all $i$. Thus we have morphisms
$u_{i}$ such that $m_{i}=u\cdot u_{i}$. The family $(u_{i})_{i}$ is a cocone
of the original diagram $D$, because if $i\leq j$, then

$u_{j}\cdot e_{i,j}=(\widehat{u}\cdot u)\cdot u_{j}\cdot
e_{i,j}=\widehat{u}\cdot m_{j}\cdot e_{i,j}=\widehat{u}\cdot
m_{i}=\widehat{u}\cdot u\cdot u_{i}=u_{i}.$

Since $(c_{i})$ is a colimit, there is a unique $f\colon M\to U$ such that
$u_{i}=f\cdot c_{i}$ for all $i$. We aim to show that $m=u\cdot f$, so that
$m\sqsubseteq u$. For this, we again use the fact that $(c_{i})$ is a
collectively epic family: $m\cdot c_{i}=m_{i}=u\cdot u_{i}=u\cdot f\cdot
c_{i}$.