nLab FinSet

Definition

$\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.)

Properties

Opposite category

Proposition

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.

Remark

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$). However, all finite complete atomic Heyting algebras are Boolean.

Universal properties

$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 cocommutative comonoids.

$FinSet$ is also the free strict mononoidal category on a symmetric monoid object (see Grandis 01).

Equivalence with the category of finite $T_1$-topological spaces

Given a continuous map $f \colon X \to Y$ between topological spaces, it is order-preserving relative to the specialisation order. Thus, we have a faithful functor $Spec$ from the category of $\mathrm{Top}$ of topological spaces to the category $\mathrm{PreOrd}$ of preordered sets.

In the other direction, to each preordered set $(X, \leq)$ we may associate a topological space whose elements are those of $X$, and whose open subsets are precisely the upward-closed sets with respect to the preordered set. This topology is called the specialization topology. This defines a functor

$$i \colon PreOrd \to Top$$

which is a full embedding; the essential image of this functor is the category of Alexandroff spaces (spaces in which an arbitrary intersection of open sets is open). Hence the category of preorders is equivalent to the category of Alexandroff spaces.

There is an an adjunction $i \dashv Spec$ between the categories PreOrd and Top making $PreOrd$ a coreflective subcategory of $Top$. In particular, the adjunction counit evaluated at a space $X$,

$$i(Spec(X)) \to X,$$

is the identity function at the level of sets, and is continuous because any open $U$ of $X$ is upward-closed with respect to $\leq$, according to the second equivalent condition of the definition of the specialization order.

This adjunction restricts to an adjoint equivalence between the categories $\mathrm{FinPreOrd}$ and $\mathrm{FinTop}$ of finite preordered sets and finite topological spaces. The unit and counit are both identity functions on underlying sets, so that in fact we have an equivalence between these categories as concrete categories.

Since the specialization order of $T_1$-topological spaces is equality in $T_1$-spaces, and every subset is upward-closed with respect to the equality relation used to define the specialization topology of a set, the above adjunction further restricts to an adjoint equivalence between the categories $\mathrm{FinSet}$ of finite sets and $\mathrm{Fin}T_1\mathrm{Sp}$ of finite $T_1$-topological spaces.

In Grpd

$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 $FinSet$ 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.)

In topos theory

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).

Subcategories of $FinSet$

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.

As a Lawvere theory

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).

Related concepts

• permutation category

• braid category

• finite homotopy type

• FinRel

• FinInj

• axiom of finiteness

References

• Steve Awodey, Category Theory – lecture 7 (pdf)

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

• Marco Grandis, Finite sets and symmetric simplicial sets, Theory and Applications of Categories 8 (2001): 244-252.

category: category