-
Notifications
You must be signed in to change notification settings - Fork 134
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Cohomology Ring of S2 \/ S4 #879
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 @mortberg On this proof, the function gets more complicated, as there is 2 variables, there is 3 trivial cases Maybe add a partition on the direct sense ? But then it would be complicated to prove retraction. |
Hi @mortberg and @aljungstrom, I have spend two days computing Though I have a very weird issue. When proving retraction, I have to prove
And this won't refine ! At the end, I finished by putting everything in a ad hoc module and just pass it as a parameter as it seems that the issue is in leftInv. I mean, the file work this way, so it can be kept this way but this annoying as you loses the computation of phi_4 when doing that, hopefully I don't need them here but still |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few quick comments
I fixed the conflicts. Will merge once the CI is finished |
PR to compute the cohomology ring of S2 / S4 which should be Z[X,Y]/<XY, X², Y²>
For CP2 / S2 / S4, this should give an example where the groups are the same but the ring are different.
This is example can be seen as better than Torus / S2 / S1 / S1 as :