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?

Last revised on August 31, 2019 at 17:04:30. See the history of this page for a list of all contributions to it.