Stream: Is there code for X?
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 of the form satisfying ?
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
Yury G. Kudryashov (Oct 02 2020 at 02:16):
Analytic functions are based on
Yury G. Kudryashov (Oct 02 2020 at 02:17):
AFAIK, we don't have the composition of
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 -algebra which is a complete local ring and elements belonging to the maximal ideal, define the evaluation of a formal power series at . 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