You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jacques Carette (Oct 22 2020 at 14:48):I'm trying to unpack the meaning of this, and I want to double-check my understanding. So "free" means that there's some Functor F that is left adjoint to some kind of forgetful functor. "Free X" usually refers to an object of the category of Xs. So to unpack the above, we need to find 2 categories and a forgetful functor between them.
The obvious category for X is then (Cartesian monoidal Categories, Homomorphisms), i.e. functors that respect the structure. In first order settings, the target category is usually Set, but here, that seems wrong, it seems we're implicitly targetting the category of categories instead. The "free" here is not about categorical structure, but rather cartesian monoidal structure.
One is often then interested in specializing the construction given by this left adjoint, i.e. applying the functor in a special case. A recent thread mentions "on 1 object". So there are infinitely many categories with 1 object... but let's assume this sloppiness means "the unit category", i.e. an inhabited contractible category, i.e. a -2-category. Right?
[I should also unpack "free symmetric monoidal category on a commutative monoid object"; assuming the unpacking above is correct, it's the "on a commutative monoid object" part that I'm fuzzy on. If the target is the category of categories, why does the left adjoint care that we apply it to a commutative monoid object? Basically: the sentence doesn't quite typecheck for me.]
Nathanael Arkor (Oct 22 2020 at 14:53):There is a choice for what to be be free on (e.g. sets, categories, etc.). I think the clearest way to state the property (i.e. free cartesian category on a category) is that, for any category C and cartesian category D, with a functor F : C → D, there exists a category Cart(C) and a cartesian functor F' : Cart(C) → D, making the triangle commute up to a unique natural isomorphism.
Nathanael Arkor (Oct 22 2020 at 14:54):The free cartesian category on a single object then takes C = 1, the terminal category.
Nathanael Arkor (Oct 22 2020 at 14:55):(See the nLab page on free objects, for instance.)
Nathanael Arkor (Oct 22 2020 at 15:01):The free symmetric monoidal category on a commutative monoid is analogous, and I think it's actually described by Tom Leinster in this blog post (or a similar construction, anyway).
John Baez (Oct 22 2020 at 16:34):Nathanael Arkor said:
There is a choice for what to be be free on (e.g. sets, categories, etc.). I think the clearest way to state the property (i.e. free cartesian category on a category) is that, for any category C and cartesian category D, with a functor F : C → D, there exists a category Cart(C) and a cartesian functor F' : Cart(C) → D, making the triangle commute up to a unique natural isomorphism.
Yes, that's nice. We can further package this by saying there's a pseudoadjunction between the 2-category Cat and the 2-category
CartCat = [cartesian categories, cartesian functors, natural transformations]
where the right adjoint
U: CartCat → Cat
sends every cartesian category to its underlying category, and the thing you're calling Cart is the left adjoint
Cart: Cat → CartCat
applied to objects.
(A "pseudoadjunction" is the most commonly useful 2-categorical generalization of adjunction.)
Dan Doel (Oct 22 2020 at 16:51):How do you arrange for stuff like 'free symmetric monoidal category with a commutative monoid object', since the stuff in the Cat part lacks the structure to talk about the object?
Jules Hedges (Oct 22 2020 at 17:07):So there's probably several different presentations of the free cartesian monoidal category on a set or a category, but there's one by Lambek that I like that goes via proof theory: it's equivalent to a category whose morphisms are certain equivalence classes of proofs in a certain proof calculus. (In this case, it will be a proof calculus for the pure logic of "and")
Nathanael Arkor (Oct 22 2020 at 17:31):Dan Doel said:
How do you arrange for stuff like 'free symmetric monoidal category with a commutative monoid object', since the stuff in the Cat part lacks the structure to talk about the object?
SMCs with commutative monoids should be given by models for the PROP of commutative monoids, for which you can talk about free models, so I imagine you can do it in two steps, by composing pseudoadjunctions Cat → SMC → SMC+CM.
Dan Doel (Oct 22 2020 at 17:32):Oh, so you don't do "free SMC" on something, you do "free (SMC with ...)" on something?
Nathanael Arkor (Oct 22 2020 at 17:37):That would be my guess, because you're really talking about commutative monoid objects, so you need a SMC to describe them in the first place.
John Baez (Oct 22 2020 at 17:43):Jules Hedges said:
So there's probably several different presentations of the free cartesian monoidal category on a set or a category, but there's one by Lambek that I like that goes via proof theory: it's equivalent to a category whose morphisms are certain equivalence classes of proofs in a certain proof calculus. (In this case, it will be a proof calculus for the pure logic of "and")
That's nice. Another thing is this: to get the free category with finite coproducts on C, form the category of presheaves on C and take the full subcategory where the objects are finite coproducts of representables.
To get the free category with finite products on C, just dualize this.
What's nice is that there are so many ways to think about this stuff: they shed different light on what's going on.
John Baez (Oct 22 2020 at 17:45):Dan Doel said:
How do you arrange for stuff like 'free symmetric monoidal category with a commutative monoid object', since the stuff in the Cat part lacks the structure to talk about the object?
I've never thought about the "free symmetric monoidal category with a commutative monoid object on a category C", though one could.
I mainly think about ""free symmetric monoidal category with a commutative monoid object". This is the case where C is empty.
John Baez (Oct 22 2020 at 17:48):For me, the "free symmetric monoidal category with a commutative monoid object" is:
such that
and
John Baez (Oct 22 2020 at 17:48):This is just like how ordinary mathematicians think about "the free group on one generator".
Reid Barton (Oct 22 2020 at 17:49):And not just the free group on one generator, but also things like "the free group on one generator such that ".
John Baez (Oct 22 2020 at 17:49):Right: there we are giving the generator extra properties.
John Baez (Oct 22 2020 at 17:50):In the categorified situation we can get a bit fancier and give the generator extra structure, like being a commutative monoid object.
John Baez (Oct 22 2020 at 17:50):But Dan is right that this idea can - and perhaps should? - be packaged into an adjunction.
John Baez (Oct 22 2020 at 17:51):Nathaniel sketched how that goes, in this case.
Dan Doel (Oct 22 2020 at 17:55):Well, for instance, it seems clear how 'free cartesian monoidal category with an object' works as an adjunction, and the phrasing is pretty much the same. I just realized I couldn't make sense of one of the examples. :)
Dan Doel (Oct 22 2020 at 17:56):I mean, it's clear to me what the thing was supposed to be. But not how to fit it in the particular free/forgetful framework.
John Baez (Oct 22 2020 at 17:58):Yes. A commutative monoid only knows how to survive in a symmetric monoidal category, so you have to freely provide its environment before you can freely provide the commutative monoid. This is an example of the microcosm principle.
It's like: to buy a goldfish, you'd better buy a fish tank first.