Given a presentable Cartesian symmetric monoidal $\infty$-category $C$, every object is a cocommutative comonoid and for a fixed $Z\in C$ there is an equivalence $C_{/Z}\simeq LCoMod_{Z}(C)$ where the coaction associated to $X→Z$ is $X\to X\times X\to Z\times X$. If we further assume that $Z$ is an algebra object of $C$ then we can equip $LCoMod_Z(C)$ with a monoidal structure, the Day convolution structure, where, roughly, the tensor product of $f\colon X\to Z$ and $g\colon Y\to Z$ is $\mu_Z(f\times g)\colon X\times Y\to Z\times Z\to Z$.

If we consider the trivial map $X\to \ast\to Z$, using the algebra structure of $Z$ to produce the unit $\ast\to Z$ it seems that this should define a comonoid in $C_{/Z}$ via the diagonal $X\to X\times X$ where the map to $Z$ on the left is $\ast$ and the map on the right is $\mu_Z\circ (\ast\times\ast)\circ\Delta\simeq\ast$. In the case of 1-categories this is pretty straightforward to prove.

Even more, given any other map $f\colon X\to Z$, there should be an $(X,\ast)$-comodule structure on $(X,f)$, again via the diagonal map, since $f\simeq \mu_Z\circ (f\times \ast)\circ\Delta$.

Does anyone know of a good categorical way to prove this, ideally $\infty$-categorical? Again, it's all relatively straightforward to check in a 1-category, but in an $\infty$-category it's not at all clear to me how to prove this.

Given a presentable Cartesian symmetric monoidal $\infty$-category $C$, every object is a cocommutative comonoid and for a fixed $Z\in C$ there is an equivalence $C_{/Z}\simeq LCoMod_{Z}(C)$ where the coaction associated to $X→Z$ is $X\to X\times X\to Z\times X$. If we further assume that $Z$ is an algebra object of $C$ then we can equip $LCoMod_Z(C)$ with a monoidal structure, the Day convolution structure, where, roughly, the tensor product of $f\colon X\to Z$ and $g\colon Y\to Z$ is $\mu_Z\circ(f\times g)\colon X\times Y\to Z\times Z\to Z$.

If we consider the trivial map $X\to \ast\to Z$, using the algebra structure of $Z$ to produce the unit $\ast\to Z$ it seems that this should define a comonoid in $C_{/Z}$ via the diagonal $X\to X\times X$ where the map to $Z$ on the left is $\ast$ and the map on the right is $\mu_Z\circ (\ast\times\ast)\circ\Delta\simeq\ast$. In the case of 1-categories this is pretty straightforward to prove.

Even more, given any other map $f\colon X\to Z$, there should be an $(X,\ast)$-comodule structure on $(X,f)$, again via the diagonal map, since $f\simeq \mu_Z\circ (f\times \ast)\circ\Delta$.

Does anyone know of a good categorical way to prove this, ideally $\infty$-categorical? Again, it's all relatively straightforward to check in a 1-category, but in an $\infty$-category it's not at all clear to me how to prove this.