Let $F\dashv U$ and let $\mathbb T=(T,\eta,U\varepsilon F)$ be the induced monad on $\mathsf C$.
The proof of Beck's monadicity theorem revolves around coequalizers of pairs $$FUFA\substack{Fa\\ \rightrightarrows\\ \varepsilon_{FA}}FA$$ where $UFA\overset{a}{\rightarrow}A$ is a $\mathbb T$-algebra.
I think I morally understand why the existence of such coequalizers is equivalent to the existence of a left adjoint $L$ to the comparison functor $K : \mathsf{D} \to \mathsf{C}^\mathbb{T}$.
However, I do not have any conceptual understanding of the following two implications:
- If $U$ preserves coequalizers of the above pairs, the unit of $L\dashv K$ is an isomorphism.
- If $U$ both preserves and reflects such coequalizers, the counit of $L\dashv K$ is an isomorphism.
I'm thinking of the coequalizer of$$FUFA\substack{Fa\\ \rightrightarrows\\ \varepsilon_{FA}}FA$$ as a "homomorphic quotient". Then, (1) says that a $\mathbb T$-algebra underlies every homomorphic quotient, while (2) says $\mathbb T$-algebras precisely underlie homomorphic quotients. What do these conditions have to do with the unit and counit being isomorphisms?
I'm looking for a conceptual explanation. The formal proof I know is clear to me, but I don't feel I could have guessed the conditions of preserving and reflecting these coequalizers.
In many motivating cases, $F\dashv U : \mathsf{D}\to\mathsf{C}$ will be a free-forgetful adjunction. We can take a universal algebra perspective. In this case $\mathsf{C}$ will traditionally be $\mathbf{Set}$, and $\mathsf{D}$ will be a category of models/algebras/varieties. To specify which category of models we specify a(n algebraic) signature, i.e. a listing of operation symbols and equations between terms built from them. To specify the equations, we need terms. To have something concrete to work with, the signature, $\Sigma$, for semigroups has one operation symbol $\mathtt{m/2}$, the $\mathtt{2}$ indicating the input arity. The set of raw terms built on a set of "variables" $V$, $T_\Sigma(V)$, is inductively defined to be either $\eta(v)$ for $v\in V$, or $o(t_1,\dots,t_n)$ for $t_i \in T_\Sigma(V)$ and $o\mathtt{/}n \in \Sigma$. With raw terms, we can now specify the single equation, which is really just a pair of raw terms, the signature for semigroups specifies: $\mathtt{m}(\mathtt{m}(\eta(x),\eta(y)),\eta(z))=\mathtt{m}(\eta(x),\mathtt{m}(\eta(y),\eta(z)))$ where these are terms in $T_\Sigma(\{x,y,z\})$. A model or $\Sigma$-algebra is a set $S$, called the carrier, and an assignment of a function to each operation symbol with the appropriate arity, e.g. $\mathtt{m/2}$ gets assigned a function $[\![\mathtt{m}]\!] : S^2 \to S$, which we lift to raw terms in the following way: given a set $V$ and a function $\rho : V \to S$, $$[\![t]\!]_\rho = \begin{cases}\rho(v), & t = \eta(v) \\ [\![\mathtt{o}]\!]([\![t_1]\!]_\rho,\dots,[\![t_n]\!]_\rho), & t = \mathtt{o}(t_1,\dots,t_n)\end{cases}$$ The assignment must satisfy the equations in the sense that given a pair of terms $t_l$ and $t_r$ in $T_\Sigma(V)$ representing an equation, for any $\rho : V \to S$, $[\![t_l]\!]_\rho = [\![t_r]\!]_\rho$. Homomorphisms of $\Sigma$-algebras are functions between the carrier sets that preserve the operations in the usual way.
$\Sigma$-algebras and homomorphisms form a category and we have a functor $U : \mathbf{Alg}_\Sigma \to \mathbf{Set}$ taking a $\Sigma$-algebra to its carrier set. This functor has a left adjoint, $F$, which takes a set to the term algebra built on that set. This is a quotient of the set of raw terms by the congruence generated by the equations. In detail, let $t_1 \sim t_2$ iff there's an equation $t_l = t_r$ and $t_1$ matches $t_l$ and $t_2$ matches $t_r$ where $t\in T_\Sigma(U)$ matches $t'\in T_\Sigma(V)$ iff there is a function $\rho : V \to T_\Sigma(U)$ such that $\rho(t') = t$ where $\rho(t)$ is like $[\![t]\!]_\rho$ only with $[\![\mathtt{o}]\!] = \mathtt{o}$. We then lift $\sim$ to a congruence. An assignment is also part of the term algebra, namely $[\![\mathtt{o}]\!]([t_1],\dots,[t_n]) = [\mathtt{o}(t_1,\dots,t_n)]$ where $[t]$ is the equivalence class containing $t$.
Now we have the monad $T = U \circ F$ and we call $TV$ the set of terms built from $V$. The unit, $\eta_V : V\to TV$, injects a "variable" into the set of terms. The counit, $\varepsilon_M : FUM\to M$, satisfies $\varepsilon_M([\eta(m)]) = m$ and $$\varepsilon_M([\mathtt{o}(t_1,\dots,t_n)]) = [\![\mathtt{o}]\!]^M(\varepsilon_M(t_1),\dots,\varepsilon_M(t_n))$$ We can think of $\varepsilon_M$ as "evaluating" the term using the $\Sigma$-algebra, $M$.
We want, as usual for an "algebraic" structure, that every $\Sigma$-algebra can be viewed as a quotient of a free algebra (i.e. the term algebra). Sure enough, $\varepsilon_M$ is a quotient map, and, further, is the coequalizer of $FU\varepsilon_M$ and $\varepsilon_{FUM}$. It's worth looking at this is more detail. I breezily stated it, but could it be that these coequalizers don't exist? How do we normally construct quotients for algebraic objects, for rings say? Well, we simply quotient the underlying set with respect to a congruence, then, by dint of the congruence property, the original operations are well-defined functions on representatives of the equivalence classes. So we have that coequalizers always exist, and the carrier of a quotient is the quotient of the carrier. Or, put another way, $U$ creates coequalizers.
When we look at the Eilenberg-Moore algebras of $T$ in $\mathbf{Set}$, we find that a $T$-algebra $a : TA \to A$ exactly corresponds to $U\varepsilon_M$ for a $\Sigma$-algebra $M$. In detail, $a$ must respect the equations to be a well-defined function of the term algebra, and the $T$-algebra laws correspond to the compositional definition of $\varepsilon_M$, namely with $$[\![\mathtt{o}]\!]^M(x_1,\dots,x_n) = a([\mathtt{o}(\eta(x_1),\dots,\eta(x_n))])$$ It's not hard to then show $\mathbf{Alg}_\Sigma \simeq \mathbf{Set}^T$, and in fact this is an adjoint equivalence. An adjoint equivalence is an adjunction where the unit and counit are isomorphisms.
Using the intuitions from the above, given a $T$-algebra, $(A,a)$, we'd expect to be able to build an object by quotienting a free object, i.e. $FA/{\sim}$, and this quotient should be the coequalizer of $\varepsilon_{FA}$ and $Fa$. We'd also expect $\varepsilon$ to essentially be a quotient map itself. Ultimately, what monadicity is saying is that a map in $\mathsf{D}$ is a map in $\mathsf{C}$ that satisfies some laws. That is, we want to think of an arrow of $\mathsf{D}$ as a map between the underlying "sets". Indeed, the counit of the $L\dashv K$ adjunction being an isomorphism is equivalent to $K$ being fully faithful, i.e. $$\mathsf{D}(M,N)\cong\mathsf{C}^\mathbb{T}((UM,U\varepsilon_M),(UN,U\varepsilon_N))\cong\{f\in\mathsf{C}(UM,UN)\mid f\circ U\varepsilon_M = U\varepsilon_N\circ FUf\}$$ Combining these ideas, a homomorphism, i.e. arrow of $\mathsf{D}$, from a coequalizer $M/{\sim}$ is, as always, an arrow satisfying some (equational) constraints, but an arbitrary homomorphism is itself a "function", i.e. arrow of $\mathsf{C}$, satisfying equational constraints (in the monadic case). Moreover, the equivalence relation induced by the coequalizer of $Uf$ and $Ug$ already includes the constraints necessary for any arrow that coequalizes them to be a homomorphism because $f$ and $g$ are homomorphisms. So, given any parallel pair of homomorphisms $f,g : M\to N$, if a coequalizer $q : UN \to Q$ of $Uf,Ug : UM\to UN$ exists, this should automatically induce a coequalizer $\hat q : N \to \hat Q$ where $U\hat q = q$. That is, $U$ should create coequalizers. (To be precise, some things can go wrong which is why the statement refers to creating coequalizers of $U$-split pairs. A weaker statement that captures the spirit of what I'm saying is a weakening of Duskin's Monadicity Theorem which states that a right adjoint between finitely complete categories is monadic if it creates quotients of congruences. The issue is we need better behaved coequalizers in general, i.e. not every coequalizer corresponds to a quotient.)
It's probably worth mentioning that for any $T$-algebra, $(A, a)$, $A$ is a split coequalizer (via $\eta_A$) of $Ta$ and $\mu_A$. This makes $Fa$ and $\varepsilon_{FA}$ examples of a $U$-split pair. A split coequalizer is an example of an absolute colimit which means it's preserved by all functors. Thus $K\circ F \circ U^\mathbb{T} : \mathsf{C}^\mathbb{T}\to\mathsf{C}^\mathbb{T}$ takes any $T$-algebra to the free $T$-algebra on its carrier which is a split coequalizer as an object of $\mathsf{C}^\mathbb{T}$. Since $U^\mathbb{T} : \mathsf{C}^\mathbb{T}\to\mathsf{C}$ is, of course, monadic, every $T$-algebra is a (not necessarily split) coequalizer in $\mathsf{C}^\mathbb{T}$.