Show the definitions of polynomials are equivalent

[felixwellen]

There are three definitions of polynomials (one is called FreeCommAlgebra) and it should be shown, that all of them are equivalent. Possibly the best strategy is to show that all fullfill the universal property of the algebra of polynomials over a commutative ring k, which is:

Hom(k[X_1,...,X_n], A) = (Fin n -> A)

where Hom denotes the type of homomorphisms of k-Algebras.

[thomas-lamiaux]

I don't have the time right now but if someone wants to do it, I have the following idea :

There are actually four potential definitions of the polynomials in the library :

1. The HIT one located in Polynomials
2. The truncated list one located in Polynomials
3. The freely generated one located ?
4. The almost null sequences one located inside Univariate.Base. No one ever developed a structure on the definition. However it should be easy as it is what is done in #798 in the complicated case where is dependency.

So about structure, it would be good to move 1 and 4, complete 4 + find new names. Possible do the same as in Int, keeping one as the preferred one.

To prove the equivalence, one could prove the universal property but actually in this case, it is probably easier to give syntactic translation. Indeed there is already a proof of 1 <-> 2. 2 <-> 4 is proved on types, so it suffices to define the structure and prove it on the operations. 1 <-> 3 should be easy as it is very similar structure. Thus givening us the equivalence without too much more work.

[thomas-lamiaux]

update : #798 is going to add full CommRing structure around 4 that was missing and prove the equivalence. Hence in the library, there is going to be 4 <-> 1 <-> 2 so it suffices to add 1 <-> 3 to finish the job

[felixwellen]

I'll do 1 <-> 3 by:

• Constructing algebra structure on the list-polynomials
• Show the map from the universal property of the polynomial HiT in Algebra.CommAlgebra.FreeCommAlgebra is surjective
• ... show it is an Embedding, by constructing a one-sided inverse (showing left invertibility with the universal property)

[felixwellen]

Or maybe I don't - just realized I have to show, that the inverse to the induced morphism is an algebra-hom... So it might still be easier to just show that the list-based-polynomials have the correct universal property.