Take a category $\mathcal{C}$ with a monad $T$ and construct the the Eilenberg-Moore category $\mathcal{C}^T$, the adjunction that arises is the terminal splitting of the monad $M$. Denote the resulting comonad on $\mathcal{C}^T$ as $S$, one can now construct its co-Eilenberg-Moore category $(\mathcal{C}^T)^{S}$ and there is a unique functor $L:\mathcal{C} \to (\mathcal{C}^T)^{S}$.
This seems to be a fairly canonical construction that somebody must have looked at before. I'm particularly interested in the case where $\mathcal{C}$ is locally presentable and the monad is accessible - it follows that case that $\mathcal{C}^{TS}$ is presentable and $L$ is accessible.
