Victor Blanchi: Toward a categorified version of Euler product formula for Riemann zeta function in HoTT
Victor Blanchi (École normale supérieure)
Abstract: In this seminar, I will present my formalizing project. First I need to define what is categorification. It is the idea of considering natural numbers as finite sets. Then there is not at most one equality between the categorified version of a natural number but a bunch of isomorphisms. Here is where homotopy type theory arrives, as it enables us to identify isomorphic finite sets. It turns out that it simplifies many constructions of combinatorics. It makes the theory of species of structure - a general framework to deal with combinatorics - clearer. A species of structure $S$ is a functor from the groupoid of finite sets to another category. For a finite set $F$, $S(F)$ is the set of all different structures of a certain kind one can put on $F$ for example all the ways of equipping $F$ with the structure of a tree. The action of $S$ on isomorphism is just renaming the different labels of the structure. In homotopy type theory the definition is much simpler as every function to the type of finite sets to another type is automatically a functor thanks to the action of the transport along identities. We also remark that many operations can be defined on more general versions of species. We then define species of sub-universe - where a sub-universe $P : \mathcal{U} \to \mathrm{Prop} $ is just the collection of types $X$ in the universe $\mathcal{U}$ satisfying the property $P(X)$ - which are function from a sub-universe $P$ to another sub-universe $Q$. Then, for every operation we define conditions on $P$ and $Q$ that make the operation associative, commutative, and unit laws.
From a species $S$ one can always defined a generating series $$\bar{S} (s) := \sum_{n : \mathbf{N}} \frac{S({1,...,n})}{n!} x ^n$$ and a Dirichlet series $$\tilde{S} (s) := \sum_{n : \mathbf{N}} \frac{S({1,...,n})}{n!} n^{-s}$$ associated to $S$. John Baez remarks that we can also categorify those definitions, using groupoid cardinality (a categorified version of rational number) and we figure out that the equation are even more simpler in homotopy type theory as for example one do not need to divide by $n!$ anymore. In the remaining part of the seminar I will explain how to get from this to a categorified version of the Euler product formula for Riemann zeta function and more generally for the Hasse-Weil zeta function of any commutative ring which are both idea of John Baez and James Dolan.
