The notion of a comonadic functor is the dual of that of a monadic functor. See there for more background.
Given a pair of adjoint functors, , with counit and unit , one forms a comonad by , . -comodules (aka -coalgebras) form a category and there is a natural comparison functor given by .
A functor is comonadic if it has a right adjoint and the corresponding comparison functor is an equivalence of categories. The adjunction is said to be a comonadic adjunction.
Beck’s monadicity theorem has its dual, comonadic analogue. To discuss it, observe that for every -comodule ,
manifestly exhibits a split equalizer sequence.
…
If is a monad on , with corresponding monadic functor , then the left adjoint is comonadic provided that the unique algebra map is a regular monomorphism and not an isomorphism. In particular, if is given by an algebraic theory with at least one constant and a model with more than one element, then the left adjoint is comonadic (if the initial algebra is nonempty, then is a split monomorphism since any constant induces an algebra map that retracts ; on the other hand there is more than one algebra map if has more than one element, so isn’t itself initial).
More generally, let be a locally small category with small copowers, and suppose is an object such that is a regular monomorphism but not an isomorphism, then the copowering with ,
(left adjoint to ) is comonadic. See proposition 6.13 and related results in this paper by Mesablishvili.
In the context of the treatment of modal operators given at Possible worlds via first-order logic and type theory, we find that base change along the terminal morphism from the type of worlds, , and its right adjoint, dependent product, form a comonadic adjunction. .
Let be a topos. For a type/object, , in we have that
(projection on the second component). And for in , we have
Hence the composite, a kind of necessity operator
(an analog of the jet comonad), sends to .
If is an inhabited object so that is an epimorphism, then is a conservative functor. Since it moreover preserves all limits (having a further left adjoint, the dependent sum operation) the monadicity theorem applies and says that the coalgebras for this comonad are the types in , or rather the types in which are in the image of , hence of the form , and equipped with the map
over ( denotes the internal hom), where the first component of the map sends to the constant map at .
To see this as an equalizer, consider the two maps from to . Over , these are formed from the two ways of mapping to , by sending in to and to .
The equalizer of these two maps is formed from the for which for all in , that is, when is constant. So the equalizer is equivalent to .
monadic functor, comonadic functor
Last revised on November 6, 2022 at 11:07:33. See the history of this page for a list of all contributions to it.