Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: Monoid-enriched Categories

Jacques Carette (Jul 03 2020 at 02:48):

Traditionally, when one speaks of enriched categories, it is over a monoidal category. But for differential categories, the "additive categories" there are commutative monoid enriched. As stated there, this means all Homs have the structure of a commutative monoid (and some interaction laws).

Question: is this in fact the same as enriching over the category of commutative monoids, with its product monoidal structure? It looks like it is, but I'm about to embark of formalizing all of this, so if I'm reading things incorrectly, I'd rather not find out the hard way! [I've read 6 or 7 papers on variations on differential categories, and all of them build the monoid-enrichment 'from scratch' without mentioning that classically enrichment goes through a monoidal category.]

Reid Barton (Jul 03 2020 at 02:54):

No, with the tensor product structure.

Reid Barton (Jul 03 2020 at 02:56):

Composition is bilinear, not linear in the pair.

Jacques Carette (Jul 03 2020 at 03:15):

Thanks, that helps. As does the implicit affirmation of the rest.

Ben MacAdam (Jul 03 2020 at 03:41):

There's a bit of an odd mismatch in differential categories where the symmetric monoidal structure is CMon-enriched, but the coalgebraic modality is not necessarily CMon-enriched.

Jacques Carette (Jul 03 2020 at 03:49):

Thanks for the warning. We'll see how that comes up in the formalization. Usually such 'odd mismatches' do manifest themselves.

John Baez (Jul 03 2020 at 05:25):

To answer one of your questions: when people say a category is "commutative monoid enriched", they're saying it's enriched over the monoidal category of commutative monoids.

(And you can replace "commutative monoid" by anything else here: "X-enriched" is short for "enriched over the monoidal category of X's".)

John Baez (Jul 03 2020 at 05:27):

But when people say "the" monoidal category of commutative monoids, they're expecting you to guess which way they're making commutative monoids into the objects of a monoidal category. There are two "obvious" ways, but the good way here uses the tensor product of commutative monoids, not the cartesian product.

Jacques Carette (Jul 03 2020 at 12:48):

Hmm, now I'm wondering about actually constructing that tensor product. Already formal linear combinations are a bit odd (but doable), but the quotient is really hard. Is there a normal form for the tensor product? Even if there is, I suspect that it will implicitly assume decidable equality.

vikraman (Jul 03 2020 at 13:26):

Do you construct CMon as the EM algebra of the free commutative monoid monad?

Jacques Carette (Jul 03 2020 at 13:30):

I was hoping for a more direct construction. But even then "free commutative monoid monad" is Bag, which is very difficult to deal with constructively. If you have decidable equality, then it's not too bad, but without, it is quite a lot of work.
[And you mean CMon as monoidal category, right? Because CMon as category is very straightforward].

vikraman (Jul 03 2020 at 13:35):

I was going to suggest that, since Bag is a commutative monad, you could get the symmetric monoidal closed structure of CMon abstractly (using a result like https://users-math.au.dk/~kock/CCGBCM.pdf), you'd just need coequalizers in Set/Type.

Jacques Carette (Jul 03 2020 at 13:41):

There's a hope I might be able to squeak through: I'm working in Setoid-enriched categories at the base, so I can indeed change the equivalence. (1,2)-categories might turn out to be "the right choice" once again. (And why do you say coequalizers? p.6 of the paper assumes equalizers).

vikraman (Jul 03 2020 at 13:49):

Here is the explicit description: https://ncatlab.org/nlab/show/tensor+product+of+algebras+over+a+commutative+monad

Reid Barton (Jul 03 2020 at 13:50):

The linked paper constructs the closed structure, not the monoidal structure.

Reid Barton (Jul 03 2020 at 13:50):

But the closed structure on CMon doesn't require anything fancy to construct.

Reid Barton (Jul 03 2020 at 13:51):

I think you can also talk about an additive category as a category "enriched in the closed category CMon" (in fact I think this might even predate the notion of a monoidal category).

Jacques Carette (Jul 03 2020 at 13:55):

@vikraman Thanks, that helps. Except for the underlying Bag angle.

@Reid Barton Indeed. I should have noticed earlier (about the paper). Re: additive category, that is an interesting remark. So it might be possible to enrich in something weaker? My original question was related to just this. Maybe what I need to do is to ignore the word 'enrich' (in its traditional meaning) and hand-code "additive category" as being CMon-valued. [And isn't additive category usually reserved for Ab-enriched?]

Reid Barton (Jul 03 2020 at 13:55):

Sure, maybe. I don't think the terminology is very consistent.

Reid Barton (Jul 03 2020 at 13:58):

If CMon is the only category you care about enriching in, it's a lot simpler to just describe what it means to be CMon-enriched directly (Hom sets have commutative monoid structures, and composition is bilinear)

Reid Barton (Jul 03 2020 at 13:58):

IMO, the most natural framework to describe this is enrichment in the multicategory CMon

Reid Barton (Jul 03 2020 at 13:59):

but that also seems to be substantially less convenient formally than it is in ordinary mathematics.

Reid Barton (Jul 03 2020 at 14:04):

I suppose it depends on what you are doing but most likely, even when dealing with a CMon-enriched category, you're still going to be composing pairs of morphisms $f \in \mathrm{Hom}(B, C)$, $g \in \mathrm{Hom}(A, B)$ to get $f \circ g$, and you want to use the laws stated in the form $f \circ (g_1 + g_2) = f \circ g_1 + f \circ g_2$.

Jacques Carette (Jul 03 2020 at 14:05):

Agda-categories already has all the infrastructure in place to enrich over monoidal categories. So it was tempting to re-use it. But that appears to be difficult constructively. And, right now, I am really interested in differential categories, so I don't want to take a long detour, if I can help it.

There is also a problem with multicategories: its formalism "bakes in" a lot of theorems about the natural numbers (and the type Fin) as strict equalities, when constructively they require more. They are all true (of coruse), but introduce a very significant amount of noise. Turns out that an 'indexed' version of multicategories, where finiteness is not assumed, is considerably easier to work with.

Reid Barton (Jul 03 2020 at 14:05):

You don't naturally come across elements in $\mathrm{Hom}(B, C) \otimes \mathrm{Hom}(A, B)$ to apply $\mu : \mathrm{Hom}(B, C) \otimes \mathrm{Hom}(A, B) \to \mathrm{Hom}(A, C)$ to.

Reid Barton (Jul 03 2020 at 14:06):

So, really the relevant way to think of composition is as a bilinear map and the fact that bilinear maps are represented by linear maps out of a "tensor product" is mostly irrelevant.

Jacques Carette (Jul 03 2020 at 14:08):

I agree that I need those laws, they are crucial. That 'irrelevance' might be rather important. It might indeed let me code things up directly. I'll try that next!

vikraman (Jul 03 2020 at 15:04):

@Jacques Carette I suggested Bag since it's a simple recursive HIT, and once you have its universal property, you can do a lot calculations using it (see here, here, here). These examples are all internally in HoTT, but in your work, you could probably axiomatise the universal property, but you'll also have to transport along the equivalences you get. So this would be one slick way to construct CMon and it's tensor product.

Jacques Carette (Jul 03 2020 at 15:17):

Amusingly, I just wrote to the authors (Carlos, Anders and Max) of the 2nd paper you link to, pointing out to them that their (mentioned but not highlighted) assumption on decidable equality of the underlying A is a huge assumption. The paper on ordinals is absolutely gorgeous. If you're a glutton for punishment, you can dig through the dumpster fire that is my Agda code at https://github.com/JacquesCarette/TheoriesAndDataStructures to see how I've implemented Bag (and proved the Adjoint property in full). Better is the set of slides https://alhassy.github.io/next-700-module-systems/papers/JC_Program_Generation_Talk_IFIP.pdf . Ignore all the .pdf from the first github repo, they are all 'wrong' (and were rightly never submitted anywhere). [Reading your slides now]

Jacques Carette (Jul 03 2020 at 15:21):

Very nice! I was wondering when permutations would creep in more explicitly. What your HIT is encoding is that the identity type of a multiset, represented as a list of members, is exactly the set of (finite) permutations. I'm kind of surprised you don't say that explicitly anywhere.

Jacques Carette (Jul 03 2020 at 15:23):

Question: why do you explicitly truncate? Either as level 1 or 2? What do you get out of doing that?

Jacques Carette (Jul 03 2020 at 15:24):

I am super interested in the differential structure, and in generalized species. I've been slowly adding features to agda-categories with that in mind. [That's probably not apparent to anyone but me, but we can talk on another forum if that interests you.]

Reid Barton (Jul 03 2020 at 15:45):

Presumably because a commutative monoid is supposed to be a set by definition, and you won't get a set unless you truncate

vikraman (Jul 03 2020 at 16:08):

With groupoids, if you want to construct the free symmetric monoidal groupoid, it gets stuck because once you add the coherences, you run into regularity issues with the target of the path constructors having hcomps.

Jacques Carette (Jul 03 2020 at 16:16):

"A monoid is supposed to be a set" is very 0-categorical thinking. I'm interested in asking "so what if we don't assume that, what changes?" The Agda standard library, which defines Monoid over Setoid, the answer is 'nothing much'. It's a tiny bit more tedious, but not remarkably so.

Jacques Carette (Jul 03 2020 at 16:17):

The response re: groupoids says that, there, indeed something does change, and truncation becomes a good option to deal with the resulting regularity problem.

Jacques Carette (Jul 03 2020 at 16:18):

Note that I'm not saying that Monoids shouldn't be sets. I'm saying that we shouldn't force them to be, until we've figured out that it's kind of necessary to do so.

Reid Barton (Jul 03 2020 at 16:51):

If they are not sets then they should have higher coherence data which we don't know how to write down in HoTT.

vikraman (Jul 03 2020 at 16:51):

A monoid object can be defined in any monoidal category, setoids, or ∞ Grpd, but it's not the same problem as defining the free monoid monad, or the free SMC 2-monad, which is supposed to be an endofunctor.