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.


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


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'$.

  • $\begingroup$ You're welcome; please call me Todd. On another note: I notice that you are not in the habit of officially accepting answers: meta.stackexchange.com/questions/5234/… Accepting answers is optional, but the reasons behind it are given in the linked post, and it's good practice to indicate to the community that a question has been resolved to the poster's satisfaction. (Also, questions without accepted answers are periodically recycled to the front page, e.g.: mathoverflow.net/questions/130667/… .) $\endgroup$ – Todd Trimble Nov 9 '13 at 16:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.