Computing Cohomology Rings in Cubical Agda
summary
Claims a first fully mechanized, constructive definition of cohomology rings implemented in Cubical Agda, with concrete computations for spheres and the Klein bottle and a proof that CP2 and S4 differ as rings. Builds direct sums and graded rings using quotient inductive types, implements multivariate polynomials as direct sums, and proves ring isomorphisms by recursion. Product laws and associativity check out and typical space computations reduce to a few dozen lines.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:26Klein Bottle vs Mickey Mouse
- 2:21The Cohomology Ring
- 3:12What do we need to solve?
- 4:45Adapting the classical direct sum
- 5:52Building Graded Rings?
- 6:57Proving the properties?
- 7:38A quotient inductive type definition
- 9:02Defining a graded ring
- 11:08The HIT polynomials
- 12:37A General Method
- 13:14The benefit of the data structure
- 13:55A word on synthetic mathematics
- 15:12Conclusion
related talks
25mOn computing homological hitting sets
50mThe Wonders of Abstraction
01h 02mFine-Grained Counting Complexity I
23mMatrix multiplication via matrix groups
05mInfinities: More Than One
55mSiegel's Theorem, Edge Coloring, and a Holant Dichotomy
01h 31mCircuits of Bounded Depth
27mScheme Pearl: Quantum Continuations