Proof

Let $\theta_X: X \to P X$ and $\theta_Y: Y \to P Y$ be the coalgebra structures. Given a commutative square

we must show that the top arrow factors through $i: U \to X$. Since $i: U \to X$ is formed by pulling back $j: V \to Y$ along $f: X \to Y$, it suffices to produce a map $H \to V$ that fits into a commutative square

Gluing together the commutative squares

and using the fact that $f$ is a coalgebra map, we may form a map from $H$ to the pullback $J$ of $\theta_Y$ and $P j$:

and now using the fact that $j: V \to Y$ is an inductive subobject, the map $J \to Y$ factors as a map $k: J \to V$ followed by $j: V \to Y$. The map $H \to J$ followed by $k: J \to V$ gives us the desired $H \to V$.

Proof

We must prove that any inductive subobject $i: U \to P W$ is the entirety of $P W$. The map $\theta$ is a coalgebra map, so by lemma , the map $j: J \to W$ formed by the pullback

is an inductive subobject. Since $W$ is well-founded, $j$ is an isomorphism. Applying $P$ to this pullback, we have a commutative square

but because $i: U \to P W$ is inductive, the map $P j: P J \to P W$ factors through $i: U \to P W$. Since $P j$ is an iso, $i$ is forced to be a monic retraction, and thus an iso itself, as was to be proved.

Proof

Notice that the underlying functor $Coalg_P \to C$ preserves and reflects colimits. Let $W = colim_\alpha W_\alpha$ be such a colimit, and let $i: U \to W$ be an inductive subobject. The pullbacks $i_\alpha: U_\alpha \to W_\alpha$ along the coalgebra maps $W_\alpha \to W$ are again inductive subobjects, and thus isomorphisms since the $W_\alpha$ are well-founded. We have $U = colim_\alpha U_\alpha$ since colimits are stable under pullback (by local cartesian closure), and the induced comparison map $i: U \to W$ between colimits in $C$ is an isomorphism since the $i_\alpha$ are. Thus $W$ is well-founded.

Proof

Under the colimit conditions on $C$, we may form unions of subobjects, and so subobject lattices are small and small-cocomplete. By lemma , the union $W$ of all well-founded subcoalgebras of $X$ is again a well-founded coalgebra; it is thus the maximal well-founded subcoalgebra. We claim this is the initial $P$-algebra.

Indeed, by theorem , it suffices to show that the coalgebra structure $\eta: W \to P W$ is an isomorphism. From the diagram

we see $\eta$ is monic. The map $P i$ is also monic since $P$ preserves monos. From lemma , the subcoalgebra $P W$ is well-founded. It therefore contains and is contained in the maximal $W$, so that $\eta$ is an isomorphism, as desired.

Proof

In the first place, $C$ is complete. For that, it suffices to show it has all small products (since it is already finitely complete and thus has equalizers).

Let $B_i$ be a collection of objects of $C$ indexed over a set $I$. Since $C$ has small coproducts by asumption, we have a map in $C$,

where $\Delta I = \sum_{i \in I} 1$, and where $p$ sends the summand $B_i$ to $i$ (the $i^{th}$ copy of $1$). Then

is the product, where $!$ is the unique map $\Delta I \to 1$. Indeed, maps $X \to \Pi_! p$ are in natural bijection with maps $!^\ast X \to p$ in $E/\Delta(I) \simeq E^I$ (this equivalence holds by infinite extensivity), i.e., with an $I$-indexed family of maps $X \to B_i$, as required.

Now let $f: B \to A$ be a morphism of $C$, and $P_f$ the associated polynomial endofunctor. Since $C$ is complete, we may form the limit of the countable chain

Moreover, $P_f$ preserves this limit because (a) this is a connected limit, and (b) the functors $B^\ast$, $\Pi_f$, and $\Sigma_A$ all preserve connected limits. It follows from Adámek’s theorem that the limit $X$, with coalgebra structure $X \to P_f X$ the isomorphism that obtains by the limit preservation by $P_f$, is a terminal coalgebra.

It now follows from theorem that there is an initial algebra $W(f)$ for $P_f$. This completes the proof.