Classical Species [00BA]

    Groupoid cardinality as motivation

    1. Groupoid Cardinality [007L]

      Definition 1.1. Groupoid [007M]

        A groupoid is a category in which every morphism is an isomorphism.

        Example 1.2. finite Sets with bijections [007N]

          It is easy to see that the category of finite sets with bijections as morphisms forms a groupoid. We will denote this category with .

          Definition 1.3. Set [007O]

            We can view a set as the groupoid with the sets elements as objects and identity morphism only. Essentially a set is the most boring kind of groupoid we can think about since its points carry no symmetries.

            Definition 1.4. Coproduct of Groupoids [007W]

              TODO. Essentially just disjoint union.

              Lemma 1.5. [007Y]

                TODO. Cardinality of coproduct is sum of cardinality.

                Definition 1.6. Product of Groupoids [007X]

                  TODO. Objects are pairs of G and H, morphisms are pairs of morphisms.

                  Lemma 1.7. [007Z]

                    TODO. Cardinality of product is product of cardinality.

                    We now want to extend our definition of a cardinality from sets to groupoids. To make this a nice definition it should be invariant under equivalences.

                    Definition 1.8. Groupoid Cardinality [007P]

                      For the cardinality of a groupoid we pick a representative for each isomorphism class of objects in . Each representative then contributes to the formal sum by , where denotes the cardinality of the automorphism group of x. In symbols

                      In the case where is finite for all and the series converges we may evaluate it to a real number.

                      Remark 1.9. [007R]

                        Notice how the definition of groupoid cardinality is crafted explicitly to be an invariant with respect to equivalence of categories.

                        Proof. TODO

                        Consider for example the terminal category as well as the groupoid with two isomorphic objects and the obvious 4 morphisms. Both are equivalent as categories and indeed they both have cardinality 1.

                        Observation 1.10. rational cardinalities [007S]

                          Other than sets, proper Groupoids may admit non-integer cardinalities. The groupoid consisting of a single point with 3 automorphisms has cardinality .

                          Example 1.11. Eulers Number [007T]

                            The cardinality of the the groupoid of is eulers number .

                            Definition 1.12. Weak Quotient / action groupoid [007U]

                              TODO

                              1.13. |S//G| = |S|/|G| [007V]

                                Definition 1.14. Exponent [0080]

                                  TODO

                                  Species count the number of structure of a specific type that one can put on a finite set of labels. Formally we define a species as follows.

                                  Definition 2. Species [0081]

                                    A (combinatorial) species is a functor . Given a finite set of labels we let denote the set of -structures one can put on the set.

                                    Example 3. two-colorings [0082]

                                      TODO

                                      Example 4. graphs [0083]

                                        TODO

                                        The above are examples where there is only a finite number of ways to put a structure on a given finite set. But our definition of a species permits degenerate examples like the following.

                                        Example 5. not so tame species [0085]

                                          For a finite set define as the set of all real valued funcitons with domain .

                                          Definition 6. tame [0086]

                                            We call a species tame if is finite for every finite set .

                                            Idea 7. [0084]

                                              We consider the action groupoid of the symmetric group acting of F(n). This should give rise to the generating function of species quite naturally.

                                              –

                                              • generating functions

                                              • Coproduct

                                              • Hamard Product

                                              • Cauchy-Product

                                              • Catalan Numbers and binary rooted trees

                                              • species count things up to isomorphism

                                              -> univalence

                                              • species as dependent types