# Maximal subcoalgebras of an $F+1$-coalgebra corresponding to an $F$-coalgebra

This context of this question is Rutten's Universal Coalgebra, used for modelling systems. I'm interested in finding a description of a functor between different types of coalgebras corresponding to finding a certain subcoalgebra.

An $F+1$-coalgebra $\langle S,\alpha:S\to F(S)+1\rangle$ can be thought of as a system whose transition shape is given by functor F plus the possibility of an error/termination, given by the +1. Assume that $F$ is a so-called Kripke polynomial functor: $F::=Id ~|~ B ~|~ F+F ~|~ F\times F ~|~ F^ A ~|~ \mathcal{P}_\omega F$, thus it preserves pullbacks.

A subcoalgebra of $\langle S,\alpha:S\to F(S)+1\rangle$ is coalgebra $\langle S',\alpha':S'\to F(S')+1\rangle$, where $S'\subseteq S$ and $\alpha'$ is $\alpha'$ restricted to $S'$, such that its range falls within $F(S')+1$.

I want to find the maximal subcoalgebra of this coalgebra which corresponds to an $F$-coalgebra. In terms of my application, this means I'm looking for the subset of states $S'\subseteq S$ that do not lead to the error state.

Clearly, I can take the pullback of the functions $\alpha:S\to F(S)+1$ and $inl:F(S)\to F(S)+1$ to get a set $S_0\subseteq S$ which do not lead to an error in the first step. Iterating this process for functors $F^i+1$ seems to lead to progressively smaller subsets $S_i$ of $S$ each avoiding the error state for $i$ steps. What I'm lacking is a coherent description of the process.

Is whether there is a more universal description of this construction in terms of limits or colimits, or at least, some known approaches to the problem?

I asked this question on the computer science theory overflow (here), but am re-asking it here as I received no feedback.

-
Incidentally, do you mean that Kripke polynomial functors are finitary, i.e. preserve filtered colimits, rather than preserving pullbacks? $\newcommand{\Pw}{\mathcal{P}_\omega} \Pw$ doesn't preserve pullbacks, if I'm not mistaken: the map $\Pw(2 \times_1 2) \rightarrow \Pw(2) \times_{\Pw(1)} \Pw(2)$ isn't injective, since $\{(x,y),(x',y')\}$ and $\{(x,y'),(x',y)\}$ both get sent to $(\{x,x'\},\{y,y'\})$. –  Peter LeFanu Lumsdaine Sep 8 '10 at 14:42

## 1 Answer

I think the construction you're looking for can be seen as a right adjoint, and hence the details of the construction can be seen as coming from general transfinite constructions of adjoints.


Now, if I'm understanding right, the construction you're looking at, the "error-free core" of an $F+1$ coalgebra, is the right adjoint to this.

Moreover, I think there should be theorems that show automagically why this can be computed by the construction you give, as an $\omega$-long limit of pullbacks — but I'm not sure exactly where, I'm afraid. It's almost certainly deducible from the Kelly "Unified treatment of transfinite constructions" paper, well-described by Tom Leinster here; the constructions of that have a very similar flavour.

Possibly relevant well-known constructions to compare (in Kelly and elsewhere): the construction of an algebraically-(co)free (co)monad on an endofunctor; the construction of the free $T$-algebra on a $T$-graph; the free $S$-algebra on a $T$-algebra, given a monad map $S \to T$.

-
That seems to be just what the doctor ordered. –  supercooldave Sep 14 '10 at 4:49
Great! One other thing I should probably have mentioned, actually: the (proofs of the) adjoint functor theorems (well-expounded in eg Mac Lane) also give explicit constructions for adjoints, under reasonable conditions; but they give an "all-at-once" (co)limit rather than a transfinite sequence, so aren't as closely related to the construction you give as the others I mentioned might be. –  Peter LeFanu Lumsdaine Sep 14 '10 at 14:44