$\DeclareMathOperator\Mod{Mod}\DeclareMathOperator\Ext{Ext}$Let $p$ be a prime. The adjunction
$$\mathbb F_p \otimes_\mathbb{Z} (-) : \Mod(\mathbb Z) \leftrightarrows \Mod(\mathbb F_p) : U $$$$\mathbb F_p \otimes_\mathbb{Z} (-) : \Mod(\mathbb Z) \rightleftarrows \Mod(\mathbb F_p) : U $$
descends (almost tautologically) to an adjunction on the Bousfield localization,
$$\mathbb F_p \otimes_\mathbb{Z} (-) : \Mod(\mathbb Z)^\wedge_p \leftrightarrows \Mod(\mathbb F_p) : U $$$$\mathbb F_p \otimes_\mathbb{Z} (-) : \Mod(\mathbb Z)^\wedge_p \rightleftarrows \Mod(\mathbb F_p) : U $$
I believe this adjunction is comonadic, and I believe this is well-known.
Question 1: What is a reference for the comonadicity of the above adjunction?
Question 2: Are there any examples of folks applying this comonadicity to the study of infinite $p$-complete abelian groups (or — almost equivalently — to infinite abelian $p$-groups)?
Notes:
In Bousfield's language, the statement is that the $\mathbb F_p$-nilpotent completion of a $\mathbb Z$-module always coincides with its $\mathbb F_p$-localization. This is related to saying something about the associated Adams spectral sequence, although I think for general objects of $\Mod(\mathbb Z)^\wedge_p$ there will still be $\varprojlim^1$ issues with the spectral sequence.
It follows, for example, from the main result of Baker–Lazarev that the above adjunction is comonadic at the unit $\mathbb Z_p$ (and hence at any compact object), but I'm not sure about general objects. Also I think the above result should be older.
This doesn't seem to follow from Mathew's theory of descendable adjunctions — $\mathbb Z_p$ is not in the thick subcategory generated by $\mathbb F_p$.
In case it's not obvious: in the above, I take an implicit $\infty$-convention and write $A = HA$ everywhere. $\Mod(R)$ is the stable $\infty$-category / dg-category of chain complexes of $R$-modules localized at quasi-isomorphism. $\Mod(\mathbb Z)^\wedge_p$ is the Bousfield localization of $\Mod(\mathbb Z)$ at $\mathbb F_p$. Alternatively, it is the stable $\infty$-category / dg-category of chain complexes of $p$-complete abelian groups localized at quasi-isomorphism. An abelian group $A$ is $p$-complete if it is a $\mathbb Z_{(p)}$-module and $\Ext^\ast(\mathbb Q, A) = 0$. For the comonadicity statement here, it's important to work with more than just the homotopy categories or just the hearts of these categories.