Overview [00DS]
Overview [00DS]
This note attempts to state a HoTTification of the key results from the paper Dirichlet Species and Arithmetic Zeta Functions. Some things I say here may simply be wrong because I have not proved most of what I am claiming here. This serves more as a roadmap than as a collection of results.
Definition 1. Species on FinSet [00DT]
Definition 1. Species on FinSet [00DT]
A species is a function , where is the groupoid of finite sets and bijections.
Definition 3. Groupoid Cardinality of 1-types [00ER]
Definition 3. Groupoid Cardinality of 1-types [00ER]
Let be a 1-type such that is finite, and for all is finite. Define the groupoid cardinality of as the rational number
where denotes a finite sum over rational numbers indexed by the finite set .
4. Dirichlet Series [00F1]
4. Dirichlet Series [00F1]
For a dirichlet species define
where is the dirichlet type of , and is the groupoid cardinality of the n-th component of the dirichlet type. We call the dirichlet series of , and the -th summand.
Definition 5. Dirichlet Product Species [00DP]
Definition 5. Dirichlet Product Species [00DP]
Given species define the dirichlet product by
where is the type of cartesian decompositions of .
TODO 6. Dirichlet series of dirichlet product of species is dirchlet product of dirichlet series [00FA]
TODO 6. Dirichlet series of dirichlet product of species is dirchlet product of dirichlet series [00FA]
i.e
clearly
To continue here we must first make progress on the groupoid cardinality of the dirichlet product of F and G, for that look at group action of on cartesian decompositions
TODO 7. Definition Dirichlet Power [00FE]
TODO 7. Definition Dirichlet Power [00FE]
TODO
TODO 8. Definition Dirichlet exponential [00FG]
TODO 8. Definition Dirichlet exponential [00FG]
Definition 9. Euler Product of Species [00FI]
Definition 9. Euler Product of Species [00FI]
For type family of species indexed by with a p-local dirichlet species.
TODO 10. [00FJ]
TODO 10. [00FJ]
11. Zeta Species [00EC]
11. Zeta Species [00EC]
Given , define
where is the underlying type of . See also Hasse-Weil species in agda-unimath
12. [00FP]
12. [00FP]
TODO 13. [00FQ]
TODO 13. [00FQ]
14. [00FR]
14. [00FR]
Define an -structure on a finite set to be a way of making that set into a field of characteristic and then choose an element of .
TODO 15. [00FS]
TODO 15. [00FS]
TODO 16. Main Theorem [00EF]
TODO 16. Main Theorem [00EF]
The zeta species and the eulerproduct on the right hand side are isomorphic as types.