So okay, here's a thread on the category of finite sets and…

First let's give some terminology and definitions. I'm going to let Γ denote the category whose objects are finite sets and morphisms are functions of finite sets. There are a whole lot of finite sets so to simplify thinking about this category, I'll work with a "skeleton."

What that means is that I'll just work with isomorphism classes of objects of Γ, i.e. if there is a bijection between two finite sets A and B, I'll think of them as the same set (this can be made categorically precise).

What I end up with then is a category whose objects are countable, namely the set {∅, {1}, {1,2}, {1,2,3},...} and whose morphisms are just functions between these sets. This will be enough to get at some cool algebraic structure.

At some point I might start writing 1 for {1} and 2 for {1,2}, and n for {1,2,3,...,n} but I'll try to let you know that I'm doing it, and hopefully it won't be too confusing of a notational switch.

So back to Γ then, the category of (isomorphism classes of) finite sets. The first thing I want you to notice about Γ is that it contains a commutative monoid with respect to coproduct, namely the object {1}. How can we see this?

First let me just say what I mean by "commutative monoid with respect to coproduct." Well if you go here https://t.co/jS9n44TUGl you'll see that to define a "monoid object" in Γ we first need to define a tensor product in Γ.

So for us, inside of Γ, the "tensor product" of finite sets will be the coproduct, or disjoint union. And then we can ask that certain diagrams commute involving an object, it's "tensor powers" and various maps.

Now we want to see that, in particular, the object {1}∈Γ is a commutative monoid. How do we see this?

Well notice that there's exactly one function μ:{1,2}→{1}, it just takes both elements to 1, and that there's a bijection {1,2}≅{1}⊔{1} (and recall that we're identifying things which are isomorphic).

So we want to think of this function μ as a "multiplication map" {1}⊔{1}→{1}. It's clearly a binary operation on {1}, but we want to check that it's associative and commutative. We'll also want to determine a unit map. I won't do every detail but I'll give you the idea.

Let's start with associativity. This should mean, from the categorical POV of {1} being a "commutative monoid object," that the two maps {1}⊔{1}⊔{1}→{1}⊔{1}→{1}, coming from applying μ on different sides, are in agreement.

You can think a bit about this if you like, about the actual functions we're considering here (I'd recommend it!) but the quick and dirty way to check associativity is to notice that {1} is terminal in Γ. So there's really only one possible map {1}⊔{1}⊔{1}≅{1,2,3}→{1}.

So in other words, that diagram we drew up there is commutative, so μ defines an associative binary operation on {1}. Checking that μ is commutative is actually easier. Notice that there are exactly two functions {1,2}→{1,2}.

There's the identity and there's the "swap" map τ given by 1↦2 and 2↦1. So there are two possible maps {1,2}≅{1}⊔{1}→{1}. There's the map μ and there's μ(τ), the "multiplication" precomposed with the swap. These give a diagram like this:

But again since {1} is terminal, these have to be the same map! In other words, the identity a∗b=b∗a holds in {1} (although of course a=b=1). So {1} has an associative and commutative binary operation on it.

To see that {1} is a monoid you need to provide a unit map to it from the monoidal unit of the category Γ, in this case ∅, but there's only one such map, and I'll let you check that this behaves like a "unit."

Okay, so Γ is a symmetric monoidal category with respect to the coproduct, and therein, {1} is a commutative monoid. And what's more, we've seen really explicitly how {1} is a commutative monoid.

So let's ask what a symmetric monoidal functor from (Γ,⊔,∅) to another symmetric monoidal category (C,⊗,𝟙) should be.

Recall that being symmetric monoidal here means that our functor F:Γ→C needs to have the property that F(A⊔B)≅F(A)⊗F(B), i.e. "F preserves tensor product," and that F(∅)=𝟙, i.e. "F preserves the monoidal unit."

Since the object {1} isn't the coproduct of any other objects and isn't the monoidal unit, being symmetric monoidal doesn't put any restrictions on F(1), so it can be any object at all in C.

But once we've decided F(1)=X∈C, F(n) is decided for every n (and now I'm using a shorthand of n={1,2,...,n}). That's because n is the n-fold coproduct of 1 with itself, so F(n)≅X⊗X⊗...⊗X, with n copies on the right hand side.

But then the map 2={1,2}→{1}=1 that we had before becomes a map X⊗X≅F(2)→X, i.e. some kind of binary operation on X. And now you get a big boost from basic category theory, because F is a functor.

So if a diagram commuted inside of Γ, then F applied to that diagram is going to commute inside of C, which means all the diagrams making {1} into a commutative monoid also make X=F(1) into a commutative monoid.

In other words, if you provide me with the data of a symmetric monoidal functor F:Γ→C, you've simultaneously provided me with the data of a commutative monoid structure on F(1) with respect to ⊗.

What's even better is that a symmetric monoidal natural transformation F→G between two such functors is exactly the same as the data of a map of commutative monoids F(1)→G(1). So this "equivalence of data" lifts to the categorical level.

That is to say, there is an equivalence of categories between the functor category SMFun(Γ,C) with symmetric monoidal natural transformations as morphisms, and the category of commutative monoids in C with commuative monoid maps between them.

It turns out that there's a very general notion for "symmetric monoidal categories D such that symmetric monoidal functors D→C correspond to all objects in C with a prescribed algebraic structure." It's Boardman and Vogt called a PROP.

The term PROP is supposed to be sort of an acronym standing for "PROduct and Permutations." I'll say something about where the "permutations" are in just a second, but "product" corresponds to everything in sight having a tensor product.

In case you read that thread I posted about operads, you might see some similarities, and indeed, PROPs are closely related to operads, but are more general. There is however an adjunction between PROPs and symmetric operads which tells you a lot about their relationship.

Unlike operads however, a PROP is pretty easy to define. It's literally just a symmetric monoidal category whose objects are (isomorphic to) the natural numbers ℕ, and whose tensor product is given by addition of natural numbers.

So you can go back and check that Γ satisfies these conditions. Anyway, what "permutations" are doing here are essentially encoding that you've got a symmetric monoidal category.

If you think a bit about it, you can probably convince yourself that in any symmetric monoidal category, the n-fold tensor product of an object with itself has an action of the symmetric group on n letters by permuting the coordinates.

In fact, that's kind of the minimal data an object needs to be an element of a symmetric monoidal category. To make this precise we can talk about another PROP, which I'll denote by Σ. We know the objects of Σ have to be ℕ again.

We don't know is what the morphisms of Σ are, but they're pretty easy to define. We say the morphisms from k to j in Σ are either: (a) the empty set ∅ if j≠k, and the symmetric group on k elements, Σₖ, if k=j.

If you like this kind of language, you can say that Σ is the coproduct of the classifying spaces (or classifying groupoids I guess) of all the groups Σₖ for all k∈ℕ.

So here's an exercise: check that the category of symmetric monoidal functors from Σ to any other symmetric monoidal category C are equivalent to the category C itself.

I.e. if we know that C is symmetric monoidal then the data of "being an object of C" is exactly the same as the data of "having actions of the symmetric groups on all of your tensor powers," more or less.

Here's another thing you can play around with: try to see why the category of finite *pointed* sets, Γ₊, is the PROP of augmented commutative monoids. The relevant monoidal structure on Γ₊ is the wedge product of pointed sets.

And before I go, I'll just mention that there are also versions of PROPs for non-symmetric monoidal categories, i.e. plain monoidal categories and braided monoidal categories.

Sometimes these are called PROs and PROBs, respectively, where the former has no more permutations, and in the latter the permutations have been replaced by braids.

I sort of prefer the terminology monoidal theory, braided theory and symmetric theory, over PRO, PROB and PROP, and try to use that, but it might be hard to overcome the inertia of PROP.

I should also say that a PROP in which you've required the tensor product to be the cartesian product specifically is often called a Lawvere theory, and these pop up in lots of cool places too.

A few credits should be rolled here:

I used @kossnocorp's @chirrapp app to write this thread and I like it a lot! I used @varkora's @q_uiver_app to make the diagrams, and I also like that a lot! And I'm about to use @threadreaderapp to unroll this thread.

Also, if you are a person who's got extra money, and this was a helpful or interesting thread for you, feel free to buy me a coffee at: https://t.co/S78AAkpD5j