nLab finite set

Introduction

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.

Definitions

Standard definition

We can for example make the following definition.

Definition

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

Finiteness constructively and internally

Variations

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

• A set is finite (for emphasis Bishop-finite or $B$-finite) if (as above) it admits a bijection with $[n]$ for some natural number $n$.

• A set is subfinite (or $\tilde{B}$-finite) if it admits an injection into some finite set $[n]$; that is, it is a subset of a finite set.

• A set is finitely indexed (or Kuratowski-finite, $K$-finite, or even sometimes, confusingly, subfinite) if it admits a surjection from some finite set $[n]$; that is, it is a quotient set of a finite set.

• A set is subfinitely indexed (or Kuratowski-subfinite or $\tilde{K}$-finite) if it admits a surjection from a subfinite set, or equivalently admits an injection to a finitely indexed set; that is, it is a subquotient set of a finite set.

• A set $X$ is Dedekind-finite if it satisfies one of the following:

  • any injection $X\hookrightarrow X$ must be a bijection.
  • for any function $f\colon \mathbb{N} \to X$ from the natural numbers, there exist $n,m$ with $n \ne m$ such that $f(n) = f(m)$.

  In contrast to the previous three notions, Dedekind-finite infinite sets can coexist with excluded middle, although countable choice suffices to banish them. The above two versions of Dedekind-finiteness are equivalent with excluded middle, but constructively they may differ. In addition, there are other forms of Dedekind-finiteness that are strictly stronger even with excluded middle; see this MO question for instance.

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

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

Moreover:

• Finite and subfinite sets have decidable equality. Conversely, any complemented subset of a finite set is finite.

• Finite sets are closed under finite limits and colimits.

• A finitely indexed set with decidable equality must actually be finite. For it is then the quotient of a decidable equivalence relation, hence a coequalizer of finite sets. In particular, a set which is both finitely indexed and subfinite must be finite, i.e. the above “commutative square” of implications is also a “pullback”.

• In particular, a set with a split surjection from $[n]$ is finite, since it has both a surjection from and an injection into $[n]$.

• Finite sets are always projective; that is, the “finite axiom of choice” always holds.

• However, if a finite set with $2$ elements (or any set, finite or not, with at least $2$ distinct elements) is choice, or if every finitely-indexed set (or even any $2$-indexed set) is projective, then the logic must be classical (see excluded middle for a proof).

• Finite sets are also Dedekind-finite (in either sense).

• If filtered category means admitting cocones of every Bishop-finite diagram, then a set is Bishop-finite iff it is a finitely presented object in Set and it is Kuratowski-finite iff it is a finitely generated object in Set.

Finiteness without infinity

All of the above definitions except for Dedekind-finiteness only make sense given the set of natural numbers. However, they can all be rephrased to make sense even without the axiom of infinity in set theory, and thus in a topos without a natural numbers object. Basically, you define (for a given set $S$) the concept of ‘collection of subsets of $S$ 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 $S$ is finite if and only if it is an element of all such collections. Namely, for any set $S$ we define the following subsets of the power set $P(S)$.

• $K(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a singleton in $S$. Then $S$ is finitely-indexed iff $S \in K(S)$. Note that $K(S)$ is also the free semilattice generated by $S$.
• $\tilde{K}(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a subsingleton in $S$. Then $S$ is subfinitely-indexed iff $S \in \tilde{K}(S)$.
• $B(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a singleton in $S$ disjoint from $A$. Then $S$ is finite iff $S \in B(S)$.
• $\tilde{B}(S)$ is the smallest subset of $P(S)$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a subset of $S$ and $B$ a subsingleton in $S$ disjoint from $A$. Then $S$ is subfinite iff $S \in \tilde{B}(S)$.

In addition, finite sets are decidable subsets of themselves, so one could use the set of decidable subsets $2^S$ in the definition of finite set instead of power sets:

• Let $B(S)$ denote the smallest subset of $2^S$ containing the empty set and closed under the operation $A \mapsto A \cup B$ for $A$ a decidable subset of $S$ and $B$ a singleton in $S$ disjoint from $A$. Then a set $S$ is finite iff $S \in B(S)$.

The definitions of subfinite, finitely indexed, and subfinitely indexed follow from above:

• A set is subfinite if it admits an injection into some finite set.

• A set is finitely indexed if it admits a surjection from some finite set.

• A set is subfinitely indexed if it admits a surjection from a subfinite set, or equivalently admits an injection to a finitely indexed set.

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 $Spec R_i$, $i=1,\ldots,n$, is again affine, $Spec (R_1 \times \cdots \times R_n)$, given a finite set $X$, the coproduct of $X$ many copies of the terminal scheme, $Spec \mathbb{Z}$, is the affine scheme $Spec (\mathbb{Z}^X)$.

Equipping $X$ with a total order, we can view it (up to isomorphism, that is, bijection) as a set of integers $\left\{ x_1, \ldots, x_n \right\}$. One can then view $X$ as the set of zeroes of the set of polynomials in one variable $y$ given by $\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 $X$ as the affine scheme (over $Spec(\mathbb{Z})$) given as the commutative ring spectrum $Spec\left( \mathbb{Z}[y] / I \right)$, where $I$ is the ideal generated by the afore-mentioned polynomial(s). Since $\mathbb{Z}[y] / I \simeq \mathbb{Z}^n$, this agrees with the above description, but additionally lets us see $X$ as a closed subscheme of the affine line $Spec(\mathbb{Z}[y])$.

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

Related concepts

• infinite set

• hereditarily finite set

• FinSet

• space of finite subsets

• finite object, finite type

• the cardinality of a finite set is a finite number

• cofinite subset

• countable ordinal

• finite-dimensional vector space

• finite homotopy type,

  • finite CW-complex, finite spectrum

• profinite set

• finite cover

• finite graph

• finite category

• finite limit, L-finite limit

• finite homotopy type, π-finite homotopy type

• locally finite type

References

Original articles:

• C. Kuratowski, Sur la notion d’ensemble fini , Fund. Math. I (1920) pp.130-131. (pdf)

See also:

• Wikipedia, Finite set

Discussion of notions of finite sets in constructive mathematics:

• Arnaud Spiwack, Thierry Coquand, Constructively Finite?, in: Contribuciones cientifícas en honor de Mirian Andrés Gómez, Universidad de La Rioja (2010) 217-230 [ISBN:978-84-96487-50-5, inria-00503917]

Formalization in homotopy type theory/univalent foundations of mathematics:

• Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide, Finite Sets in Homotopy Type Theory, in CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (2018) 201–214 [doi:10.1145/3167085, pdf]