Formal group law?

Stream: Is there code for X?

[Jz Pan]

I remembered that I had asked this question before, maybe in the elliptic curve thread, and it's said that there are people working on this. But I can't find it anymore.

Again, do we have formal group laws in mathlib yet? Quoting from the book Formal groups and applications:

An n-dimensional formal group law over a ring A is an n-tuple of of power series F(X,Y)=(F_1(X,Y), ... ,F_n(X,Y)) in 2n indeterminates X_1, ... ,X_n, Y_1, ... ,Y_n such that F_i(X,Y) = X_i + Y_i mod deg 2and F_i(F(X,Y),Z)=F_i(X,F(Y,Z)) for all i. [...]

I think the answer is no, as F_i(F(X,Y),Z) is not defined in mathlib yet. This is similar to Polynomial.comp or [Mv]Polynomial.aeval, but it needs to consider the topology. For now maybe MvPowerSeries.comp can be defined in an ad-hoc way, ignoring constant coefficients. Then we can, at least, write down the definition of formal group law.

Some important properties:

• There is a unique inverse power series i(X). Should we add it to the definition, or just noncomputable def from a formal group law?
• Formal group law can give rise to actual groups.
• ...

Applications:

• Elliptic curves
• Fontaine's theory on p-divisible groups

[Ruben Van de Velde]

You don't mean #8485, right?

[Jz Pan]

Ruben Van de Velde said:

You don't mean #8485, right?

No, not that, which is the actual group structure on points of elliptic curves.

What I mean "application on elliptic curves" is the Chapter IV in Silverman's book The Arithmetic of elliptic curves. Some important properties of elliptic curves over finite fields and local fields derived from the formal groups.

[Junyan Xu]

There's #15158 which requires the constant coefficient to be nilpotent.

[Jz Pan]

I see. Seems that they must have projects on formal groups, then.

In the formal groups case, the constant coefficients are always zero.

[Junyan Xu]

Seems that they must have projects on formal groups, then.

Doesn't seem like so. The PRs are apparently from this directory in the divided powers repo.
(Did you just find out this thread and thumed up?)

[Jz Pan]

Junyan Xu said:

Seems that they must have projects on formal groups, then.

Doesn't seem like so. The PRs are apparently from this directory in the divided powers repo.

Oh I see. As far as I know, divided powers is used in Fontaine's theory and should be related to formal group laws.

(Did you just find out this thread and thumed up?)

Yes, I remembered that I have read that thread.