mv_power_series

Stream: Is there code for X?

[Reid Barton]

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?

[Reid Barton]

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

[Reid Barton]

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.

[Yury G. Kudryashov]

Analytic functions are based on multilinear_functions, not mv_power_series.

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Reid Barton]

Does this outline sound correct? Given an $R$-algebra $A$ which is a complete local ring and elements $x, y, \ldots \in A$ belonging to the maximal ideal, define the evaluation of a formal power series $F \in R[[X, Y, \ldots]]$ at $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.

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

@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.

[Yury G. Kudryashov]

/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).