nLab FinSet




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 FinSet\Fin\Set skeletal; there is one object for each natural number nn (including n=0n = 0), and a morphism from mm to nn is an mm-tuple (f 0,,f m1)(f_0, \ldots, f_{m-1}) of numbers satisfying 0f i<n0 \leq f_i \lt n. This amounts to identifying nn with the set {0,,n1}\{0, \ldots, n - 1\}. (Sometimes {1,,n}\{1, \ldots, n\} is used instead.)


Opposite category


The opposite category of FinSetFinSet is equivalent to that of finite Boolean algebras

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

This equivalence is induced by the power set-functor

𝒫:FinSet opFinBool. \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 FinSetFinSet 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 FinSetFinSet). However, all finite complete atomic Heyting algebras are Boolean.

Universal properties

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

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

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

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

The last fact is closely connected to this: FinSetFinSet, 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 opFinSet^{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(FinSet, +)^{op} is equivalent to the PROP for cocommutative comonoids.

Equivalence with the category of finite T 1T_1-topological spaces

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

In the other direction, to each preordered set (X,)(X, \leq) we may associate a topological space whose elements are those of XX, 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:PreOrdTopi \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 iSpeci \dashv Spec between the categories PreOrd and Top making PreOrdPreOrd a coreflective subcategory of TopTop. In particular, the adjunction counit evaluated at a space XX,

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

is the identity function at the level of sets, and is continuous because any open UU of XX 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 FinPreOrd\mathrm{FinPreOrd} and FinTop\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 T_1 -topological spaces is equality in T 1T_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 FinSet\mathrm{FinSet} of finite sets and FinT 1Sp\mathrm{Fin}T_1\mathrm{Sp} of finite T 1T_1-topological spaces.

In Grpd

FinSetFinSet 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)1+XF(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 FinSetFinSet is a vertical categorification of the poset \mathbb{N} of natural numbers.

As a groupoid itself, the core of FinSetFin 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.)

In topos theory

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

Mathematics done within or about FinSetFinSet is finite mathematics.

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

The copresheaf category [FinSet,Set][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 FinSetFinSet

The simplex category Δ\Delta embeds into FinSet\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 +FinSet_+ of nonempty finite sets is the multi-sorted Lawvere theory of unbiased boolean algebras. As a Lawvere theory, FinSetFinSet 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).


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

Last revised on September 10, 2023 at 13:13:16. See the history of this page for a list of all contributions to it.