FinSet

FinSet is the category whose objects are finite sets and whose morphisms are all functions between them. It is a full subcategory of Set, obtained by restricting objects to finite sets. In many treatments FinSet is taken as a skeleton of this subcategory, where each object is identified up to isomorphism with a standard n-element set, and Hom(m,n) is the set of all functions from an m-element set to an n-element set.

Objects and morphisms: A typical object is a finite set A with |A| = n, and a morphism f: A → B is a function between these sets. Up to isomorphism, objects are indexed by natural numbers n ≥ 0, and FinSet is equivalent to the category with objects [n] = {1,...,n} and Hom([m],[n]) ≅ n^m.

Limits, colimits, and structure: FinSet has all finite limits and colimits. The terminal object is a singleton, the initial object is the empty set, products are cartesian products, and coproducts are disjoint unions. Every finite set has a finite number of elements, so hom-sets are finite; in particular, |Hom(A,B)| = |B|^|A|.

Cartesian closed and topos: FinSet is cartesian closed; the exponential B^A consists of all functions from A to B and is finite when A and B are finite. It is also an elementary topos, equipped with a subobject classifier isomorphic to the two-element set {0,1}.

Applications: FinSet provides a canonical setting for reasoning about finite types in logic and computer science, and serves as a simple, well-behaved model for finite combinatorial structures.

Notes: As a full subcategory of Set, FinSet inherits many properties from Set while remaining closed under the finite constructions that finite sets require.