Zulip Chat Archive

Stream: Is there code for X?

Topic: mv_power_series


view this post on Zulip Reid Barton (Oct 02 2020 at 00:03):

Do we have composition of formal power series yet (under suitable conditions)? Or, what is more or less the same thing, evaluation at elements in the maximal ideal of a complete local ring?

view this post on Zulip Reid Barton (Oct 02 2020 at 00:04):

Can I define a formal group law--roughly, a power series F(X,Y)R[[X,Y]]F(X, Y) \in R[[X, Y]] of the form F(X,Y)=X+Y+F(X, Y) = X + Y + \cdots satisfying F(F(X,Y),Z)=F(X,F(Y,Z))F(F(X, Y), Z) = F(X, F(Y, Z))?

view this post on Zulip Reid Barton (Oct 02 2020 at 00:12):

I know we have analysis.analytic.composition so we must have something in this area but it's a bit intimidating and I didn't immediately find anything like mv_power_series.eval or .comp.

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 02:16):

Analytic functions are based on multilinear_functions, not mv_power_series.

view this post on Zulip Yury G. Kudryashov (Oct 02 2020 at 02:17):

AFAIK, we don't have the composition of (mv_)power_series yet.

view this post on Zulip Johan Commelin (Oct 02 2020 at 06:09):

@Reid Barton Nope, we don't have these yet... sorry

view this post on Zulip Reid Barton (Oct 04 2020 at 17:06):

Does this outline sound correct? Given an RR-algebra AA which is a complete local ring and elements x,y,Ax, y, \ldots \in A belonging to the maximal ideal, define the evaluation of a formal power series FR[[X,Y,]]F \in R[[X, Y, \ldots]] at x,y,x, y, \ldots. Then prove the power series ring is itself such an algebra whose maximal ideal consists of the power series with 0 leading term.

view this post on Zulip Reid Barton (Oct 04 2020 at 17:07):

Are those the right hypotheses? Do we have these concepts in mathlib yet?

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 20:44):

You don't need local. If J is an ideal of the R-algebra A and A is J-adically separated and complete (a concept which we might not have -- but which we used in the perfectoid project so will be around somewhere -- it just means that A to projlim A/J^n is an iso) then you can evaluate power series at elements of J

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 20:46):

Probably in the perfectoid project we had the concept of the J-adic topology on A and the notion of the corresponding uniform space being complete and separated but now there might be some work defining that power series map

view this post on Zulip Johan Commelin (Oct 04 2020 at 20:53):

@Reid Barton I think we have all what @Kevin Buzzard is talking about in mathlib now. Thanks to @Kenny Lau who added J-adic stuff.

view this post on Zulip Yury G. Kudryashov (Oct 04 2020 at 21:02):

/me feels like a person in a foreign country. I hope, after someone formalizes this, we'll have mv_power_series.comp (f g : mv_power_series σ R) that gives what everybody expects (if g has a non-zero constant coeff, then comp can either return zero, or silently subtract this constant first).


Last updated: May 17 2021 at 15:13 UTC