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?

  • $\begingroup$ 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)? $\endgroup$ Sep 8, 2010 at 8:34
  • $\begingroup$ Functors are so-called Kripke polynomial functors, and thus preserve pullbacks. $\endgroup$ Sep 8, 2010 at 8:48

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.