Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Definition of dirichlet series #626

Merged
merged 6 commits into from
May 22, 2023
Merged

Definition of dirichlet series #626

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c50a02f
I have cleaned the file dirichlet-products-species-of-types-in-subuni…
VictorBlanchi May 19, 2023
01052fc
make pre-commit
VictorBlanchi May 19, 2023
662c5c7
Reviews
VictorBlanchi May 19, 2023
e8e5c99
Pre-commit
VictorBlanchi May 19, 2023
1cd8c14
product -> products
VictorBlanchi May 19, 2023
6ffaf87
Merge branch 'master' into dirichlet-series
fredrik-bakke May 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 4 additions & 0 deletions src/species.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,8 @@ open import species.coproducts-species-of-types-in-subuniverses public
open import species.cycle-index-series-species-of-types public
open import species.derivatives-species-of-types public
open import species.dirichlet-products-species-of-types-in-subuniverses public
open import species.dirichlet-series-species-of-finite-inhabited-types public
open import species.dirichlet-series-species-of-types-in-subuniverses public
open import species.equivalences-species-of-types public
open import species.equivalences-species-of-types-in-subuniverses public
open import species.exponentials-cauchy-series-of-types public
Expand All @@ -32,6 +34,8 @@ open import species.pointing-species-of-types public
open import species.precategory-of-finite-species public
open import species.products-cauchy-series-species-of-types public
open import species.products-cauchy-series-species-of-types-in-subuniverses public
open import species.products-dirichlet-series-species-of-finite-inhabited-types public
open import species.products-dirichlet-series-species-of-types-in-subuniverses public
open import species.small-cauchy-composition-species-of-finite-inhabited-types public
open import species.small-cauchy-composition-species-of-types-in-subuniverses public
open import species.species-of-finite-inhabited-types public
Expand Down
178 changes: 86 additions & 92 deletions src/species/dirichlet-products-species-of-types-in-subuniverses.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,85 +40,97 @@ dirichlet product is also a species of subuniverse from `P` to `Q`

## Definition

### The underlying type of the Dirichlet product of species in a subuniverse

```agda
module _
{l1 l2 l3 : Level} (P : subuniverse l1 l1) (Q : global-subuniverse id)
{l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
where

dirichlet-product-species-subuniverse' :
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l2))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(X : type-subuniverse P) → UU (lsuc l1 ⊔ l2 ⊔ l3)
dirichlet-product-species-subuniverse' S T X =
type-dirichlet-product-species-subuniverse :
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
(X : type-subuniverse P) → UU (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4)
type-dirichlet-product-species-subuniverse S T X =
Σ ( binary-product-Decomposition P X)
( λ d →
inclusion-subuniverse ( subuniverse-global-subuniverse Q l2)
( S (left-summand-binary-product-Decomposition P X d)) ×
inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( S (left-summand-binary-product-Decomposition P X d)) ×
inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
( T (right-summand-binary-product-Decomposition P X d)))
```

### Subuniverses closed under the Dirichlet product of species in a subuniverse

```agda
is-closed-under-dirichlet-product-species-subuniverse :
{l1 l2 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id) →
UUω
is-closed-under-dirichlet-product-species-subuniverse {l1} {l2} P Q =
{l3 l4 : Level}
(S : species-subuniverse P (subuniverse-global-subuniverse Q l3))
(T : species-subuniverse P (subuniverse-global-subuniverse Q l4))
(X : type-subuniverse P) →
is-in-subuniverse
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
( type-dirichlet-product-species-subuniverse P Q S T X)
```

### The Dirichlet product of species of types in a subuniverse

```agda
module _
{l1 l2 l3 : Level} (P : subuniverse l1 l1) (Q : global-subuniverse id)
( C1 :
( (l4 l5 : Level)
(S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
(T : species-subuniverse P (subuniverse-global-subuniverse Q l5))
(X : type-subuniverse P) →
is-in-subuniverse
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l4 ⊔ l5))
( dirichlet-product-species-subuniverse' P Q S T X)))
{l1 l2 l3 l4 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
where

dirichlet-product-species-subuniverse :
species-subuniverse P ( subuniverse-global-subuniverse Q l2) →
species-subuniverse P ( subuniverse-global-subuniverse Q l3) →
species-subuniverse P ( subuniverse-global-subuniverse Q l4) →
species-subuniverse P
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3))
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
pr1 (dirichlet-product-species-subuniverse S T X) =
dirichlet-product-species-subuniverse' P Q S T X
pr2 (dirichlet-product-species-subuniverse S T X) = C1 l2 l3 S T X
type-dirichlet-product-species-subuniverse P Q S T X
pr2 (dirichlet-product-species-subuniverse S T X) = C1 S T X
```

## Properties

```agda
module _
{l1 l2 l3 l4 : Level} (P : subuniverse l1 l1) (Q : global-subuniverse id)
( C1 :
(l5 l6 : Level)
(S : species-subuniverse P (subuniverse-global-subuniverse Q l5))
(T : species-subuniverse P (subuniverse-global-subuniverse Q l6))
(X : type-subuniverse P) →
is-in-subuniverse
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l5 ⊔ l6))
( dirichlet-product-species-subuniverse' P Q S T X))
{l1 l2 l3 l4 l5 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
( C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
( C2 : is-closed-under-products-subuniverse P)
where

module _
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l2))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(U : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
(U : species-subuniverse P ( subuniverse-global-subuniverse Q l5))
(X : type-subuniverse P)
where

equiv-left-iterated-dirichlet-product-species-subuniverse :
dirichlet-product-species-subuniverse' P Q
type-dirichlet-product-species-subuniverse P Q
( dirichlet-product-species-subuniverse P Q C1 S T)
( U)
( X) ≃
Σ ( ternary-product-Decomposition P X)
( λ d →
inclusion-subuniverse ( subuniverse-global-subuniverse Q l2)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( S (first-summand-ternary-product-Decomposition P X d)) ×
( inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
( T (second-summand-ternary-product-Decomposition P X d)) ×
inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l5)
( U (third-summand-ternary-product-Decomposition P X d))))
equiv-left-iterated-dirichlet-product-species-subuniverse =
( ( equiv-Σ
( λ d →
inclusion-subuniverse ( subuniverse-global-subuniverse Q l2)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( S (first-summand-ternary-product-Decomposition P X d)) ×
( inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
( T (second-summand-ternary-product-Decomposition P X d)) ×
inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l5)
( U (third-summand-ternary-product-Decomposition P X d)))))
( ( equiv-Σ
( _)
Expand All @@ -137,17 +149,17 @@ module _
( ( equiv-tot λ d → right-distributive-prod-Σ))))

equiv-right-iterated-dirichlet-product-species-subuniverse :
dirichlet-product-species-subuniverse' P Q
type-dirichlet-product-species-subuniverse P Q
( S)
( dirichlet-product-species-subuniverse P Q C1 T U)
( X) ≃
Σ ( ternary-product-Decomposition P X)
( λ d →
inclusion-subuniverse ( subuniverse-global-subuniverse Q l2)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( S (first-summand-ternary-product-Decomposition P X d)) ×
( inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
( T (second-summand-ternary-product-Decomposition P X d)) ×
inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l5)
( U (third-summand-ternary-product-Decomposition P X d))))
equiv-right-iterated-dirichlet-product-species-subuniverse =
( ( equiv-Σ-equiv-base
Expand All @@ -160,11 +172,11 @@ module _
( ( equiv-tot (λ d → left-distributive-prod-Σ)))))

equiv-associative-dirichlet-product-species-subuniverse :
dirichlet-product-species-subuniverse' P Q
type-dirichlet-product-species-subuniverse P Q
( dirichlet-product-species-subuniverse P Q C1 S T)
( U)
( X) ≃
dirichlet-product-species-subuniverse' P Q
type-dirichlet-product-species-subuniverse P Q
( S)
( dirichlet-product-species-subuniverse P Q C1 T U)
( X)
Expand All @@ -173,9 +185,9 @@ module _
equiv-left-iterated-dirichlet-product-species-subuniverse

module _
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l2))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(U : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
(U : species-subuniverse P ( subuniverse-global-subuniverse Q l5))
where

associative-dirichlet-product-species-subuniverse :
Expand All @@ -187,7 +199,7 @@ module _
( dirichlet-product-species-subuniverse P Q C1 T U)
associative-dirichlet-product-species-subuniverse =
eq-equiv-fam-subuniverse
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5))
( dirichlet-product-species-subuniverse P Q C1
( dirichlet-product-species-subuniverse P Q C1 S T)
( U))
Expand All @@ -201,31 +213,24 @@ module _

```agda
module _
{l1 l2 l3 : Level}
(P : subuniverse l1 l1)
{l1 l2 l3 l4 : Level}
(P : subuniverse l1 l2)
(Q : global-subuniverse id)
( C1 :
( (l4 l5 : Level)
(S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
(T : species-subuniverse P (subuniverse-global-subuniverse Q l5))
(X : type-subuniverse P) →
is-in-subuniverse
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l4 ⊔ l5))
( dirichlet-product-species-subuniverse' P Q S T X)))
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l2))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
(T : species-subuniverse P ( subuniverse-global-subuniverse Q l4))
where

equiv-commutative-dirichlet-product-species-subuniverse :
(X : type-subuniverse P) →
dirichlet-product-species-subuniverse' P Q S T X ≃
dirichlet-product-species-subuniverse' P Q T S X
type-dirichlet-product-species-subuniverse P Q S T X ≃
type-dirichlet-product-species-subuniverse P Q T S X
equiv-commutative-dirichlet-product-species-subuniverse X =
equiv-Σ
( λ d →
inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l4)
( T (left-summand-binary-product-Decomposition P X d)) ×
inclusion-subuniverse ( subuniverse-global-subuniverse Q l2)
inclusion-subuniverse ( subuniverse-global-subuniverse Q l3)
( S (right-summand-binary-product-Decomposition P X d)))
( equiv-commutative-binary-product-Decomposition P X)
( λ _ → commutative-prod)
Expand All @@ -235,7 +240,7 @@ module _
dirichlet-product-species-subuniverse P Q C1 T S
commutative-dirichlet-product-species-subuniverse =
eq-equiv-fam-subuniverse
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3))
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l2 ⊔ l3 ⊔ l4))
( dirichlet-product-species-subuniverse P Q C1 S T)
( dirichlet-product-species-subuniverse P Q C1 T S)
( equiv-commutative-dirichlet-product-species-subuniverse)
Expand All @@ -245,53 +250,44 @@ module _

```agda
unit-dirichlet-product-species-subuniverse :
{l1 : Level} →
(P Q : subuniverse l1 l1) →
{l1 l2 l3 : Level} →
(P : subuniverse l1 l2) (Q : subuniverse l1 l3) →
( (X : type-subuniverse P) →
is-in-subuniverse Q ( is-contr (inclusion-subuniverse P X))) →
species-subuniverse P Q
unit-dirichlet-product-species-subuniverse P Q C X =
is-contr (inclusion-subuniverse P X) , C X

module _
{l1 l2 : Level} (P : subuniverse l1 l1) (Q : global-subuniverse id)
(C1 :
( (l4 l5 : Level)
(S : species-subuniverse P (subuniverse-global-subuniverse Q l4))
(T : species-subuniverse P (subuniverse-global-subuniverse Q l5))
(X : type-subuniverse P) →
is-in-subuniverse
( subuniverse-global-subuniverse Q (lsuc l1 ⊔ l4 ⊔ l5))
( dirichlet-product-species-subuniverse' P Q S T X)))
{l1 l2 l3 : Level} (P : subuniverse l1 l2) (Q : global-subuniverse id)
(C1 : is-closed-under-dirichlet-product-species-subuniverse P Q)
(C2 : is-in-subuniverse P (raise-unit l1))
(C3 :
(X : type-subuniverse P) →
is-in-subuniverse
( subuniverse-global-subuniverse Q l1)
( is-contr (inclusion-subuniverse P X)))
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l2))
(S : species-subuniverse P ( subuniverse-global-subuniverse Q l3))
where

equiv-right-unit-law-dirichlet-product-species-subuniverse :
{l : Level} →
(S : species-subuniverse P (subuniverse-global-subuniverse Q l)) →
(X : type-subuniverse P) →
dirichlet-product-species-subuniverse' P Q
type-dirichlet-product-species-subuniverse P Q
( S)
( unit-dirichlet-product-species-subuniverse
( P)
( subuniverse-global-subuniverse Q l1)
( C3))
( X) ≃
inclusion-subuniverse (subuniverse-global-subuniverse Q l) (S X)
equiv-right-unit-law-dirichlet-product-species-subuniverse {l} S X =
inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S X)
equiv-right-unit-law-dirichlet-product-species-subuniverse X =
( ( left-unit-law-Σ-is-contr
( is-contr-total-equiv-subuniverse P X)
( X , id-equiv)) ∘e
( ( equiv-Σ-equiv-base
( λ p →
inclusion-subuniverse
( subuniverse-global-subuniverse Q l)
( subuniverse-global-subuniverse Q l3)
( S (pr1 (p))))
( equiv-is-contr-right-summand-binary-product-Decomposition
P
Expand All @@ -309,7 +305,7 @@ module _
( right-summand-binary-product-Decomposition P X d)))
( λ z →
inclusion-subuniverse
( subuniverse-global-subuniverse Q l)
( subuniverse-global-subuniverse Q l3)
( S
( left-summand-binary-product-Decomposition
P
Expand All @@ -318,19 +314,17 @@ module _
( ( equiv-tot (λ _ → commutative-prod))))))

equiv-left-unit-law-dirichlet-product-species-subuniverse :
{l : Level} →
(S : species-subuniverse P (subuniverse-global-subuniverse Q l)) →
(X : type-subuniverse P) →
dirichlet-product-species-subuniverse' P Q
type-dirichlet-product-species-subuniverse P Q
( unit-dirichlet-product-species-subuniverse
( P)
( subuniverse-global-subuniverse Q l1)
( C3))
( S)
( X) ≃
inclusion-subuniverse (subuniverse-global-subuniverse Q l) (S X)
equiv-left-unit-law-dirichlet-product-species-subuniverse {l} S X =
equiv-right-unit-law-dirichlet-product-species-subuniverse S X ∘e
inclusion-subuniverse (subuniverse-global-subuniverse Q l3) (S X)
equiv-left-unit-law-dirichlet-product-species-subuniverse X =
equiv-right-unit-law-dirichlet-product-species-subuniverse X ∘e
equiv-commutative-dirichlet-product-species-subuniverse
( P)
( Q)
Expand Down