An object of is a set with a finite list of partial unary operations. The first is total; the domain of each later operation consists exactly of the defined fixed points of the immediately preceding operation. Morphisms preserve every defined operation. Take to be the Category of sets. This tower gives examples of arbitrary finite monadic length even though its long free–forgetful composites induce the same first monad.
For an object of the nested partial unary operation category , adjoining the next operation freely gives one new value at each defined fixed point of the previous operation. Each new value starts an infinite free chain under the first unary operation; the other old operations are undefined on those new points. The new top operation consequently has no fixed points, so subsequent free extensions add no points. This gives a left adjoint to forgetting the last operation; extensions of maps along the chains are forced by the first target operation.
In the nested partial unary operation category, suppose the lower-operation diagram has a split coequalizer with , and . The section takes eligible fixed points to eligible fixed points, so the displayed next operation is defined on exactly the required domain. For eligible , the equations giveThus preserves the next operation. Every factored morphism preserves it by evaluating at , giving creation of the specified coequalizer. Together with reflection of isomorphisms, the Beck monadicity theorem proves one-step monadicity.
Articles by others on the same topic
There are currently no matching articles.