Let $S$ be a scheme (not necessarily locally noetherian), $X$ a smooth separated group scheme over $S$, and $\hat{X}$ be the formal completion along with the identity section.
Then does the group scheme-structure on $X$ induce the formal group scheme-structure on $\hat{X}$? i.e., do the multiplication $m : X \times_S X \to X$ and the inversion $X \to X$ factor through $\hat{X}$, and these satisfy the group law?
And is the correspondence $X \to \hat{X}$ a functor from the category of nice group schemes to the category of the formal groups?
If this is true, then an abelian scheme induces a formal group of $\dim$-variables. (The multiplication is the image of $T$ under $A[[T]] \to A[[X, Y]]$, the inversion is the image of $T$ under $A[[T]] \to A[[T]]$. )
I have shown that a morpshim of schemes induce a unique morphism on their formal completion: $S$ a scheme, $X, Y$ $S$-schemes given with sections (assume its sheaf of ideals are finitely presented), $f : X \to Y$ an $S$ morphism which is compatible with their given sections. Then there exists only one morphism $\hat{f} : \hat{X} \to \hat{Y}$ which is compatible with $f$.
So it seems that if we can show the compatibility of completion with fibre products (i.e., $ (X \times_S Y)^{\hat{}} \cong \hat{X} \hat{\times}_S \hat{Y}$, including the canonical map to $X \times_S Y$), the highlighted statement is true.
For, since we can take $\hat{X} \hat{\times}_S \hat{X}$ as the completion of $X \times_S X$, there exists a unique map $m : \hat{X} \hat{\times}_S \hat{X} \to \hat{X} $, compatible with the multiplication on $X$.
And similar to the inversion.
The group law follows from the uniqueness of the completion of morphism.
And if this is true, then a morphism between nice schemes induces a morphism of formal groups, and hence we have a functor from the category of "nice" group scheme to the category of formal groups.
Is my opinion right? And please show the compatibility of completion with fibre products.
P.S. I have posted a similar question. The answer says that using the functor of points we can show that $\hat{X} \hat{\times} \hat{X} \to X \times X \to X$ factors through $\hat{X}$. But I can't understand it.
Thank you very much!