nLab successor monad

The Successor Monad

The successor monad is an example of a monad on Set. For $X$ a set, we define $S X$ as a disjoint union of $S$ and a singleton set $1$. Given a function $f\colon X \to Y$, we have $S f\colon S X \to S Y$ as

$$\begin {matrix} S f(x) \coloneqq f(x) & x\colon X ;\\ S f({*}) \coloneqq * & *\colon 1 \end {matrix}$$

In material set theory (with the axiom of foundation), it is handy to define this as $S X \coloneq X \cup \{X\}$; then for $f\colon X \to Y$,

$$S f(x) \coloneqq \left\{ \begin{matrix} f(x) & x \in X \\ Y & x = X \end{matrix} \right .$$

The structure map $\eta_X$ is the inclusion of $X$ in $S X$; the map $\mu_X\colon S S X \to S X$ restricts to $S X$ as the identity, and futhermore has as image $\mu_X(S X) = X$.

The hom-set of morphisms in the Kleisli category of $(S,\eta,\mu)$ from $X$ to $Y$ is canonically equivalent (using excluded middle) to the set of partial functions from $X$ to $Y$; its Eilenberg–Moore category is equivalent to the category of pointed sets and pointed function?s, i.e. functions of the form $1 \to X$ and commuting squares between such functions.

The successor monad as defined here is also interesting in that it stabilizes the finite von Neumann ordinals and monotone maps between them, and that $\eta$ and $\mu$ are also monotone. Thus the successor monad restricts as a monad to the augmented simplex category (this is the opposite of the Décalage comonad). Furthermore, every monotone map of finite ordinals can be written as a composite of arrows of the form $S^k \mu_l$ and $S^m \eta_n$. Indeed, the monoidal category $\Delta_a$ is generated by the monoid object $0 \overset{\iota_0}\rightarrow 1 \overset{\mu_0}\leftarrow 2$.

JCMcKeown: I want to say something like $(S,\eta,\mu)$ generates the (skeletal augmented) simplex category; there is surely a right way to say that, but what is it?

Toby: I don't think that it's quite true that $S$ generates the simplex category, because you need an object to start applying it to. But I'd agree that $(S,\eta,\mu)$ generates it starting from $0$. I don't know any slick way to say that.

I've put in a suggestion by Finn above. How's that?