Regarding a difficulty in the Fakir article about associated idempotent triple

Question

I just had post this question in SE: https://math.stackexchange.com/questions/518054/about-details-of-the-fakir-theorem-proof-associated-idempotent-triple but dont get any answer.

I understand that at the first sight it seems a silly/trivial verifications (to me too) but I discussed the matter with some known person (PhD) and my doubt seems to be well founded.

On the ncatlab work http://ncatlab.org/toddtrimble/published/Associated+idempotent+monad+of+a+monad Todd Trimbe quote the Fakir theorem in [1] about the associated idempotent triple:

Let $(T, \eta , \mu)$ a triple on a complete category $\mathscr{C}$

in his article [1] Fakir claim to define a triple $(T', \eta', \mu')$ as follow: let $T'$ the Kernel: $T' \xrightarrow{k_X} T \rightrightarrows T \circ T$ where the couple is given by $\eta T$ and $T\eta $. From $\eta T \ast \eta = T\eta \ast \eta $ (apply $\eta$ to $\eta_X$) follow $\eta': 1 \Rightarrow T'$ with $\eta_X= k_X\circ \eta'_X $. We observe that:

1) $\mu_X \circ T(\eta_X)= 1_{T(X)}$ and then $\mu_X\circ T(k_X)\circ T(\eta'_X)=1$ .

For obtain $\mu': T'T' \Rightarrow T'$ we consider that $T'T'(X)$ is defined as the follow Kernel:

$T'(T'(X)) \xrightarrow{k_{T'(X)}} T(T'(X)) \rightrightarrows (T \circ T)(T'(X))$ where the couple is given by $\eta_{TT'X}$ and $T(\eta_{T'X}) $.

In the article [1] Fakir claim to obtain a morphism $\mu': T'T'(X) \to T(X)$ from the universal property of kernel, assuming (implicitly) that $\mu_X\circ T(k_X)\circ k_{T'X}$ equalize the couple $\eta_{TX},\ T\eta_X: T(X) \to T T(X)$, observe that from (1) $\mu_X\circ T(k_X)$ cannot equalize this couple.

Then I consider the diagram

$$\begin{array}{ccccc} T'T'X & \xrightarrow{k_{T'X}} & TT'X & \xrightarrow[T\eta_{T'X}]{\eta_{TT'X}} & TTT'X \\ && T(k_X)\downarrow && \downarrow TT(k_X)\\ & & TTX & \xrightarrow[T\eta_{TX}]{\eta_{TTX}} & TTTX \\ && \mu_X\downarrow && \downarrow f\\ & & TX & \xrightarrow[T\eta_X]{\eta_{TX}} & TTX \\ \end{array}$$

If this is (mutually) commutative we are done. The top square is mutually commutative, but the below isn't if we put $f=T\mu$ or $f=\mu_T$.

How can we prove the existence of $\mu'$?.

I wish a proof in term of natural transformation, seems that in terms of string diagrams the things work well, but I dont know how translate in "classical" terms.

Biblio:

[1] Fakir, Monade idempotente associee a une monade, C. R. Acad. Sci. Paris Ser. A 270 (1970), 99-101

Answer 1

Yes, we first want to show that the composites of those squares are serially commutative, taking $f = T\mu$. In other words (let me drop the $X$; it plays no role) that

• $\eta T \circ \mu \circ Tk = T\mu \circ TTk \circ \eta TT'$, and

• $T\eta \circ \mu \circ Tk = T\mu \circ TTk \circ T\eta T'$.

Now the first of these is trivial because it's just an instance of a naturality square for $\eta$. For the second, notice that both sides of the asserted equation are $T$-algebra maps. To check the equality of $T$-algebra maps $\phi, \psi$ when their common domain is a free $T$-algebra $T T'$, it suffices to show that $\phi \circ \eta T' = \psi \circ \eta T'$ (this is the universal property of free algebras).

So we have to check that

• $T\eta \circ \mu \circ Tk \circ \eta T' = T\mu \circ TTk \circ T\eta T' \circ \eta T'$.

The left side is $T\eta \circ \mu \circ \eta T \circ k$ (by $\eta$-naturality), and reduces to $T\eta \circ k$ since $\mu \circ \eta T$ is an identity morphism.

The right side is $T\mu \circ TTk \circ \eta TT' \circ \eta T'$ (by $\eta$-naturality), and we apply $\eta$-naturality a few more times:

$$\begin{array} T\mu \circ TTk \circ \eta TT' \circ \eta T' & = & T\mu \circ \eta TT \circ Tk \circ \eta T' \\ & = & T\mu \circ \eta TT \circ \eta T \circ k \\ & = & \eta T \circ \mu \circ \eta T \circ k \end{array}$$

and this reduces to $\eta T \circ k$ since $\mu \circ \eta T$ is an identity.

So after the reductions, it boils down to the equality $T\eta \circ k = \eta T \circ k$, which is true since $k$ is the equalizer of $T\eta, \eta T$.

---

It should be obvious to Buschi Sergio that this is enough, but for anyone else reading out there: the required map $\mu': T'T' \to T'$ is defined to be the unique morphism such that $\mu \circ Tk \circ kT' = k \circ \mu'$, where the existence of $\mu'$ would follow (since $k$ is the equalizer of $T\eta, \eta T$) from the fact that

$$T\eta \circ \mu \circ Tk \circ kT' = \eta T \circ \mu \circ Tk \circ kT'.$$

But the serial commutativity shown above allows us to rewrite this asserted equation as

$$T\mu \circ TTk \circ T\eta T' \circ kT' = T\mu \circ TTk \circ \eta TT' \circ kT'$$

which clearly holds since $kT'$ equalizes $T\eta T', \eta TT'$.