Cohomology Ring of the Klein Bottle

[thomas-lamiaux]

Starting computing the cohomology ring of K²

[thomas-lamiaux]

@aljungstrom won't compute after 10 minutes on my ok computer https://github.com/agda/cubical/pull/882/files#diff-b89e4f1599c7dba39bcde49cd6c8c0df1239f68261f2abf543ca8b274b049a45R461

[thomas-lamiaux]

@aljungstrom @mortberg This example is done up to the proof that (a b : ℤ) → (ϕ₁ a) ⌣ (ϕ₁ b) ≡ 0ₕ 2 Proof that seems too slow to compute on my computer

[thomas-lamiaux]

I have added :

• it suffices to prove (phi 1) cup (phi 1) = 0 to prove it for any a b
• I have added that if the H^n is odd, and H^2n is without Z, then (phi n) cup (phi n) = 0 I wanted to do that to prove the cup product is trivial but it ony work if there is not 2-torsion group, but Z/2... is an entire 2-torsion group

[thomas-lamiaux]

@mortberg With Axel lemme, it is now done

[thomas-lamiaux]

done