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

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 $\Fin\Set$ 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)

category: category

Last revised on January 5, 2016 at 00:03:48. See the history of this page for a list of all contributions to it.