Skip to content
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 RP2 \/ S1 #883

Merged
merged 172 commits into from
Sep 19, 2022
Merged

Cohomology Ring of RP2 \/ S1 #883

merged 172 commits into from
Sep 19, 2022

Conversation

thomas-lamiaux
Copy link
Contributor

Start computing the cohomology Ring of RP2 / S1

thomas-lamiaux and others added 30 commits April 6, 2022 13:57
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
@thomas-lamiaux thomas-lamiaux marked this pull request as ready for review September 4, 2022 16:45
@thomas-lamiaux
Copy link
Contributor Author

@mortberg Ready too.

@mortberg
Copy link
Collaborator

Lots of conflicts here now, please rebase on master

Copy link
Collaborator

@mortberg mortberg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

minor comments

Cubical/ZCohomology/Groups/RP2wedgeS1.agda Outdated Show resolved Hide resolved
Cubical/ZCohomology/Groups/RP2wedgeS1.agda Outdated Show resolved Hide resolved
Cubical/ZCohomology/Groups/RP2wedgeS1.agda Outdated Show resolved Hide resolved
@mortberg mortberg merged commit 1acc15f into agda:master Sep 19, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants