comonadic functor



The notion of a comonadic functor is the dual of that of a monadic functor. See there for more background.


Given a pair LRL\dashv R of adjoint functors, L:AB:RL\colon A \to B\colon R, with counit ϵ\epsilon and unit η\eta, one forms a comonad Ω=(Ω,δ,ϵ)\mathbf{\Omega} = (\Omega, \delta, \epsilon) by ΩLR\Omega \coloneqq L \circ R, δLηR\delta \coloneqq L \eta R. Ω\mathbf{\Omega}-comodules (aka Ω\mathbf{\Omega}-coalgebras) form a category B ΩB_{\mathbf{\Omega}} and there is a natural comparison functor K=K Ω:AB ΩK = K_{\mathbf{\Omega}}\colon A \to B_{\mathbf{\Omega}} given by A(LA,LAL(η A)LRLA)A \mapsto (L A, L A \stackrel{L(\eta_A)}\to L R L A).

A functor L:ABL\colon A\to B is comonadic if it has a right adjoint RR and the corresponding comparison functor KK is an equivalence of categories. The adjunction LRL \dashv R is said to be a comonadic adjunction.


Beck’s monadicity theorem has its dual, comonadic analogue. To discuss it, observe that for every Ω\Omega-comodule (N,ρ)(N, \rho),

Layer 1 N ρ Q * Q * N Q * η Q * N Q * Q * ρ Q * Q * Q * Q * N N\xrightarrow[\rho]{\qquad}Q^Q_ N\underoverset{\; Q^* \eta_{Q_N}\quad}{\;Q^ Q_* \rho\quad}{\rightrightarrows}Q^* Q_Q^ Q_* N ϵ Q * Q * N \epsilon_{Q^* Q_* N} ϵ N \epsilon_{N}

manifestly exhibits a split equalizer sequence.


If T:SetSetT: Set \to Set is a monad on SetSet, with corresponding monadic functor U:Set TSetU: Set^T \to Set, then the left adjoint F:SetSet TF: Set \to Set^T is comonadic provided that F(!):F(0)F(1)F(!): F(0) \to F(1) is a regular monomorphism and not an isomorphism. In particular, if TT is given by an algebraic theory with at least one constant symbol and at least one function symbol of arity greater than zero, then the left adjoint is comonadic (because then F(!):F(0)F(1)F(!): F(0) \to F(1) is a split monomorphism but not an isomorphism).

More generally, let AA be a locally small category with small copowers, and suppose aa is an object such that 0a0 \to a is a regular monomorphism but not an isomorphism, then the copowering with aa,

a:SetA- \cdot a: Set \to A

(left adjoint to A(a,):ASetA(a, -): A \to Set) is comonadic. See proposition 6.13 and related results in this paper by Mesablishvili.

Revised on July 12, 2014 04:24:20 by Todd Trimble (