What's the final coalgebra of $F(S) = 1 + N \times S$ and initial algebra of $F(S) = N \times S$

Question

There are 4 algebras in my mind and they make me very confusion.

I will list 2 (co)algebras which I can understand, and then list other 2 (co)algebras that I can not fully undertand.

• Given the functor $F(S) = 1 + \mathbb N \times S$, the initial algebra of $F$ should be $(List \ \mathbb N, fix)$, where

fix : 1 + N x List N -> List N
fix * = []
fix (n, nx) = [n] ++ nx

• Given the functor $F(S) = \mathbb N \times S$, the final coalgebra of F should be $(Stream \ \mathbb N, unfix)$, where

 unfix : Stream N -> N x Stream N
 unfix s = (head(s), rest(s))

I can understand the these two (co)algebras above, but following two (co)algebras make me very confusion...

• Given the functor $F(S) = 1 + \mathbb N \times S$, what is the final coalgebra of $F$?

  The carry object of this final coalgebra is $List \ \mathbb N$ or $Stream \ \mathbb N$?

  What is the struct map of this final coalgebra ?

• Given the functor $F(S) = \mathbb N \times S$, what is the initial algebra of $F$?

  The carry object of this initial algebra is $\emptyset$ or $Stream \ \mathbb N$?

  What is the struct map of this initial coalgebra ?

The last question is what is the relationship among these 4 algebras and the induction /coinduction types and greatest/least fixed points of $F$?

---

Edit for adding more information.

1. All $F$ appeared in the quesion are endofunctor $F : Set \to Set$.
2. All $\mathbb N$ appeared in the quesion are $Nat$ set.
3. $List \ \mathbb N$ means finite list of $\mathbb N$, $Stream \ \mathbb N$ means infinite stream of $\mathbb N$.
4. The functor $F(S) = 1 + \mathbb N \times S$, when it map morphism $f : S \to S'$

fmap : S -> S' -> 1 + N × S -> 1 + N × S'
fmap f * = *
fmap f (n, s) = (n, f s)

5. The functor $F(S)= \mathbb N ×S$, when it map morphism $f : S \to S'$

fmap : S -> S' -> N × S -> N × S'
fmap f (n, s) = (n, f s)

Answer 1

Partial answer. I can't help you with the induction/coinduction types and greatest/least fixed points questions. I'm not sure what you mean by them.

The initial algebra of $F(S)=\newcommand\N{\Bbb{N}}\N\times S$ is definitely $\varnothing$. Since $F(\varnothing)=\varnothing$, we have a unique possible structure map $\varnothing \to \varnothing$, and since $\varnothing$ is initial in $\mathbf{Set}$, this is definitely the initial algebra.

The more interesting question is what is the final coalgebra (if it exists) for $F(S)= 1+\N\times S$. By definition, this would be a set $S$ with map $\alpha : S\to F(S)$ such that for any other coalgebra $(T,\beta)$ there is a unique map $f:T\to S$ such that the square $$ \require{AMScd} \begin{CD} T@>\beta>> F(T) \\ @VfVV @VVF(f)V \\ S @>\alpha>> F(S) \\ \end{CD} $$ commutes.

Let's think about the meaning of a coalgebra for this functor for a moment. It means that for each $t\in T$, we produce either $*$ or a pair $(n,t')$. In other words, for each $t$ we can produce a stream of natural numbers that might be finite if at some point we reach $*$ or go on forever. Thus suggests that we should take $$S=\operatorname{List}(\N)\cup \operatorname{Stream}(\N)$$ in your notation. We should define $\alpha(\epsilon)=*$, where $\epsilon$ is the empty list and $\alpha(n_1n_2\cdots) = (n_1,n_2\cdots)$.

Then for any coalgebra $(T,\beta)$ we define $f$ recursively by $$ f(t)=\begin{cases} \epsilon & \beta(t)=* \\ nf(t') & \beta(t)=(n,t'). \end{cases} $$

You can check that this makes the diagram commute and is the unique map doing so.

Answer 2

Just to complete @jgon's answer, which did provide the initial algebra / final co-algebra that you were looking for.

Such initial algebras are (no matter the functor, as long as they exist) fixed points of $F$. To prove that, take $(A, s)$ an initial $F$-algebra, and consider $(F(A), F(s))$. By initiality, there is a unique map $s': A \to F(A)$ such that $$ \require{AMScd} \begin{CD} F(A) @> s >> A\\ @V F(s') VV @VV s' V\\ F(F(A)) @> F(s) >> F(A) \end{CD} $$ commutes. But then, $$ \require{AMScd} \begin{CD} F(A) @> F(s') >> F(F(A)) @> F(s) >> F(A)\\ @V s VV @V F(s) VV @V s VV\\ F @> s' >> F(S') @> s >> A \end{CD} $$ commutes, that is, $s\circ s'$ is an algebra map $(A, s) \to (A, s)$. So is the identity (F-algebra with their map form a category), so by unicity $s\circ s'=\mathrm{Id}$. The other direction is easy: $s' \circ s = F(s) \circ F(s') = F(s\circ s')=F(\mathrm{Id})=\mathrm{Id}$.

This means that $s$ is an isomorphism between $F(A)$ and $A$, which means $A$ is a fixed point (up-to-isomorphism) of $F$. The same goes for final co-algebras. Since initial algebras (resp. final co-algebras) are, in some way, the smallest algebras (resp. the biggest one), they are called least/greatest fixpoints of $F$.