7:28 PM
@AntonFetisov they're right: no one knows. you can reformulate what peter said like this: if there exists a map MU –> E of commutative rings at all, then Spf E^* CP^∞ gives a formal group, and then such maps furthermore biject with coordinates on it
the quantifiers here are really different from what happens in algebra: for any ring R and any formal group G / R and any coordinate x on G, there's a map f: MU_* –> R such that (G, x) = f^* (G_univ, x_univ) arises as the base-change of a fixed (G_univ, x_univ) over MU_*
in the topological setting there is a fixed object G = Spf E^* CP^∞, whose presentations (if it admits presentation as a formal group at all) arise as base-change from Spf MU^* CP^∞
so if your proposed definition of "derived formal group" admits more than one per choise of base ring spectrum, then it's not what's captured by MU
adding "E_∞" only makes the situation more confusing still
idk how appropriate this analogy truly is, but in explicit class field theory, one attaches to a local number ring a particular formal group, its Lubin-Tate group, and extracts information about the number ring through that
the situation in topology seems to be rather near to that