Functorial Composition of Species

Definition 8.14. [BLL98, chp. 2.2] Let F and G be two species of structures. The species F ⊓ ⊔ G (also denoted F[G]), called the functorial composite of F and G, is defined as

(49)

for any finite set U.

ToDo ⊲ 34 ⊳

rhx ⊲ 23 ⊳ 02-Mar-2007: Add transport condition due to [BLL98, chp. 2.2].

Type Constructor

FunctorialCompose

Description

Construct the functorial composite of combinatorial species.

191a⟨dom: FunctorialCompose 191a⟩≡   (55)
FunctorialCompose(
    F: SPECIES,
    G: SPECIES
)(L: LabelType): CombinatorialSpecies(L) == add {
        Rep == F G L;
        import from Rep;
        ⟨implementation: FunctorialCompose 191b⟩
}

Defines:
FunctorialCompose, used in chunk 655.

Uses CombinatorialSpecies 71, LabelType 62, and SPECIES 55.

191b⟨implementation: FunctorialCompose 191b⟩≡ (191a) 191c ⊳
(tw: TextWriter) << (x: %): TextWriter == tw << rep(x);

191c⟨implementation: FunctorialCompose 191b⟩+≡ (191a) ⊲191b 192a ⊳
(x: %) = (y: %): Boolean == rep x = rep y;

192a⟨implementation: FunctorialCompose 191b⟩+≡   (191a)  ⊲191c  192b ⊳
generatingSeries: ExponentialGeneratingSeries == new();
isomorphismTypeGeneratingSeries: OrdinaryGeneratingSeries == new();
cycleIndexSeries: CycleIndexSeries == new();
expression: SpeciesExpression == new();
local init(): () == {
        set!(generatingSeries $ %,
            functorialCompose(generatingSeries $ F(L), generatingSeries $ G(L))
        );
        set!(
            cycleIndexSeries $ %,
            functorialCompose(cycleIndexSeries $ F(L), cycleIndexSeries $ G(L))
        );
        set!(
            isomorphismTypeGeneratingSeries $ %,
            (cycleIndexSeries $ %) :: OrdinaryGeneratingSeries
        );
        set!(expression$%, compose(expression$F(L), expression$G(L)));
}
init();

Uses CycleIndexSeries 330, ExponentialGeneratingSeries 316, OrdinaryGeneratingSeries 311, and SpeciesExpression 430.

192b⟨implementation: FunctorialCompose 191b⟩+≡   (191a)  ⊲192a  192c ⊳
structures(s: SetSpecies L): Generator % == generate {
        import from List G L;
        gs: SetSpecies G L := set [structures(s)$G(L)];
        for x in structures(gs) $ F(G L) repeat yield per x;
}

Uses Generator 617 and SetSpecies 117.

8.13 Functorial Composition of Species