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-02-14.

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

Σ (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 : 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 equal to 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