Polynomials and formal power series

[lowasser]

In addition to the standard analytic power series in #1354 , we should consider building out the theory of formal power series and polynomials. It's not obvious to me how closely we should relate those two notions -- we could, for example, define polynomials as formal power series whose coefficients become zero after a certain upper bound.

Formal power series are not least on my mind because I've been reading a lot about generating functions recently, but they're also an easy environment in which to develop many analytic notions and functions first, and they're definable on any ring. I guess as a result they'd probably at least start in the ring theory folder.

[fredrik-bakke]

If the coefficient ring $R$ is not commutative, which of the following is taken as the definition of a formal power series?

1. $$\sum a_i x^i$$ (defines a left module over $R$)
2. $$\sum a_{i0} x^i a_{i1}$$ (defines a bimodule over $R$)
3. $$\sum a_{i0}\cdot x\cdot a_{i1} \cdot x \cdot \ldots \cdot x \cdot a_{ii}$$ (defines something like an $R$-algebra)

You might want to go with number 1 if your intention is to do commutative algebra eventually, but at least keep in mind that the noncommutative case is more ambiguous. Also, while these concepts have many many generalizations, it makes the most sense to me to start by defining them for arbitrary semirings.

[lowasser]

I lean towards sticking to the commutative case; I missed the importance of that criterion.

[fredrik-bakke]

I would be very surprised if one-sided formal power series are not useful in noncommutative algebra. For instance, already if you consider formal power series with coefficients in the center of $R$, then all the definitions of formal power series again coincide.

[lowasser]

Dumping thoughts for later implementation:

• I want to use this as a demonstration of the principles in Best practices: encapsulation #1359 . We're just going to pick one implementation, but make sure we have room to switch the implementation for something more general later, e.g. a simple specialization of the non-commutative case.
• Polynomials in one variable seem adequate, at least to start with. Notably, R[x, y] = R[x][y], so the univariate case suffices for any finite number of variables. (We probably want to prove things about swapping the variables and reassociating.)
• I think the best near-term implementation is the combination of a map N -> R of coefficients, and the mere existence of an upper bound on the nonzero coefficients. That seems pretty much necessary for the real numbers to be usable as polynomial coefficients.
• To actually calculate a polynomial's degree, we need decidable equality on the ring, and we further need a variation on the currently existing well-ordering property on the natural numbers: it's not decidable whether a natural number is an upper bound on the nonzero coefficients, but given that succ-N n is an upper bound, it's decidable if n is an upper bound. That's a weaker condition than the current well-ordering principle formulation, but it's sufficient.