FinSet

$\Fin\Set$ is the category of finite sets and all functions between them: the full subcategory of Set on finite sets.

(For constructive purposes, take the strictest sense of ‘finite’.)

It is easy (and thus common) to make $\Fin\Set$ skeletal; there is one object for each natural number $n$ (including $n = 0$), and a morphism from $m$ to $n$ is an $m$-tuple $(f_0, \ldots, f_{m-1})$ of numbers satisfying $0 \leq f_i \lt n$. This amounts to identifying $n$ with the set $\{0, \ldots, n - 1\}$. (Sometimes $\{1, \ldots, n\}$ is used instead.)

The opposite category of $FinSet$ is equivalent to that of finite Boolean algebras

$FinSet^{op} \simeq FinBool
\,.$

This equivalence is induced by the power set-functor

$\mathcal{P} \;\colon\; FinSet^{op} \stackrel{\simeq}{\to} FinBool
\,.$

This is discussed for instance as (Awodey, prop. 7.31). For the generalization to all sets see at *Set – Properties – Opposite category and Boolean algebras*. See at *Stone duality* for more on this.

In constructive mathematics, for any flavor of *finite*, $\mathcal{P}$ defines an equivalence of $FinSet$ with the opposite category of that of those complete atomic Heyting algebras whose set of atomic elements is finite (in the same sense as in the definition of $FinSet$).

$FinSet$ is the free category with finite coproducts on one object: that is, for any category $C$ with finite coproducts and any object $c \in C$ there is a functor $F : FinSet \to C$ preserving finite coproducts with $F(1) = c$, and $F$ is unique up to natural isomorphism.

The first fact is closely connected to the fact that $FinSet$ is the vertical categorification of the set of natural numbers $\mathbb{N}$, and $\mathbb{N}$ is the free monoid on one generator.

$FinSet$ is also the free category with finite colimits on one object: that is, for any category $C$ with finite colimits and any object $c \in C$ there is a functor $F : FinSet \to C$ preserving finite colimits with $F(1) = c$, and $F$ is unique up to natural isomorphism.

$FinSet$ is also the free symmetric monoidal category on a commutative monoid object: that is, for any symmetric monoidal category $(C, \otimes)$ and any commutative monoid object $c \in C$ there is a symmetric monoidal functor $F : (FinSet,+) \to (C, \otimes)$ with $F(1) = c$, and $F$ is unique up to monoidal natural isomorphism.

The last fact is closely connected to this: $FinSet$, made symmetric monoidal using $+$, is equivalent to the PROP for commutative monoids. A proof is given in Lafont’s paper below. Moreover, the sub-prop generated by the unit of the monoid consists of the monics, while the free prop generated by the multiplication of the monoid are the epics.

All these universal properties have useful duals. $FinSet^{op}$ is the free category with finite products on one object and also the free category with finite limits on one object; the symmetric monoidal category $(FinSet, +)^{op}$ is equivalent to the PROP for cococommutative comonoids.

$FinSet$ is a natural numbers object in the (2,1)-topos Grpd of groupoids and functors, as it is an initial algebra of the 2-endofunctor $F(X) \cong 1 + X$. It is also a free monoid object on one generator in Grpd, an initial rig object? in Grpd, and a category. This all follows from the fact that the category $FinSet$ is a vertical categorification of the poset $\mathbb{N}$ of natural numbers.

As a groupoid itself, the core of $Fin Set$ is (with the operation of disjoint union) the free symmetric monoidal category on one object. (There is no way to generate non-invertible morphisms from this data.)

The category $FinSet$ is an elementary topos and the inclusion $FinSet \hookrightarrow Set$ is a logical morphism of toposes. (Elephant, example 2.1.2).

Mathematics done within or about $FinSet$ is finite mathematics.

A presheaf of sets on $\Fin\Set$ is a symmetric set; one generally uses the skeletal version of $\Fin\Set$ for this.

The copresheaf category $[FinSet,Set]$ is the classifying topos for the *theory of objects* (the empty theory over the signature with one sort and no primitive symbols except equality). (Elephant, D3.2).

The simplex category $\Delta$ embeds into $\Fin\Set$ as a category with the same objects but fewer morphisms. The category of cyclic sets introduced by Connes lies in between. All the three are special cases of extensions of $\Delta$ by a group in a particularly nice way. Full classification of allowed skew-simplicial sets has been given by Krasauskas and independently by Loday and Fiedorowicz.

The cartesian monoidal category $FinSet_+$ of nonempty finite sets is the multi-sorted Lawvere theory of unbiased boolean algebras. As a Lawvere theory, $FinSet$ has one more sort, corresponding to $\emptyset$, and one more model, in which every sort has exactly one element (in all the other models, the sort corresponding to $\emptyset$ is empty).

- Steve Awodey,
*Category Theory – lecture 7*(pdf)

- Yves Lafont, Towards an algebraic theory of Boolean circuits, February 12, 2013. (pdf)

category: category