Mon 16 Jan 2023 16:45 - 17:07 at Studio 1 - Formalized Mathematics I Chair(s): Adam Chlipala

In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomology groups together with a multiplication induced by the cup product, and can in many cases be characterized as quotients of multivariate polynomial rings. To this end, we introduce appropriate definitions of direct sums and graded rings, which we then use to define both cohomology rings and multivariate polynomial rings. Using this, we compute the cohomology rings of some classical spaces, such as the spheres and the Klein bottle. The formalization is constructive so that it can be used to do concrete computations, and it relies on the Cubical Agda system which natively supports higher inductive types and computational univalence.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 18:00
Formalized Mathematics ICPP at Studio 1
Chair(s): Adam Chlipala Massachusetts Institute of Technology
16:00
22m
Talk
Formalising the h-principle and sphere eversionremote presentation
CPP
Patrick Massot , Floris van Doorn University of Pittsburgh, Oliver Nash Imperial College, London
16:22
22m
Talk
A Formalized Reduction of Keller's Conjecture
CPP
Joshua Clune Carnegie Mellon University
16:45
22m
Talk
Computing Cohomology Rings in Cubical Agdadistinguished paper
CPP
Thomas Lamiaux University of Paris-Saclay, Ens Paris-Saclay, Axel Ljungström Stockholm University, Anders Mörtberg Department of Mathematics, Stockholm University
17:07
8m
Break
short break
CPP

17:15
45m
Meeting
CPP Business Meeting
CPP

Pre-print