nLab finite number

The cardinality of a finite set is a finite number.

Category of finite numbers

Let’s identify finite numbers with elements of \mathbb{N}.

\mathbb{N} can be made into a category FNumbFNumb with hom-sets FNumb[n,p]={}FNumb[n,p]=\{\bullet\} if npn \le p and FNumb[n,p]=FNumb[n,p]= \emptyset else.

Cardinality functor

Write MonoFSetMonoFSet for the wide subcategory of FSetFSet with objects finite sets and morphisms injections.

We then have the cardinality functor |.|:MonoFSetFNumb|.|: MonoFSet \rightarrow FNumb which associates its number of elements to every finite set.

This functor verifies the following properties:

  • |A×B|=|A|.|B||A \times B| = |A|.|B|
  • |f×g|=|f|.|g||f \times g| = |f|.|g|
  • |AB|=|A|+|B||A \sqcup B| = |A|+|B|
  • |fg|=|f|+|g||f \sqcup g| = |f|+|g|
  • ||=0|\emptyset| = 0

Last revised on July 30, 2022 at 15:33:12. See the history of this page for a list of all contributions to it.