Is the Thom diagonal co-$E_\infty$? Given a map of spaces $f:X\to BGL_1(R)$ for $R$ an $E_\infty$-ring spectrum (of course this can be done more generally) one can produce a Thom spectrum $Mf$ by a number of methods. Let's denote such a datum by $(X,f)$ and let $(X,\ast)$ denote the datum $X\to \ast\to BGL_1(R)$, whose associated Thom spectrum is $R\wedge\Sigma^\infty_+X$, which we will denote by $R[X]$. There is a morphism in $Top_{BGL_1(R)}$, which we might denote $(\Delta,-\times\ast):(X,f)\to (X\times X,f\times\ast)$ which Thomifies to the morphism of spectra $Mf\to Mf\wedge R[X]$ (note that the target of this map is an object of $Top_{BGL_1(R)}$ because we can multiply the two maps together using the multiplicative structure on $BGL_1(R)$). It is not hard to show that the map $(X,\ast)\to (X,\ast\times\ast)$ induces a co-$E_\infty$ comultiplication on $R[X]$. However, it seems much less clear to me that the Thom diagonal in general exhibits $Mf$ as an $E_\infty$-comodule over $R[X]$. This would follow from showing that the above diagonal map exhibits $(X,f)$ as a co-$E_\infty$-comodule in $Top_{BGL_1(R)}$. Intuitively, I believe this to be true because all of the necessary coherences exist on the diagonal map, and on the morphism $f$ we're simply crossing with the trivial map. Note that the above is not the trivial coaction, which would be given by $X\simeq X\times\ast\overset{id_X\times\ast}\to X\times X$.
For me, being a co-$E_\infty$ comodule simply means being an $E_\infty$-module over the $E_\infty$-algebra $R[X]$ in the opposite of the category of interest. Note also that in the category $Top_{BGL_1(R)}$ the symmetric monoidal structure is given by the infinite loop space structure of $BGL_1(R)$. 
I have been playing with this for some time but have not been able to prove it with the tools I have.  
 A: The answer to this is yes, it is co-$E_\infty$. Let $\iota\colon BGL_1(R)\to Mod_R$ be the inclusion. Since colimit is left adjoint to the strong monoidal diagonal functor, it's oplax monoidal. Note that the constant functor $\kappa_R\colon X\to Mod_R$ is the monoidal unit for the pointwise monoidal structure in $Mod_R^X$ (hence a coalgebra over which every other functor is a comodule). So there is an equivalence $\iota\circ f\xrightarrow{\sim} (\iota\circ f)\otimes_{pw} \kappa_R$ in $Mod_R^X$, where $\otimes_{pw}$ is the pointwise tensor product. Taking the colimit of this, and using that colimit is oplax monoidal gives us a coaction of $colim(\kappa_R)\simeq R[X]$ on $colim(\iota\circ f)\simeq Mf$. This is all as monoidal (e.g. $\mathbb{E}_k$-monoidal) as its various moving parts allow it to be. The only thing one needs to check is that the resulting morphism $Mf\to Mf\otimes_R R[X]\simeq Mf\otimes X$ is the "Thom diagonal" in the literature. This follows from Theorem 4.15 in my preprint.
