Let $p$ be a prime. The adjunction

$$\mathbb F_p \otimes_\mathbb{Z} (-) : Mod(\mathbb Z) {}^\to_\leftarrow 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 {}^\to_\leftarrow 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](https://arxiv.org/abs/math/0105079) 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](https://arxiv.org/abs/1404.2156) -- $\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](https://ncatlab.org/nlab/show/implicit+infinity-category+theory+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.