Cycle index series of species
Content created by Egbert Rijke, Fredrik Bakke and Victor Blanchi.
Created on 2023-03-21.
Last modified on 2023-10-09.
module species.cycle-index-series-species-of-types where
Imports
open import elementary-number-theory.natural-numbers open import foundation.dependent-pair-types open import foundation.universe-levels open import univalent-combinatorics.cyclic-finite-types
Idea
The cycle index series of a species of types F
is a type family indexed by
finite families of cyclic types. Note that a finite family of cyclic types Cᵢ
uniquely determines a permutation e
on the disjoint union C := Σᵢ Cᵢ
of the
underlying types of the Cᵢ
. This permutation determines an action F e
on
F C
. The cycle index series of F
at the family Cᵢ
is the type Fix (F e)
of fixed points of F e
.
Definition
total-type-family-of-cyclic-types : {l1 l2 : Level} (X : UU l1) (C : X → Σ ℕ (Cyclic-Type l2)) → UU (l1 ⊔ l2) total-type-family-of-cyclic-types X C = Σ X (λ x → type-Cyclic-Type (pr1 (C x)) (pr2 (C x))) {- permutation-family-of-cyclic-types : {l1 l2 : Level} (X : 𝔽 l1) (C : type-𝔽 X → Σ ℕ (Cyclic-Type l2)) → Aut (total-type-family-of-cyclic-types X C) permutation-family-of-cyclic-types X C = {!!} cycle-index-series-species-types : {l1 l2 : Level} (F : species-types l1 l2) (X : 𝔽 l1) → (type-𝔽 X → Σ ℕ (Cyclic-Type {!!} ∘ succ-ℕ)) → UU {!!} cycle-index-series-species-types F X C = Σ {!F (total-type-family-of-cyclic-types X C)!} {!!} -}
Recent changes
- 2023-10-09. Egbert Rijke. Navigation tables for all files related to cyclic types, groups, and rings (#823).
- 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
- 2023-03-21. Victor Blanchi. Associativity of species composition (#478).