Is FinSet the homotopy category of a computationally-nice preorder?

General
1

One of Lawvere’s great insights was that it’s much easier to work with properties than it is to work with structure. Preorders are the type of category where morphisms are properties rather than structure, and so if it is possible to get away with a preorder instead of a category, there are some benefits.

Additionally, in a preorder the “product” (or “meet”) of two objects is the natural notion of “diff” between them. In a category, this is just the product, and hence not very interesting. But in a preorder this can tell you something about how the two objects are related.

The idea for this post happened through thinking about how to implement version control for finite sets, ala chit. In a traditional implementation of finite sets, a finite set is just a natural number. However, in chit a finite set is a finite subset A of the set of UUIDs (which we will identify with \mathbb{N}), along with an equivalence relation on A, which is represented by an idempotent function u_A : A \to A (a \sim_A a' iff u_A(a) = u_A(a')) (this would be implemented as a union-find data structure).

There is a natural preorder structure we can put on the collection of such (A,u_A). Namely, (A, u_A) \leq (B, u_B) if A \subseteq B and the following commutes:

In other words, u_B = u_B \circ u_A. Thus, if a \sim_A a' then a \sim_B a'.

It appears that this condition is quite strict, but in fact it is equivalent to to the inclusion preserving the equivalence relation. To see why, consider (\{1,2\}, - \mapsto 1) and (\{1,2\}, - \mapsto 2). Although these choose different representatives for their equivalence classes, it is the case that (\{1,2\}, - \mapsto 1) \cong (\{1,2\}, - \mapsto 2). More generally, if the inclusion preserves the equivalence relation, then u_A will take an element a of A to something in the same equivalence class in B, so u_B(a) = u_B(u_A(a)) as required.

We call the preorder of such pairs \mathsf{FinRep}, as each pair represents a finite set.

Now, there is a functor from \mathsf{FinRep} to \mathsf{FinSet} which sends each pair (A, u_A) to the set \mathrm{im}(u_A) \cong A/\sim, and sends an inclusion (A, u_A) \leq (B, u_B) to u_B|_{\mathrm{im}(u_A)} \colon \mathrm{im}(u_A) \to \mathrm{im}(u_B). Then we put a weak equivalence structure on \mathsf{FinRep} such that (A, u_A) \leq (B, u_B) is a weak equivalence iff it is sent to an isomorphism in \mathsf{FinSet}. This satisfies 2-out-of-6 because the isomorphisms in \mathsf{FinSet} satisfy 2-out-of-6, so this makes \mathsf{FinRep} into a homotopical category.

Let us now investigate finite limits and colimits in \mathsf{FinRep}. It has an initial object, i.e. the empty set, but no terminal object because we only allow finite sets. We now investigate meets (i.e. products). The meet of (A, u_A) and (B, u_B) is A \cap B along with any choice of representatives for the equivalence relation of x \sim_{A \cap B} y iff x \sim_A y and x \sim_B y. Likewise, the join of (A, u_A) and (B, u_B) is A \cup B with the equivalence relation generated by \sim_A and \sim_B. Hopefully there is an efficient algorithm for computing both meets and joins.

Note that the functor \mathsf{FinRep} \to \mathsf{FinSet} is not continuous or cocontinuous. We can think of limits/colimits in \mathsf{FinSet} as being in “general position” somehow. I.e., in general A \cap B = \emptyset, and then A \sqcup B = A \cup B. The “general position” for product is taking the join of (A \times B, (a,b) \sim (a, b')), (A \times B, (a,b) \sim (a',b)), which is A \times B with the trivial equivalence relation.

We now investigate the homotopy category of \mathsf{FinRep}. Here I am on very weak ground because I don’t have a lot of experience with categorical homotopy theory, but I will attempt to sketch some ideas.

First of all, the functor \mathsf{FinRep} \to \mathsf{FinSet} is essentially surjective, faithful, and the only maps that get sent to isomorphisms are weak equivalences, by definition. I’m pretty sure this should imply that \mathsf{FinSet} is the homotopy category of \mathsf{FinRep}.

Another way of getting at this would be to consider the category of cospans in \mathsf{FinRep} whose right leg is a weak equivalence, composed by pushout (i.e. meet),

and quotiented by the equivalence relation generated by diagrams of the form

Note that the middle arrow must be a weak equivalence by 2-out-of-3. Call this category \mathrm{WCsp}(\mathsf{FinRep}).

I thought I could get an equivalence \mathsf{FinSet} \cong \mathrm{WCsp}(\mathsf{FinRep}), but something seems to go wrong. Here was my attempt: let’s see if anyone can fix it.

Let \mathbb{F} be a skeleton of \mathsf{FinSet}, whose objects are identified with \mathbb{N}. Then pick an injective function \langle -, -\rangle \colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}, and define a functor F \colon \mathbb{F} \to \mathrm{WCsp}(\mathsf{FinRep}) in the following way. Send n \in \mathbb{F} to F(n) = \{\langle n, 1 \rangle, \ldots, \langle n, n \rangle\}, and send f \colon n \to m to the cospan

This makes sense… except for the case n = m when the right injection fails to be a weak equivalence. In fact, there seem to be no non-identity endomorphisms in \mathrm{WCsp}(\mathsf{FinRep}), which makes it unlikely in my mind that \mathrm{WCsp}(\mathsf{FinRep}) would be the homotopy category of \mathsf{FinRep}.

So I’m not exactly sure where to go from here. I hope the basic idea is clear enough that someone who knows more homotopy theory could give me some guidance.

1 Like
2

Just a quick remark that being faithful, surjective, and inverting the right maps isn’t enough to get the desired homotopy category, since all these properties are preserved if you freely add more maps to the codomain. I’m not sure yet about anything else here.

3

Yeah that’s a good point! Somehow I feel like every morphism in FinSet is hit by something though.

1 Like
4

I love this post, it’s such a cool idea. I thiiink you’re right that FinSet is the homotopy category of FinRep, which is kind of a big deal! I know it won’t be in the finite case but I wonder if when you allow non-finite subsets of N (the naturals) you might get a model category structure on Rep… Anyway here’s why I think it’s true:

Basically I like your construction of morphisms as cospans, but I think you don’t want to use a skeleton of FinSet but rather the equivalent category with two isomorphic sets of each cardinality. Then a function X → Y for any X =/= Y looks like a cospan in FinRep with apex X + Y (using an analogous injective function 2N x N → N and the appropriate eq relation on X + Y) and the right injection is always a weak equivalence, which does not solve the case of X=X that you pointed out but does allow for all of the isomorphisms X_1 → X_2 between the two distinct sets of the same cardinality. With these isomorphisms now available we can observe that the desired automorphisms arise as composites of isomorphisms X_1 → X_2 → X_1, but these composites in WCsp(FinRep) will just be identities which makes WCsp(FinRep) not the localization, like you said.

However, this is enough to still prove that FinSet is the localization I think, by checking that the universal property holds: Any functor F : FinRep → C inverting weak equivalences factors through FinSet uniquely up to natural isomorphism. To do this treat WCsp(FinRep) not as a category (since the composition is wrong for maps X → Y → X) but as a graph, and observe that a functor FinRep → C inverting weak equivalences gives a graph homomorphism WCsp(FinRep) → C since the backward leg of each span has an inverse in C (it’s probably moreover some kind of functor of partial categories but I don’t know if we need that). Then since we have a graph homomorphism FinSet (with objects 2N) → WCsp(FinRep) (which is also some kind of partial functor) we get a graph homomorphism FinSet → A which should be functorial and factor F up to iso.

There’s certainly more details to check but I think something like this could work. And I’m very excited by the result if so; I’m not sure yet how I would use it but I know that I really really want to!

5

Also, this may be of interest (I haven’t gone through the cited paper to figure out if it agrees with this construction, but it seems to be saying that every category is a localization of some preorder.

ct.category theory - Is every category a localization of a poset? - MathOverflow).

6

That’s kind of beautiful; it means that categories are nothing more than preorders+groupoids. I feel like this is why in computer science you don’t see so many morphisms of finite sets, rather you just rely on the implicit morphism of names matching up; if you combine that with the ability to rename, that actually gives you all the morphisms you need.

2 Likes