nLab comonadic functor

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 $L\dashv R$ of adjoint functors, $L\colon A \to B\colon R$, with counit $\epsilon$ and unit $\eta$, one forms a comonad $\mathbf{\Omega} = (\Omega, \delta, \epsilon)$ by $\Omega \coloneqq L \circ R$, $\delta \coloneqq L \eta R$. $\mathbf{\Omega}$-comodules (aka $\mathbf{\Omega}$-coalgebras) form a category $B_{\mathbf{\Omega}}$ and there is a natural comparison functor $K = K_{\mathbf{\Omega}}\colon A \to B_{\mathbf{\Omega}}$ given by $A \mapsto (L A, L A \stackrel{L(\eta_A)}\to L R L A)$.

A functor $L\colon A\to B$ is comonadic if it has a right adjoint $R$ and the corresponding comparison functor $K$ is an equivalence of categories. The adjunction $L \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, \rho)$,

manifestly exhibits a split equalizer sequence.

…

Examples

Comonadic adjoints to monadic functors

If $T: Set \to Set$ is a monad on $Set$, with corresponding monadic functor $U: Set^T \to Set$, then the left adjoint $F: Set \to Set^T$ is comonadic provided that the unique algebra map $!: F(0) \to F(1)$ is a regular monomorphism and not an isomorphism. In particular, if $T$ 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)$ is nonempty, then $!: F(0) \to F(1)$ is a split monomorphism since any constant $c: 1 \to F(0)$ induces an algebra map $F(1) \to F(0)$ that retracts $!$; on the other hand there is more than one algebra map $F(1) \to M$ if $M$ has more than one element, so $F(1)$ isn’t itself initial).

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

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

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

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

$$W^{\ast} (P) = P \times W \to W$$

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

$$\prod_W (Q) = \Gamma_W(Q)$$

(space of sections).

Hence the composite, a kind of necessity operator

$$\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 $Q \to W$ to $\Gamma_W(Q) \times W \to W$.

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

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

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

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

The equalizer of these two maps is formed from the $f$ for which $g = h$ for all $w, w'$ in $W$, that is, when $f$ is constant. So the equalizer is equivalent to $W^{\ast} P = P \times W \to W$.

Related concepts

• monadic functor, comonadic functor

• monadicity theorem