Direct sum and gradedRing

[thomas-lamiaux]

The goal of this PR has changed during the work. This is the updated message

Overview

The goal of this PR is to add a general notion graded ring.
This for two definitions of the direct sum that shown equivalent.

HIT Direct Sum

• Add a pseudo normal form for the HIT direct sum if indexed by N
• Add a proof that base is base k a = base l b => a = 0_k & b = 0_l for a decidable index
• Add a universal property

Almost null sequences Direct Sum

• Add another definition of the direct sum using almost null sequences
• Prove the equivalence between the two definition of the direct sum if the index is N

Graded Ring

• Add a general notion of graded ring using the HIT direct sum
• Add some instances of gradedRing :
• • Trivial Graded Ring
• • Polynomial
• • Cohomology Ring
• Replace the following constructions using the new graded ring construction
• • Polynomials
• • Cohomology Ring
• Add the almost null sequences as an instance of the graded Ring when the index is a N monoid.
• Add Instances using this new definition :
• • Polynomials
• • Cohomology Ring

[thomas-lamiaux]

I have proved that if can compute a normal form then the function is injective and so you have the equivalence !
This a huge progress because the data structure are mess here and this proof gives which data structures to use and how to use them.

I still have to add the some lemma on depVec and compute the normal form but now this should work.
By the way, The PR is currently a big mess.
This due to the complexity of all the data structures that makes really hard to prove things without trying a bunch of things and looking at the entire technical details.
Hence there is a lot of traces of past attempts and several naming convention coexisting due to past attempts.
This will be clean once the proof are completed.

[thomas-lamiaux]

@mortberg I have refactored Polynomials. Do you prefer the current

• Multivariate
• Univariate
• • UnivariateList
• • UnivariateFun
• • UnivariateHIT

Or would you prefer

• Multivariate
• Univariate
• UnivariateList
• UnivariateFun
• UnivariateHIT

[thomas-lamiaux]

I have fixed all issues except the bit of code that needs to be generalize that I will do by thursday.

[mortberg]

@mortberg I have refactored Polynomials. Do you prefer the current

* Multivariate

* Univariate

* * UnivariateList

* * UnivariateFun

* * UnivariateHIT

Or would you prefer

* Multivariate

* Univariate

* UnivariateList

* UnivariateFun

* UnivariateHIT

What is "Univariate" in the second suggestion? I think I prefer the flatter structure on matter what, there's already so much nesting.

[thomas-lamiaux]

@mortberg you can consider it as done