论文标题
Cubical AGDA中的计算同种学环
Computing Cohomology Rings in Cubical Agda
论文作者
论文摘要
在同型类型理论中，使用较高的电感类型和单位性研究了共同体理论。本文通过提供了第一个完全机械化的共同体环定义来扩展以前的发展。这些环可以定义为共同学组的直接总和以及由杯产物引起的乘法，并且在许多情况下可以将其描述为多元多项式环的商。为此，我们介绍了直接总和和分级环的适当定义，然后我们用它们来定义同时的共同体环和多元多项式环。使用此过程，我们计算某些经典空间（例如球形和克莱因瓶）的共同学环。形式化是建设性的，因此可以用于进行具体计算，并且依赖于立方AGDA系统，该系统在本地支持更高的电感类型和计算单相。
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.
