## Stream: Is there code for X?

### Topic: mv_power_series

#### 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?

#### Reid Barton (Oct 02 2020 at 00:04):

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

#### Yury G. Kudryashov (Oct 02 2020 at 02:16):

Analytic functions are based on multilinear_functions, not mv_power_series.

#### Yury G. Kudryashov (Oct 02 2020 at 02:17):

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

#### Johan Commelin (Oct 02 2020 at 06:09):

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

#### Reid Barton (Oct 04 2020 at 17:06):

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 (Oct 04 2020 at 17:07):

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

#### 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

#### 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

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

#### 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