Sorry for being cryptic here! After inverting $\ell$, taking $\hat{G}$-invariants is exact, so the result is clear. Also, taking $\hat{G}$-invariants preserves finite type $\mathbb Z_\ell$-algebras; I gather I missed the good reference for that. Then to prove that it's a universal homeomorphism, it suffices to identify $\overline{\mathbb F}_\ell$-points. These correspond, by Haboush, to closed $\hat{G}$-orbits of the algebras base changed to $\overline{\mathbb F}_\ell$. But these closed $\hat{G}$-orbits can be identified easily.

In general, to check something lies in $D((C,C^+)_\blacksquare)\subset D(\mathrm{Cond}(C))$, one can forget along $D(\mathrm{Cond}(C))\to D(\mathrm{Cond}(C^+))$ and check containment in $D((C^+,C^+)_\blacksquare)$.

Ah, yes, I was assuming the norm to be multiplicative. This is the critical case of Gelfand-Mazur. (Once you know that case, you get spectral theory, and thus the whole Gelfand-Mazur. Also, for finite extensions of $\mathbb C$, you can always find a multiplicative norm (by norming down to $\mathbb C$).)

Is this proof known? I also wanted to comment that the existence of the minimum is not really important: One can rewrite the proof in slightly more constructive manner, as starting from any $z_0$ and producing a $z_1$ with $|x-z_1|\leq 0.99|x-z_0|$ (and $|z_1-z_0|\leq 100|x-z_0|$, so the resulting sequence of $z_i$'s will converge for trivial reasons). In this rewriting, one even needs only finitely many roots of unity.

You are right that in the non-derived setting, you get the Banach-Smith duality (and in general you get the compact-open topology, so likely nonderived biduality more generally for "stereotype" spaces). In the derived setting, things are much more subtle however! The derived dual of a Smith is the corresponding Banach (concentrated in degree 0), but I expect that for most infinite-dimensional Banach spaces, the derived dual sits in many degrees. This is related to this entropy nonsense (which gives Ext^1's of l^1 against R), but also to whether the continuum hypothesis holds or so.

1: Yes. 2: It is already solid, as solid modules are stable under all colimits(!).

As mentioned in the other question, the solid tensor products do not quite work out this way. I haven't tried to look at loop groups from this perspective.

The unique extension can be phrased as the condition that the map $\mathrm{Hom}(\mathcal M_p(S),V)\to H^0(S,V)$ is an isomorphism. Going "higher", one can ask that also $\mathrm{Ext}^i(\mathcal M_p(S),V)\to H^i(S,V)$ is an isomorphism, and for profinite $S$, one has $H^i(S,V)=0$ for $i>0$, so one arrives at this Ext-vanishing statement.