nLab
FinSet

Definition

$FinSet$ 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 $FinSet$ 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,\dots ,f_{m-1})$ of numbers satisfying $0\le f_i<n$. This amounts to identifying $n$ with the set $\{0,\dots ,n-1\}$. (Sometimes $\{1,\dots ,n\}$ is used instead.)

Subcategories of $\mathrm{FinSet}$

The simplex category $\Delta$ embeds into $FinSet$ 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 ${\mathrm{FinSet}}_{+}$ of nonempty finite sets is the multi-sorted Lawvere theory of unbiased boolean algebras. As a lawvere theory, $\mathrm{FinSet}$ has one more sort, corresponding to $\varnothing$, and one more model, in which every sort has exactly one element (in all the other models, the sort corresponding to $\varnothing$ is empty).

In topos theory

The category $\mathrm{FinSet}$ is an elementary topos and the inclusion $\mathrm{FinSet}\hookrightarrow \mathrm{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 $FinSet$ is a symmetric set; one generally uses the skeletal version of $FinSet$ for this.

The copresheaf category $[\mathrm{FinSet},\mathrm{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).

Properties

Opposite category

Proposition

The opposite category of $\mathrm{FinSet}$ is equivalent to that of finite Boolean algebras

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

This equivalence is induced by the power set-functor

$$𝒫:{\mathrm{FinSet}}^{\mathrm{op}}\stackrel{\simeq }{\to }\mathrm{FinBool}.$$\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.

References

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

category: category