Write and for the unit and counit of an adjunction. The induced monad hasThe Eilenberg-Moore comparison functor sends to the algebra for a monadand sends to . The triangle identities for an adjunction give the algebra unit law, and naturality of the counit gives the algebra multiplication law and the algebra-morphism equation for .
If has coequalizers, define the Left adjoint to the Eilenberg-Moore comparison functor at an algebra byThe parallel pair is reflexive through . A morphism is equivalently an arrow with . Under , its transpose is . The transpose of is , while the transpose of is . Hence the coequalizer condition is exactlythe equation for a morphism of algebras for a monad . This supplies the natural bijection proving , and also defines on algebra morphisms by the coequalizer universal property.
Let forget the last partial unary operation. For an object of the nested partial unary operation category , setThe nesting rule implies that every earlier operation is defined and fixes such an . To construct a free extension of nested partial unary operations, adjoin a disjoint infinite chain for each :Keep the old operations on . On each new chain put ; every old operation with is undefined there, because the first operation has no fixed points there. Define the new operation only on , by . These are exactly the fixed points of the old top operation, so the required domain rule is satisfied. The inclusion preserves all old defined operations.
For a morphism , preservation of the old operations makes whenever . Any extension to a morphism must haveThe operation is defined at , and is total, so this formula exists. It preserves the new operation and the chain operation; there are no other defined operations on new points to check. It therefore gives the unique extension. Naturality and functoriality follow from uniqueness. ThusNotice the useful extra fact: the new top operation has no fixed points, since every value is new and every input is old. Hence freely adding any further operations adds no more points; those operations have empty domains.
Put . The initial free construction sends to with . A function extends uniquely by . Its induced monad is , with unit and multiplication . An algebra for a monad is determined by the action of , so its Eilenberg-Moore category is . Thus this first free–forgetful adjunction is a monadic adjunction without needing the given assumption for .
The monadic length counts successive Eilenberg-Moore comparison functor steps until the comparison becomes an equivalence. Fix . For , the free construction in the preceding part adds the st operation with no fixed points. For , the free first operation also has no fixed points. Consequently the left adjoint to the composite forgetful functor is obtained by the one-step free construction, followed by empty higher operations. In particular, its underlying object of , unit and multiplication are exactly those of the one-step adjunction:as monads, not merely as object functions. The multiplication agrees because both counits evaluate the same first new operation and the same chains; no later operation has a value on a free object.
By the assumed one-step monadic adjunction property, or the explicit argument above when , the Eilenberg-Moore category is equivalent to . Under this equivalence the comparison is precisely . Indeed, its algebra action evaluates each newly adjoined chain using , and evaluates the first new value using ; it retains that operation and ignores all higher ones. The comparison has a left adjoint by the same explicit free extension. Thus the whole monadic tower for nested partial unary operations iswith the remaining comparison at stage equal to , and stage the identity.
It does not terminate earlier. If , take the same underlying two-element set in two objects of , making every operation up to the identity. In the first object make all remaining operations identities; in the second make exchange the two elements, and leave all subsequent operations undefined. Both satisfy the nesting rule. The identity function is a morphism after forgetting to , but is not a morphism between the original objects. Thus is not a full functor, and cannot be an equivalence. Therefore
Articles by others on the same topic
There are currently no matching articles.