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.


Comonadic adjoints to monadic functors

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.


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, WW, and its right adjoint, dependent product, form a comonadic adjunction. W * WW^{\ast} \dashv \prod_W.

Let H\mathbf{H} be a topos. For a type/object, PP, in HH /*\mathbf{H} \simeq \mathbf{H}_{/\ast} we have that

W *(P)=P×WW W^{\ast} (P) = P \times W \to W

(projection on the second component). And for [QW][Q \to W] in H /W\mathbf{H}_{/W}, we have

W(Q)=Γ W(Q) \prod_W (Q) = \Gamma_W(Q)

(space of sections).

Hence the composite, a kind of necessity operator

W:H /W WHW *H /W \Box_W \colon \mathbf{H}_{/W}\stackrel{\prod_W}{\longrightarrow} \mathbf{H} \stackrel{W^\ast}{\longrightarrow} \mathbf{H}_{/W}

(an analog of the jet comonad), sends QWQ \to W to Γ W(Q)×WW\Gamma_W(Q) \times W \to W.

If WW is an inhabited object so that W*W \to \ast is an epimorphism, then W *W^\ast 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 H\mathbf{H}, or rather the types in H /W\mathbf{H}_{/W} which are in the image of W *W^{\ast}, hence of the form P×WP \times W, and equipped with the map

(const,id):P×W W(P×W)P W×W (const, id) \;\colon\; P \times W \longrightarrow \Box_W (P \times W) \simeq P^W \times W

over WW (P WP^W denotes the internal hom), where the first component of the map sends p:Pp: P to the constant map at pp.

To see this as an equalizer, consider the two maps from W(P×WW)\Box_W (P \times W \to W) to W W(P×WW)\Box_W \Box_W (P \times W \to W). Over WW, these are formed from the two ways of mapping P WP^W to P (W×W)P^{(W \times W)}, by sending ff in P WP^W to g:(w,w)f(w)g \colon (w, w') \mapsto f(w) and to h:(w,w)f(w)h \colon (w, w') \mapsto f(w').

The equalizer of these two maps is formed from the ff for which g=hg = h for all w,ww, w' in WW, that is, when ff is constant. So the equalizer is equivalent to W *P=P×WWW^{\ast} P = P \times W \to W.

Revised on September 17, 2015 03:25:38 by David Corfield (