11:10 AM
re: derived formal groups: i think it's unreasonable to expect MU to play the role of a moduli of derived formal groups in the generality y'all intend. the moduli it represents (in the homotopy category) is really different from the one you're used to: the algebroid (MU_, MU_ MU) tracks all (smooth, 1-dim'l) formal groups you can ever find on your favorite graded ring R_, but the algebroid (MU, MU ^ MU) only tracks coordinates on a single *fixed formal group Spf R^* CP^infty
if your definition of 'derived formal group' is wider than 'CP^'infty', MU won't directly know about it
there is a similar classical phenomenon that morava is super fond of: lubin-tate explicit CFT associates to a local number field L a particular (connected) p-divisible group. you can ofc find other formal groups over L, but this is the relevant one that governs CFT
i think a really responsible thing to ask yourself here is: how many other examples do you even want to capture with a definition of 'derived formal group'? and how many of those are more than one-step-removed variations on CP^infty?
i think there might be some out there as variations on the above analogy: even if L has only one formal group that's "relevant", something like k((t)) has a lot of relevant formal groups owing to the large number of abelian varieties over k, and maybe someday homotopy theory will have enough analogues of equi-characteristic objects that you'll find a rich & cool generic theory of derived formal groups lying around
you can imagine other similar fountainheads, but i think we are not there yet, and phenomena should come before theory here
(and, for what it's worth, i think SAG Section 8 is not really after any of this; it sounds like it's trying to recover facts in the neighborhood of: passing to a formal thickening of a closed object in a noetherian parent gives a flat map)
anyway: obviously just my opinion, happy to change it if yall think otherwise