Define polynomials in iset.mm

[jkingdon]

The most obviously relevant definitions for polynomials in set.mm are:

• support of a function, supp
• finitely supported, finSupp
• power series, mPwSer
• polynomial, mPoly

The way these fare in iset.mm is:

• support. Very problematic; it wouldn't appear that either "support" or "strong support" as defined at https://ncatlab.org/nlab/show/support+of+a+function#in_constructive_mathematics gets us very far when it comes to arbitrary rings
• finitely supported. Doesn't seem any easier than support.
• power series. I didn't try formalizing it but at a glance it seems like the set.mm definition might work.
  • the most obviously scary thing is the reference to gsum which isn't in iset.mm and which seems to have similar issues to the ones described in the rest of this issue about a finitely supported function, versus a function defined on a finite domain
• polynomial. My first idea is to start with set.mm's mPoly definition and change 𝑓 finSupp (0g‘𝑟) to dom f e. Fin.
  • although it is perhaps a good exercise to start, at least in one's thinking, with something simple, like a map from a natural number to coefficients, we do at some point want to build the ability to add polynomials, multiply polynomials, etc (see "polynomial ring" at https://en.wikipedia.org/wiki/Polynomial_ring or https://ncatlab.org/nlab/show/polynomial )
  • are there a lot of theorems in set.mm which want a countably infinite number of coefficients (and in the polynomial case all but a finite number of which are zero)? If so, one way or another we'd need to build the ability to take a finite number of coefficients and zero-fill all the other coefficients.

[jkingdon]

Some discussions I've had seem to confirm that finitely supported won't work and that instead we need some way of expressing an upper bound of the degree of the polynomial.

• https://mathstodon.xyz/@jdw/114644164458089269
• https://mathoverflow.net/questions/302516/constructively-is-the-unit-of-the-free-abelian-group-monad-on-sets-injective

The above idea for dom f e. Fin would seem to fit that concept.