What exactly does Remark 7.2 in math.uni-bonn.de/people/scholze/Condensed.pdf want to say? What goes from if the underlying condensed ring is not discrete? I am quite confused by the remark. I am not sure what he wants to say, so any short explanation would be helpful and appreciated.

It's just saying that the functor S↦A[S] has additional functoriality: not only for maps S→T but also for $\underline(A)$-linear combinations thereof. The things that break if A is not discrete is the description of $\underline{A}[S](-)$ as sheafification of $\underline{A}[S(-)]$. I'm quite sure what the point of that remark is, since it is pretty much obvious that you have this added functoriality if A is an analytic ring. Perhaps he wanted to remark this is not true for general pre-analytic?

@Dedalus Well, it's the object representing the functor M↦M(S). I'm not quite sure of the details beyond that

But as I said, it's not completely clear to me what the point of that remark is

@DenisNardin Sorry, what is M?

An arbitrary $\underline{A}$-module

OK, now I see. You want to say that \underline{A}[S] is the object representing evaluation at S. This exists because of adjoint functor theorems, I suppose. Do I need to care about size issuses here? I often feel uncomfortable invoking those theorems here because of size...

Dunno, maybe I should stop answering because I did not think this through honestly

Your answers are very helpful :)

In HA Prop. A.1.9 Lurie proves the following theorem: Let $\mathcal{X}$ be an $\infty$-topos locally of constant shape, then for any morphism $X \to Y$ in $\mathcal{S}$, and any morphism $Z \to \pi^*Y$ in $\mathcal{X}$, the morphism $\pi_!(\pi^*X \times_{\pi^*Y} Z) \to X \times_Y \pi_! Z$ is an equivalence. In his proof, Lurie reduces to the case $Y = 1$ by writing $Y$ as a colimit of a constant diagram valued in $1$; cont.

curiously (in my mind) he takes the constant diagram from the category of simplices of $Y$ rather than just $Y$ itself. Is this necessary? I don't see what goes wrong if I just use $Y$.

@AdrianClough it is not. What's happening here is that as a functor of Y, buth sides commutes with colimits (where you think of it as a functor in Y by pulling back Z and X). Then spaces is generated under colimits from the point, no matter how exactly :-)

@S.carmeli Good, that's what I thought! Thanks!

@AdrianClough actually, the fact that both sides are colimits preserving made me hope I could prove it also for a morphism A-->B of infinity topoi which is not terminal. But then B is not generated by the terminal object and the proof breaks down. I suspect this is not true in general but have no counter example.

Where Cellular here means obtained by taking pushouts of attaching maps from free operads on a single operation of some arity times a sphere of some dimension mapping to $\mathbb{E}_0$

So in other words i'm starting with $\mathbb{E}_0$ and trying to approximate $\mathbb{E}_{\infty}$ with it up to dimension $k$ as efficiently as possible arity-wise.

@SaalHardali i can't piece together a more solid thing to say, but i'd recommend looking at the introductions to hedayatzadeh's various articles on multilinear algebra with group schemes. he points out various things that can go wrong: you may not actually have enough colimits unless you put more serious restrictions on the base than BP_* enjoys; even if you have colimits, an argument with slopes shows that you might be forced to get 0 back, but which surely won't match BP_* K(Z, m); …

again, this second part about existence is sort of an aside; i don't think these theorems actually bear directly on BP_* K(Z, m), but maybe they'll heighten your sense of caution

@EricPeterson Thanks that's helpful. I have to say my sense of caution is all over the place about this. However whenever I go back to these RW papers I do get the feeling that there is somewhere in the ether a canonical coordinate independent description of this hopf algebra. So at least once I wanna see how the naive attempt fails and why