H*(Kleinbottle,Z/2) - Githubissues

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

454 stars 139 forks source link

H*(Kleinbottle,Z/2) #928

Closed aljungstrom closed 2 years ago

aljungstrom commented 2 years ago

This PR contains

Def of cohomology rings with R-coeffs (pretty much a direct copy of the Z-case)
Cohomology ring of the Klein bottle in Z/2-coeffs.
For some reason I had cohomology groups of wedge sums on this branch too, so I threw them in as well.

thomas-lamiaux commented 2 years ago

Shouldn't this def be in algebra ? https://github.com/agda/cubical/pull/928/files#diff-2ac1bdc3baa3997bd843c09403b37cfa86fbb20580d09320cc88bbc58ad940e9R205

mortberg commented 2 years ago

Shouldn't this def be in algebra ? https://github.com/agda/cubical/pull/928/files#diff-2ac1bdc3baa3997bd843c09403b37cfa86fbb20580d09320cc88bbc58ad940e9R205

I can't see which proof you're referring to. Please comment on the actual line in the code instead