successor monad

The Successor Monad

The successor monad is an example of a monad on Set. For XX a set, we define SXS X as a disjoint union of SS and a singleton set 11. Given a function f:XYf\colon X \to Y, we have Sf:SXSYS f\colon S X \to S Y as

Sf(x)f(x) x:X; Sf(*)* *:1 \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 SX∶−X{X}S X \coloneq X \cup \{X\}; then for f:XYf\colon X \to Y,

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

The structure map η X\eta_X is the inclusion of XX in SXS X; the map μ X:SSXSX\mu_X\colon S S X \to S X restricts to SXS X as the identity, and futhermore has as image μ X(SX)=X\mu_X(S X) = X.

The hom-set of morphisms in the Kleisli category of (S,η,μ)(S,\eta,\mu) from XX to YY is canonically equivalent (using excluded middle) to the set of partial functions from XX to YY; its Eilenberg–Moore category is equivalent to the category of pointed sets and pointed function?s, i.e. functions of the form 1X1 \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. Furthermore, every monotone map of finite ordinals can be written as a composite of arrows of the form S kμ lS^k \mu_l and S mη nS^m \eta_n. Indeed, the monoidal category Δ a\Delta_a is generated by the monoid object 0ι 01μ 020 \overset{\iota_0}\rightarrow 1 \overset{\mu_0}\leftarrow 2.

JCMcKeown: I want to say something like (S,η,μ)(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 SS generates the simplex category, because you need an object to start applying it to. But I'd agree that (S,η,μ)(S,\eta,\mu) generates it starting from 00. 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 September 16, 2010 at 19:28:34. See the history of this page for a list of all contributions to it.