Mention another universal property.

]]>A nicer version might look at how finite $T_1$ spaces correspond to the discrete preorders inside finite preorders, using the equivalence between finite preorders and finite Alexandroff spaces, and if one is especially motivated, how the $R_0$ and $T_0$ spaces sit between these.

]]>Re #10: this seems awfully elaborate. If you asked ordinary mathematicians how to prove it, they might say this: in a $T_1$-space, all points are closed; since finite unions of closed sets are closed, this implies that every subset of a finite $T_1$-space is closed, i.e., a finite $T_1$-space is discrete. But the category of finite discrete spaces is clearly equivalent to the category of finite sets.

Is there a reason for doing it in this much more complicated way?

]]>have hyperlinked more of the technical terms (eg. *Top*)

adding section about the equivalence between FinSet and the category of finite $T_1$-topological spaces

]]>Ah, ignore most of #7 then. I misread and thought you were referring to $FinSet_*$ rather than the category you were actually defining.

]]>@Hurkyl,

regarding non-empty: my mistake (but, constructively, it would even be inhabited sets). If you have a surjection at the level of objects, then you get a section of the functor (modulo the correction) that is an adjoint inverse, and in fact I think these are isomorphic (supposing we had chosen a small skeleton): the set of section of the surjection on objects, thought of as a discrete category, and the category of sections of the functor that are also adjoint inverses. This follows the construction in CWM of a unique adjoint inverse from a certain section at the object level.

]]>(Nitpick: the image of $FinSet_* \to FinSet$ only surjects onto the full subcategory of nonempty sets)

I don’t think we require functions between sets preserve the choices, do we? I.e. we’re not asking for $FinSet_* \to FinSet_{\ncong \varnothing}$ to have a section or even $Core(FinSet_*) \to Core(FinSet_{\ncong \varnothing})$, but instead it’s $Ob(FinSet_*) \to Ob(FinSet_{\ncong \varnothing})$ we want to have a section.

]]>@Madeleine,

I doubt it without some Choice, because surely that would imply that the ff, surjective-on-objects functor from the category of pointed finite sets and arbitrary functions to FinSet had a section. Even if one took a skeleton of FinSet and restricted to that, it would imply that the function $u\colon \mathcal{N}\to \mathbb{N}$ has a section, where $|u^{-1}(n)|= n$.

]]>Does FinSet have a global choice operator?

]]>Typo fix: $FinSet^op$ is freely generated by finite limits (not finite colimits).

]]>Added facts about the universal properties of FinSet and its opposite.

]]>Added to *FinSet* a remark on the opposite category $FinSet^{op}$ from a constructive perspective:

“In constructive mathematics, for any flavor of *finite*, $\mathcal{P}$ defines an equivalence of $FinSet$ with the opposite category of that of those complete atomic Heyting algebras whose set of atomic elements is finite (in the same sense as in the definition of $FinSet$).”

I don’t know whether for some values of *finite*, this characterization can be made more interesting, i.e. whether we can give a condition which does not explicitly mention the set of atomic elements.

I have briefly recorded the equivalence of FinSet${}^{op}$ with finite Booplean algebras at *FinSet – Properties – Opposite category*. Then I linked to this from various related entries, such as *finite set*, *power set*, *Stone duality*, *opposite category*.

(I thought we long had that information on the $n$Lab, but it seems we didn’t)

]]>