Dirichlet series of species of finite inhabited types

Content created by Fredrik Bakke and Victor Blanchi.

Created on 2023-05-22.
Last modified on 2025-08-30.

module species.dirichlet-series-species-of-finite-inhabited-types where
Imports 
open import elementary-number-theory.natural-numbers

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

open import species.species-of-finite-inhabited-types

open import univalent-combinatorics.cycle-prime-decomposition-natural-numbers
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.inhabited-finite-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 : Finite-Type∖{∅}), T(F) × (S → F).

We can generalize it to species of types as

  Σ (X : UU) (T(X) × (S → X)).

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

  Σ ( n : ℕ∖{0}),
    ( Σ ( F : Type-With-Cardinality-ℕ n) ,
        ( T(F) × (S → cycle-prime-decomposition-ℕ n)).

We have picked the concrete group cycle-prime-decomposition-ℕ n because it is closed under cartesian product and also because its groupoid cardinality is 1/n.

Definition

dirichlet-series-species-Inhabited-Finite-Type :
  {l1 l2 l3 : Level} → species-Inhabited-Finite-Type l1 l2 → UU l3 →
  UU (lsuc l1 ⊔ l2 ⊔ l3)
dirichlet-series-species-Inhabited-Finite-Type {l1} T S =
  Σ ( ℕ)
    ( λ n →
      Σ ( Type-With-Cardinality-ℕ l1 (succ-ℕ n))
        ( λ F →
          ( type-Finite-Type
            ( T
              ( type-Type-With-Cardinality-ℕ (succ-ℕ n) F ,
                is-finite-and-inhabited-type-Type-With-Cardinality-ℕ-succ-ℕ
                  n
                  F))) ×
          ( S → cycle-prime-decomposition-ℕ (succ-ℕ n) _)))

Recent changes