nLab comonadic functor

Redirected from "comonadicity theorem".
Contents

Contents

Idea

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

Definition

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.

Properties

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.

Examples

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 the unique algebra map !:F(0)F(1)!: 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 and a model with more than one element, then the left adjoint is comonadic (if the initial algebra F(0)F(0) is nonempty, then !:F(0)F(1)!: F(0) \to F(1) is a split monomorphism since any constant c:1F(0)c: 1 \to F(0) induces an algebra map F(1)F(0)F(1) \to F(0) that retracts !!; on the other hand there is more than one algebra map F(1)MF(1) \to M if MM has more than one element, so F(1)F(1) isn’t itself initial).

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.

Necessity

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.

Last revised on November 6, 2022 at 11:07:33. See the history of this page for a list of all contributions to it.