# Dirichlet series of species of types

Content created by Fredrik Bakke, Egbert Rijke and Victor Blanchi.

Created on 2023-06-08.
Last modified on 2023-06-09.

module species.dirichlet-series-species-of-types where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import species.species-of-types


## Idea

In classical mathematics, the Dirichlet series of a species of finite inhabited types T is the formal series in s :

Σ (n : ℕ∖{0}) (|T({1,...,n}| n^(-s) / n!))


If s is a negative integer, the categorified version of this formula is

Σ (F : 𝔽 ∖ {∅}), T (F) × (S → F)


We can generalize it to species of types as

Σ (U : UU) (T (U) × (S → U))


The interesting case is when s is a positive number. The categorified version of this formula then becomes

Σ ( n : ℕ ∖ {0}),
( Σ (F : UU-Fin n) , T (F) × (S → cycle-prime-decomposition-ℕ (n))


We can generalize the two notions to species of types in subuniverses. Let P and Q two subuniverse such that P is closed by cartesian product. Let H : P → UU be a species such that for every X , Y : P the following equality is satisfied H (X × Y) ≃ H X × H Y. Then we can define the H-Dirichlet series to any species of subuniverse T by

Σ (X : P) (T (X) × (S → H (X)))


The condition on H ensure that all the usual properties of the Dirichlet series are satisfied.

## Definition

module _
{l1 l2 l3 l4 : Level}
(H : species-types l1 l2)
(C1 : preserves-product-species-types H)
(T : species-types l1 l3)
(S : UU l4)
where

dirichlet-series-species-types : UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
dirichlet-series-species-types = Σ (UU l1) (λ X → (T X) × (S → H (X)))