finite set



A finite set is, roughly speaking, a set with only finitely many elements. There are a number of ways to make this precise.

Classically, the finite sets are the finitely presentable objects in Set. Constructively, the same is true if finitely presented is properly interpreted, see there for details.

The category FinSet of finite sets and functions between them is a prime example of an elementary topos which is not a Grothendieck topos. It is essentially the subject matter of combinatorics; it is fundamental in the subject of structure types.


Standard definition

We can for example make the following definition.


A finite set is a set AA for which there exists a bijection between AA and the set [n]{k|k<n}[n] \coloneqq \{k\in \mathbb{N} | k\lt n\} for some nn\in \mathbb{N}, where \mathbb{N} is the natural numbers.

Finiteness constructively and internally


In constructive mathematics, and internally to a topos, a number of classically equivalent notions of finiteness become distinguishable:

In constructive mathematics, one is usually interested in the finite sets, although the finitely indexed sets are also sometimes useful, as are the Dedekind-finite sets in the second sense.

Properties and relationships

Of course, we have

finitelyindexed finite subfinitelyindexed subfinite \array{ & & finitely\;indexed\\ & \neArrow & & \seArrow\\ finite & & & & subfinitely\;indexed\\ & \seArrow & & \neArrow\\ & & subfinite }


Finiteness without infinity

All of the above definitions except for Dedekind-finiteness only make sense given the set of natural numbers, i.e., given an axiom of infinity. However, they can all be rephrased to make sense even without an axiom of infinity (and thus in a topos without a natural numbers object). Basically, you define (for a given set SS) the concept of ‘collection of subsets of SS that includes all of the finite subsets’ by requiring it to be closed under inductive operations appropriate for the sense of ‘finite’ that you want; then SS is finite if and only if it is an element of all such collections. Namely, for any set SS we define the following subsets of the power set P(S)P(S).

Challenge: Finiteness predicatively without infinity

Can you think of a way to define these notions of finite without power objects and without a natural numbers object? More specifically (and generously), can you define them in an arbitrary locally cartesian closed pretopos with enough projectives?

In a topos

In a topos, there are both “external” and “internal” versions of all the above notions of finiteness, depending on whether we interpret their meaning “globally” or in the internal logic of the topos. See finite object.

Properties of the category of finite sets

The category FinSet of finite sets is equivalent to that of finite Boolean algebras by the power set-functor. See at FinSet – Opposite category for details and see at Stone duality for more.

Viewing as schemes

Every finite set can be viewed as an affine scheme. Indeed, since a finite coproduct of affine schemes SpecR iSpec R_i, i=1,,ni=1,\ldots,n, is again affine, Spec(R 1××R n)Spec (R_1 \times \cdots \times R_n), given a finite set XX, the coproduct of XX many copies of the terminal scheme, SpecSpec \mathbb{Z}, is the affine scheme Spec( X)Spec (\mathbb{Z}^X).

Equipping XX with a total order, we can view it (up to isomorphism, that is, bijection) as a set of integers {x 1,,x n}\left\{ x_1, \ldots, x_n \right\}. One can then view XX as the set of zeroes of the set of polynomials in one variable yy given by {yx 1,,yx n}\left\{ y - x_1, \ldots, y - x_n \right\}, or of the single polynomial given by the product of all these.

Thus, one can view XX as the affine scheme (over Spec()Spec(\mathbb{Z})) given as the commutative ring spectrum Spec([y]/I)Spec\left( \mathbb{Z}[y] / I \right), where II is the ideal generated by the afore-mentioned polynomial(s). Since [y]/I n\mathbb{Z}[y] / I \simeq \mathbb{Z}^n, this agrees with the above description, but additionally lets us see XX as a closed subscheme of the affine line Spec([y])Spec(\mathbb{Z}[y]).

One can view XX as a ‘constant scheme’ over any other base scheme YY by base change, that is, by means of the canonical projection morphism Y×XYY \times X \to Y.


For a treatment in homotopy type theory see

See also