nLab
FinSet

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

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

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

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

References

category: category

Revised on April 11, 2014 09:26:38 by Ingo Blechschmidt (137.250.162.16)