Clean up Cohomology Ring #845
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
-> 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
-> A cleaner way to deal with the cup product -> Finish all the structure except some cases of the cup-product -> Prove the retraction property
|
@aljungstrom Let me know when the hole has been filled by marking this ready for review and I'll review it. @thomas-lamiaux It will be easier for me to review this PR if it's just about CP2 and the cleaning of the other cohomology ring examples are done in separate PRs building on this one (just make a branch starting from the tip of this one and make a new PR based on it). That way I know what's going on in each PR and don't get such huge diffs in lots of files when I just want to look at the code for CP2 :-) |
|
I have transformed this on in cleaning because I would like to have those functions when I do RP2 |
|
Does someone have an idea why this is not working anymore ? |
|
@thomas-lamiaux If you rebase your PR, CI should go back to passing 🙂 |
|
@plt-amy indeed, good to go |
This file add CP2 up to a missing lemma as indicated in the file.
The lemma is provable according to Axel, at least by switching the isomorphism.
In consequence, the file is written in such a fashion that it suffices to pluggin the good iso plus the missing lemma to have a characterization.
This PR also adds a simpler way to handle the cup-product by just looking at the eliminator and some notation.
Those the other files are going to be rewritten accordingly.