= Split-coequalizer lifting for a fixed-point-domain operation
{title2=$\beta_Q(z)=q\beta_B(sz)$}
In the <nested partial unary operation category>, suppose the lower-operation diagram $A\rightrightarrows B\xrightarrow{q}Q$ has a <split coequalizer> with $qs=1$, $ft=1$ and $gt=sq$. The section $s$ takes eligible <fixed points> to eligible fixed points, so the displayed next operation is defined on exactly the required domain. For eligible $x\in B$, the equations give
$$
q\beta_B(x)=qf\beta_A(tx)=qg\beta_A(tx)=q\beta_B(sqx).
$$
Thus $q$ preserves the next operation. Every factored <morphism> preserves it by evaluating at $sz$, giving creation of the specified <coequalizer>. Together with reflection of <isomorphisms>, the <Beck monadicity theorem> proves one-step monadicity.
Back to article page
