# 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 withing $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 $\mathit{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?

-
Do you have any assumptions on $F$? It would help if we knew that $A \subseteq B$ implies $F(A) \subseteq F(B)$, i.e., does $F$ preserve monos? Perhaps it preserves finite limits (which then implies that it preserves monos)? – Andrej Bauer Sep 8 '10 at 8:34
Functors are so-called Kripke polynomial functors, and thus preserve pullbacks. – Dave Clarke Sep 8 '10 at 8:48

Suppose that the functor $F$ preserves monos. In fact, I am going to assume something slightly stronger, namely that $S \subseteq T$ implies $F(S) \subseteq F(T)$ (otherwise we have to insert isomorphisms here and there). Your Kripke functors are of this kind, I think.
First a little diversion. Let $G$ be a functor from sets to sets which preserves the subset relation. Consider a coalgebra $s : S \to G(S)$ and a subset $A \subseteq S$. Call a subset $T \subseteq S$ "good" if the restriction $s_T : T \to G(S)$ of $s$ to $T$ gives a coalgebra $s_T : T \to G(T)$ and the image $s(T)$ is disjoint from $A$. Any union of good subsets is again a good subset. Indeed, suppose $T_i$'s are good and let $T = \bigcup_i T_i$. Then $s$ restricted to $T$ maps into $\bigcup_i G(T_i) \subseteq G(T)$, and obviously $T$ is disjoint from $A$. Therefore, there exists the largest good subset of $T$, namely the union of all the good ones.
Now apply the previous paragraph to the functor $G(X) = F(X) + 1$ and $A = \lbrace \mathrm{inr}()\rbrace$ to get the desired result.