nLab
FinSet

Contents

Contents

Definition

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

Properties

Opposite category

Proposition

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.

Remark

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

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 cococommutative comonoids.

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 tye fact that the category FinSetFinSet is the vertical categorification of the poset \mathbb{N} of natural numbers.

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

References

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

Last revised on May 3, 2021 at 22:25:59. See the history of this page for a list of all contributions to it.