FinSet.yaml

id: FinSet
name: category of finite sets
notation: $\FinSet$
objects: finite sets
morphisms: maps
description: null
nlab_link: https://ncatlab.org/nlab/show/FinSet

tags:
  - set theory

related:
  - FI
  - FS
  - Set
  - Set_c
  - Set_f

satisfied_properties:
  - property: locally small
    proof: There is a forgetful functor $\FinSet \to \Set$ and $\Set$ is locally small.

  - property: locally finite
    proof: This is trivial.

  - property: essentially countable
    proof: Every finite set is isomorphic to some $\{1,\dotsc,n\}$ for some $n \in \IN$.

  - property: generator
    proof: The one-point set is a generator since it represents the forgetful functor $\FinSet \to \Set$.

  - property: cogenerator
    proof: The two-element set is a cogenerator.

  - property: semi-strongly connected
    proof: Every non-empty finite set is weakly terminal (by using constant maps).

  - property: elementary topos
    proof: This follows easily from the fact that sets form an elementary topos.

  - property: ℵ₁-cofiltered limits
    proof: 'Let $D : \I \to \FinSet$ be a $\aleph_1$-cofiltered diagram. Let $(p_i : P \to D(i))_{i \in \I}$ be a limit cone of the corresponding diagram in $\Set$. We only need to show that $P$ is finite. If not, then it contains a sequence of pairwise distinct elements $x_1,x_2,\dotsc$. For all $n \neq m$ there is some $i_{n,m} \in I$ with $p_{i_{n,m}}(x_n) \neq p_{i_{n,m}}(x_m)$. Since $\I$ is $\aleph_1$-cofiltered, it contains a cone $(j \to i_{m,n})$. Then $p_j(x_n) \neq p_j(x_m)$ for all $n \neq m$. This is not possible since $D(j)$ is a finite set.'

unsatisfied_properties:
  - property: small
    proof: Even the collection of all singletons is not a set.

  - property: skeletal
    proof: This is trivial.

  - property: countable
    proof: This is trivial.

  - property: natural numbers object
    proof: >-
      If $(N,z,s)$ is a natural numbers object, then
      $$1 \xrightarrow{z} N \xleftarrow{s} N$$
      is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. But there is no finite set $N$ with $N \cong 1 + N$.

special_objects:
  initial object:
    description: empty set
  terminal object:
    description: singleton set
  coproducts:
    description: '[finite case] disjoint union'
  products:
    description: '[finite case] direct products'

special_morphisms:
  isomorphisms:
    description: bijective maps
    proof: This follows exactly as for sets.
  monomorphisms:
    description: injective maps
    proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms.
  epimorphisms:
    description: surjective maps
    proof: Use the same proof as for sets.
  regular monomorphisms:
    description: same as monomorphisms
    proof: This is because the category is mono-regular.
  regular epimorphisms:
    description: same as epimorphisms
    proof: This is because the category is epi-regular.