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: deprecated: thermodynamics

Topic: 2-operad algebras

Owen Lynch (Apr 21 2022 at 22:39):

I need a notion of operad algebra where the collection of things corresponding to a type in the operad is in fact a category. Equivalently, instead of a lax symmetric monoidal functor from a symmetric monoidal category to $\mathsf{Set}$, I want a lax symmetric monoidal functor to $\mathsf{Cat}$. I guess you might call this a "categorification" of operad-algebras. Does anyone have a good reference for this? The theory is pretty obvious, so I can just derive it myself, but I should cite somebody who invented it before.

John Baez (Apr 22 2022 at 00:15):

Are you going to use a symmetric lax monoidal functor to the mere category $\mathsf{Cat}$, or are you going to take advantage of the fact that $\mathsf{Cat}$ is a 2-category to consider a symmetric lax monoidal pseudofunctor to $\mathsf{Cat}$?

John Baez (Apr 22 2022 at 00:16):

In simpler terms: are you planning to "weaken" the concept of operad algebra, making some laws hold only up to isomorphism?

Owen Lynch (Apr 22 2022 at 00:17):

Yes

Owen Lynch (Apr 22 2022 at 00:17):

Because the laxator is not strict

John Baez (Apr 22 2022 at 00:17):

Not strict in what sense?

Owen Lynch (Apr 22 2022 at 00:17):

I.e., the laxator takes manifolds $M$ and $N$ and produces their product $M \times N$

Owen Lynch (Apr 22 2022 at 00:18):

So the laxator is only associative up to isomorphism

John Baez (Apr 22 2022 at 00:18):

Okay...

John Baez (Apr 22 2022 at 00:18):

Too bad. If you weren't weakening, you could use the well-known existing concept of "algebra of an operad in an arbitrary symmetric monoidal category", taking that category to be $\mathsf{Cat}$.

John Baez (Apr 22 2022 at 00:19):

I'm a bit confused - there's a lot of room for level slips here - but anyway: you may be able to weasel out of these issues by judicious application of Mac Lane's strictification theorem.

Owen Lynch (Apr 22 2022 at 00:20):

Uh oh.

Owen Lynch (Apr 22 2022 at 00:20):

That sounds slightly evil

John Baez (Apr 22 2022 at 00:20):

As Google's new motto says, "Sometimes it pays to be evil".

Owen Lynch (Apr 22 2022 at 00:20):

Hahaha

John Baez (Apr 22 2022 at 00:21):

There is work on "weak" algebras of operads, but when I last checked it was very thin on the ground, and I have a hunch this is a case where a bit of judicious strictification would save you tons of trouble.

Owen Lynch (Apr 22 2022 at 00:22):

I'll look into it

Owen Lynch (Apr 22 2022 at 00:23):

The thing is, strictifying the cartesian product of manifolds seems very dodgy

John Baez (Apr 22 2022 at 00:26):

There's an old n-Cafe post where I ask about "weak algebras" of operads, or maybe "weak operads".... it's been so long I barely remember. But Julie Bergner and others wrote about "homotopy algebras" of Lawvere theories, which are similar but even weaker.

John Baez (Apr 22 2022 at 00:28):

Here's a reference to that sort of thing: [[homotopy T-algebra]].

John Baez (Apr 22 2022 at 00:28):

The main punchline is that such algebras can always be strictified, so that all the laws hold on the nose.

John Baez (Apr 22 2022 at 00:29):

An operad can be seen as a special sort of multisorted Lawvere theory, so those results do apply here... though there may be some finagling required to get them to apply to algebras in Cat rather than algebras in the category of simplicial sets.

John Baez (Apr 22 2022 at 00:30):

(Categories can be seen as specially nice simplicial sets.)

John Baez (Apr 22 2022 at 00:30):

So you see, working with "weak" things tends to push you into learning some homotopy theory.

Owen Lynch (Apr 22 2022 at 00:32):

I feel like homotopy theorists are to category theorists as category theorist are to regular mathematicians: waiting in the wings ready to swoop down and say "HA! I told you so! You DID need me!"

John Baez (Apr 22 2022 at 00:33):

Oh, very much so. And there are a bunch of them reading this thread, like vultures sitting in the tree-tops looking down at us.

Owen Lynch (Apr 22 2022 at 00:34):

In this case, however, I think I'm going to be stubborn and just plow ahead with what I know the definition must be, and then look back and see if it matches up with other stuff, now that I've ticked the box of "see if there's something obvious I'm missing."

Owen Lynch (Apr 22 2022 at 00:35):

Because there's a reason we use regular monoidal categories and not only strict monoidal categories, and so I think that having these weaker operad algebras is very similar in my mind.

Owen Lynch (Apr 22 2022 at 00:36):

I.e., associativity of products forces you to consider weakness, but only up to the pentagon identity.

John Baez (Apr 22 2022 at 00:36):

Btw, what are you hoping to use these for? You're writing a thesis on physics... I hope you don't get sucked too deep into higher-categorical issues.

Owen Lynch (Apr 22 2022 at 00:36):

It's very simple.

Owen Lynch (Apr 22 2022 at 00:36):

I want to compose port-Hamiltonian systems with an operad

Owen Lynch (Apr 22 2022 at 00:37):

It's the operad that comes out of the symmetric monoidal category of dirac relations

Owen Lynch (Apr 22 2022 at 00:37):

The set of port-Hamiltonian systems on an interface has a natural category structure

Owen Lynch (Apr 22 2022 at 00:37):

And composition is cartesian product + some other stuff

Owen Lynch (Apr 22 2022 at 00:38):

So I need a slightly weaker form of operad algebra in order to model this

Owen Lynch (Apr 22 2022 at 00:38):

But just slightly weaker!

Owen Lynch (Apr 22 2022 at 00:38):

Everything is pretty well-behaved

Owen Lynch (Apr 22 2022 at 00:39):

Anyways, I have to go now so I can't discuss this more now, but I will respond to anything you post later

John Baez (Apr 22 2022 at 00:39):

Okay. For anyone else reading this, I should add that the only reason I'd like to avoid "weak operads" is that your thesis is due this June! So there's not really a lot of time to write it.

John Baez (Apr 22 2022 at 00:40):

Ciao.

Owen Lynch (Apr 22 2022 at 03:08):

So the good news is that the functor to $\mathsf{Cat}$ is a strict functor

Owen Lynch (Apr 22 2022 at 03:08):

It's just the identities for the laxator that only hold up to natural isomorphism

Owen Lynch (Apr 22 2022 at 03:09):

I.e., these diagrams:
image.png

Owen Lynch (Apr 22 2022 at 03:09):

So it's just a tiny bit weaker than a typical operad algebra

Owen Lynch (Apr 22 2022 at 03:11):

So all I need to do is to come up with some higher identity analogous to pentagon and triangle identities that will hold in this case

Owen Lynch (Apr 22 2022 at 03:13):

Oh boy

Owen Lynch (Apr 22 2022 at 03:13):

That is not so simple

Owen Lynch (Apr 22 2022 at 03:14):

Well, I don't actually need higher coherence for anything (I don't think), because I don't really have any theorems that I'm looking to prove

Owen Lynch (Apr 22 2022 at 03:15):

So, worst comes to worst, I have a definition that works but is perhaps not as complete as I would like

Owen Lynch (Apr 22 2022 at 03:15):

But let me think if I can get something analogous to the pentagon/triangle identities

Owen Lynch (Apr 22 2022 at 03:18):

Also, wait, I know exactly what the condition is

Owen Lynch (Apr 22 2022 at 03:20):

The condition is that for any $X_1,\ldots,X_n$, the subcategory of the functor category $F(X_1) \otimes \cdots \otimes F(X_n) \to F(X_1 \otimes \cdots \otimes X_n)$ (with arbitrary chosen parenthesizations) that is generated by all functors composed of the laxator and the associator, and all natural isomorphisms generated by the natural isomorphisms making the above squares commute, is contractible

Owen Lynch (Apr 22 2022 at 03:22):

This is basically saying "we don't know what the coherence laws are, but just find some that are sufficient to prove this coherence theorem"

Owen Lynch (Apr 22 2022 at 03:23):

In a standard operad algebra, we would have that however you make the morphism $F(X_1) \otimes \cdots \otimes F(X_n) \to F(X_1 \otimes \cdots \otimes X_n)$, you get the same morphism. The natural generalization is that there is a canonical isomorphism between any two ways of making that morphism.

Owen Lynch (Apr 22 2022 at 03:25):

I could either prove this by finding some sufficient condition that just involved $X_1,X_2,X_3,X_4$, or I could try and prove this directly.

Owen Lynch (Apr 22 2022 at 03:29):

So, I guess if we take this to the operad level, we are saying that a "weak" operad algebra assigns a category $F(X)$ to each type $X$, and a contractible subcategory of the functor category $\mathrm{Hom}_{\mathsf{Cat}}(F(X_1) \times \cdots \times F(X_n),F(Y))$ to every operation $f$.

Owen Lynch (Apr 22 2022 at 03:33):

You may be right @John Baez that to actually write out everything for this may be a task beyond me in the time I have. But it is at least completely clear what this should be.

Owen Lynch (Apr 22 2022 at 03:35):

What I'm going to do for now is state the coherence principle for the "weak laxator", and then return to this later if I have time.

Owen Lynch (Apr 22 2022 at 03:37):

And I really would be surprised if nobody has looked at this before...