<p>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.</p>

<p>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.</p>

<p>Now apply the previous paragraph to the functor $G(X) = F(X) + 1$ and $A = \lbrace \mathrm{inr}()\rbrace$ to get the desired result.</p>

CC BY-SA 2.5
2010-09-08T11:07:12.043Z
2010-09-08T20:43:53.330Z
2010-09-08T20:43:53.330Z
Andrej Bauer
<p>This context of this question is Rutten's <em><a href="http://en.wikipedia.org/wiki/F-coalgebra" rel="nofollow">Universal Coalgebra</a></em>, 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.</p>

<p>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.</p>

<p>A <em>subcoalgebra</em> 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$.</p>

<p>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. </p>

<p>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.</p>

<p>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?</p>

CC BY-SA 2.5
2010-09-08T08:34:08.810Z
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
CC BY-SA 2.5
2010-09-08T08:48:21.123Z
Functors are so-called Kripke polynomial functors, and thus preserve pullbacks.
Dave Clarke
<ct.category-theory>
Maximal subcoalgebras of an $F+1$-coalgebra corresponding to an $F$-coalgebra
Dave Clarke
# Maximal subcoalgebras of an $F+1$-coalgebra corresponding to an $F$-coalgebra

(Asked by: username_0 on 2010-09-03)

This context of this question is Rutten's *[Universal Coalgebra](http://en.wikipedia.org/wiki/F-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?

**Tags:** ct.category-theory

> **Comments:**
> **username_1**: 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)?  
> **username_0**: Functors are so-called Kripke polynomial functors, and thus preserve pullbacks.  

---

## 1 answers

### Answer by username_1 on 2010-09-08. Score: 4 | Accepted answer

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.


---

