I am reading Barry Mazur and Tom Weston's note Euler Systems and Arithmetic Geometry ([here][1] is the link). I have a question about the following fact in section 2.2 page 87:
Let $K$ be a local field with the ring of integers $\mathcal O$ with the maximal ideal $\mathfrak m$ and the residue field $k$, and let $A$ be an abelian variety over $K$. Then the kernel $A_1$ of the reduction map $A(\mathcal O)\to A(k)$ can be identified with the $\mathfrak m-$valued points of some formal group.
Here, I guess this formal group is defined by the completion of $\mathcal A$ (the Neron model of $A$) along $\mathfrak m$ at the identity element, similarly to the elliptic curve case (you can see more detail about this definition [here][2], Andrei Jorza's thesis, section 2.6.1). Is it true?
When $A$ is an elliptic curve, this result is proved in Joseph Silverman's book, The arithmetic of elliptic curves, Chapter VII. Proposition 2.2. However, it seems that this proof can not handle the general case because abelian varieties can not be described by explicit equations.
Can anyone provide me some hints with any reference to this fact?
Edit: It is Theorem C.2.6 in Diophantine Geometry, M. Hindry and J. Silverman. The construction of formal groups and the proof of the theorem are quite similar to the elliptic curve case. [1]: https://people.math.umass.edu/~weston/cn/mazur.pdf [2]: https://wstein.org/projects/jorza.pdf