Products of Dirichlet series of species of types in subuniverses

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

Created on 2023-05-22.
Last modified on 2024-02-06.

module species.products-dirichlet-series-species-of-types-in-subuniverses where
Imports 
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-dependent-pair-types
open import foundation.global-subuniverses
open import foundation.homotopies
open import foundation.postcomposition-functions
open import foundation.subuniverses
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universal-property-cartesian-product-types
open import foundation.universe-levels

open import species.dirichlet-products-species-of-types-in-subuniverses
open import species.dirichlet-series-species-of-types-in-subuniverses
open import species.species-of-types-in-subuniverses

Idea

The product of two Dirichlet series is the pointwise product.

Definition

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  (C1 : is-closed-under-products-subuniverse P)
  (H : species-subuniverse-domain l5 P)
  (C2 : preserves-product-species-subuniverse-domain P C1 H)
  (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  (X : UU l6)
  where

  product-dirichlet-series-species-subuniverse :
    UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
  product-dirichlet-series-species-subuniverse =
    dirichlet-series-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q l3)
      ( C1)
      ( H)
      ( C2)
      ( S)
      ( X) ×
    dirichlet-series-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q l4)
      ( C1)
      ( H)
      ( C2)
      ( T)
      ( X)

Properties

The Dirichlet series associated to the Dirichlet product of S and T is equal to the product of their Dirichlet series

module _
  {l1 l2 l3 l4 l5 : Level}
  (P : subuniverse l1 l2)
  (Q : global-subuniverse (λ l → l))
  (C1 : is-closed-under-products-subuniverse P)
  (H : species-subuniverse-domain l5 P)
  (C2 : preserves-product-species-subuniverse-domain P C1 H)
  (C3 : is-closed-under-dirichlet-product-species-subuniverse P Q)
  (C4 : is-closed-under-coproducts-subuniverse P)
  (S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
  (T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
  (X : UU l5)
  where

  private
    reassociate :
      dirichlet-series-species-subuniverse
        ( P)
        ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
        ( C1)
        ( H)
        ( C2)
        ( dirichlet-product-species-subuniverse P Q C3 S T) X ≃
      Σ ( type-subuniverse P)
        ( λ A →
          Σ ( type-subuniverse P)
            ( λ B →
              Σ ( Σ ( type-subuniverse P)
                    ( λ F →
                      inclusion-subuniverse P F ≃
                      ( inclusion-subuniverse P A × inclusion-subuniverse P B)))
                ( λ F →
                  ( ( inclusion-subuniverse
                      ( subuniverse-global-subuniverse Q l3)
                      ( S A)) ×
                    ( inclusion-subuniverse
                      ( subuniverse-global-subuniverse Q l4)
                      ( T B))) × (X → H (pr1 F)))))
    pr1 reassociate (F , ((A , B , e) , x) , y) = (A , B , (F , e) , x , y)
    pr2 reassociate =
      is-equiv-is-invertible
        ( λ (A , B , (F , e) , x , y) → (F , ((A , B , e) , x) , y))
        ( refl-htpy)
        ( refl-htpy)

    reassociate' :
      Σ ( type-subuniverse P)
        ( λ A →
          Σ ( type-subuniverse P)
            ( λ B →
              ( ( inclusion-subuniverse
                  ( subuniverse-global-subuniverse Q l3)
                  ( S A)) ×
                inclusion-subuniverse
                  ( subuniverse-global-subuniverse Q l4)
                  ( T B)) ×
              ( (X → H A) × (X → H B)))) ≃
      product-dirichlet-series-species-subuniverse P Q C1 H C2 S T X
    pr1 reassociate' (A , B , (s , t) , (fs , ft)) =
      ((A , (s , fs)) , (B , (t , ft)))
    pr2 reassociate' =
      is-equiv-is-invertible
        ( λ ((A , (s , fs)) , (B , (t , ft))) →
          (A , B , (s , t) , (fs , ft)))
        ( refl-htpy)
        ( refl-htpy)

  equiv-dirichlet-series-dirichlet-product-species-subuniverse :
    dirichlet-series-species-subuniverse
      ( P)
      ( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
      ( C1)
      ( H)
      ( C2)
      ( dirichlet-product-species-subuniverse P Q C3 S T)
      ( X) ≃
    product-dirichlet-series-species-subuniverse P Q C1 H C2 S T X
  equiv-dirichlet-series-dirichlet-product-species-subuniverse =
    ( reassociate') ∘e
    ( ( equiv-tot
        ( λ A →
          equiv-tot
            ( λ B →
              ( equiv-product
                ( id-equiv)
                ( equiv-up-product ∘e equiv-postcomp X (C2 A B))) ∘e
              left-unit-law-Σ-is-contr
                ( is-torsorial-equiv-subuniverse'
                  ( P)
                  ( inclusion-subuniverse P A ×
                    inclusion-subuniverse P B ,
                    C1
                      ( is-in-subuniverse-inclusion-subuniverse P A)
                      ( is-in-subuniverse-inclusion-subuniverse P B)))
                ( ( inclusion-subuniverse P A × inclusion-subuniverse P B ,
                    C1
                      ( is-in-subuniverse-inclusion-subuniverse P A)
                      ( is-in-subuniverse-inclusion-subuniverse P B)) ,
                  id-equiv)))) ∘e
      ( reassociate))

Recent changes