Cohomology Rings #759
Cohomology Rings #759
Conversation
The index and the groups were at the same level. The should be at different one, for instance if the index is Nat, and the group something else
-> Modify some notions in gradedCommutativity -> new lemme for the "good" -h^ -> proof
-> Because this case is so degenerated, things compute. This new proof is forgetting some of the computation to have proof that will rise better to non-degenerated case
-> changing gradedComm by gradedCom' to account the previuous change
|
To prove that H^n (X) are gradedCommutative, -h _ . _ is introduced. Hence I have a introduced a -h _ ._ and renamed the other one and the related function by adding a prime. Nevertheless, this breaks a lot of dependency because the graded operator is used in several files. |
-> There is a need of the special as on the left we need the CommRing to take A / < a, ..., b > and we nedd a ring on the right as H*(X) is not a CommRing but a gradedComm Ring
|
The content of the Pull request is done. |
Cubical/Algebra/CommRing/Instances/MultivariatePoly-Quotient-notationZ.agda
Outdated
Show resolved
Hide resolved
Cubical/ZCohomology/CohomologyRings/Eliminator-Poly-Quotient-to-Ring.agda
Outdated
Show resolved
Hide resolved
Add a proper definition of the cohomology rings.
Work in progress : compute some cohomology rings