When is a formal group smooth? This is a question that I suspect is simply a matter of technical issues written down or clarified somewhere in the literature, but which I can't find.
Suppose we're working over an arbitrary base scheme $S$, maybe with some unspecified basic niceness assumptions. Following, e.g., the terminology used on p. 493 of Hazewinkel's tome Formal Groups and Applications, we can define the category of formal groups over $S$ simply as the group objects in formal schemes. Some of these formal groups' underlying spaces can be written as a relative formal spectrum, for example in the one-dimensional case $\underline{\operatorname{Spf}}_S\mathcal{O}_S[[t]]$, in which case they are called smooth by Hazewinkel. I've also variously seen the smooth ones called formal Lie groups, or even the term "formal groups" used exclusively to refer to these special ones, as in the notes of Weinstein on The geometry of Lubin–Tate spaces.
In any case, these formal groups that possess such a framing give rise to formal group laws, which is great. My question is, what are the most natural/general conditions on a formal group that imply that it has a framing? For example, I guess certainly at minimum it should be connected and formally smooth, and I believe this is enough if $S$ is the spectrum of a DVR, or even a local ring. 
But in general it seems like the sheaf on $S$ given by the relative tangent space also needs to be free. For example, if we take a non-stacky open modular curve over $\mathbb{Z}[1/N]$ or even $\mathbb{Q}$, and look at the formal completion of the universal elliptic curve over it, I believe it can't have a framing since the corresponding vector bundle is in general nontrivial. (This point is what motivated the question, because on the bottom of p. 19 of Artin and Mazur - Formal groups arising from algebraic varieties, it seems to be claimed that a pretty general class formal groups of including the universal elliptic curve example is of Lie type, which seems false.)
Is this triviality of the relative tangent bundle sufficient? It seems like you could probably prove something like this using formal smoothness by lifting jets over increasing thickenings, but I'd love a place this is all written down.
 A: I think an adaptation of Schlessinger's argument from Functors of Artin rings should work. Let $\Lambda$ be a Noetherian ring, and suppose we have a connected formal group $\mathcal{G}$ formally smooth over $\Lambda$ with relative tangent space $\mathcal{G}(\Lambda[t]/t^2)\cong \Lambda^n$. We also assume that at any closed point $\Lambda \to k$, $\mathcal{G}$ has a formal group law, hence consists only a single point (the reduction of the identity). In practice, this seems like very little to ask, though it'd be nice to figure out a more natural way to state this hypothesis in terms of $\mathcal{G}$ over $\Lambda$. (Edit: oh I guess it's probably more natural to just require $\mathcal{G}(\Lambda)$ to be a singleton; I thought there was a problem with this, but it's actually fine.)
We claim $\mathcal{G}$ can be pro-represented by some topological Noetherian $\Lambda$-algebra $R$, which is furthermore complete with respect to the ideal $\mathfrak{a}$ giving the identity section $R/\mathfrak{a} \cong \Lambda$. Indeed, we can always replace any representing object $O$ by the completion of its local ring at the identity point $\widehat{\mathcal{O}(O)_{id}}$, since for an arbitrary local Artin algebra $A$ over $R$ and an $A$-point of $\mathcal{G}$, the image of this ideal under any induced map of rings $\mathcal{O}(O)_{\text{id}}\to A$ must be nilpotent - which is just to say that the unique closed point of $\text{Spec }A$ must map to a reduction of the identity, as mentioned earlier. 
Using the map $\mathcal{G}(\Lambda[t]/t^2)\cong \Lambda^n$, iteratively lift the $n$ basis vectors on the RHS by formal smoothness to elements of $\mathcal{G}(\Lambda[t])/t^k)$ for increasing $k$; in the limit, we obtain a continuous map $R\to \Lambda[[t_1,t_2,\ldots, t_n]]$ which induces an isomorphism on tangent spaces. We claim this is an isomorphism. The key lemma is an adaptation of Lemma 1.1 from Schlessinger:
Lemma: Let $S$ and $T$ be local topological Noetherian $\Lambda$-algebras, each with a distinguished $\Lambda$-point given by the respective ideals $\mathfrak{m}$ and $\mathfrak{n}$, and complete with respect to these ideals. If $\phi: S\to T$ is an adic map (sending $\mathfrak{m}$ into $\mathfrak{n}$) respecting these $R$-points, and it induces a surjection on relative tangent spaces over $\Lambda$, then it is a surjection.
Proof: The problem is to lift the surjection $\mathfrak{m}/\mathfrak{m}^2\twoheadrightarrow \mathfrak{n}/\mathfrak{n}^2$ to a surjection $\mathfrak{m}\twoheadrightarrow \mathfrak{n}$, as then we would be done since $\phi$ respects the $R$-point. We can further reduce this into showing $\mathfrak{m}^k/\mathfrak{m}^{k+1}\twoheadrightarrow \mathfrak{n}^k/\mathfrak{n}^{k+1}$ via a similar dévissage argument. This last assertion follows by pushing forward the $k=1$ case along the surjections $\text{Sym}^k(\mathfrak{m}/\mathfrak{m}^2)\twoheadrightarrow \mathfrak{m}^k/\mathfrak{m}^{k+1}$ and similarly for $\mathfrak{n}$. $\square$
In the end, the crucial thing was just that formal groups' coordinate rings can be taken to be complete with respect to the ideal at a distinguished point over an arbitrary base.
