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: applied category theory

Topic: nashator & friends


view this post on Zulip Cole Comfort (Apr 20 2023 at 11:05):

Matteo Capucci (he/him) said:

Bruno Gavranović said:

John Baez said:

Then there's a great little theorem saying the right adjoint of a strong monoidal functor is lax monoidal!

Ah, this is the whole story of vertical (lax monoidal) and horizontal (oplax monoidal) morphisms in a double category, since here we've got a shadow of the adjunction in a double category, making our oplax monoidal additionally strong (since it needs to be at least lax).

(Notice though that lax+oplax \neq strong, e.g. the Nashator is lax monoidal structure on a functor which is also oplax monoidal but the oplax structure is only left inverse to the lax one)

If you ever have an oplax and lax monoidal situation which is not strong, then a good millieu is a [[Frobenius monoidal functor]]. I think they are really underated, and separable when the oplaxator is let inverse to the laxator; this nice distributive law allows you to comppose them. Is the nashator such a situation?

view this post on Zulip Matteo Capucci (he/him) (Apr 20 2023 at 11:06):

Ah good point, I didn't check!

view this post on Zulip Notification Bot (Apr 20 2023 at 11:09):

2 messages were moved here from #learning: questions > Is this well defined? by Matteo Capucci (he/him).

view this post on Zulip Matteo Capucci (he/him) (Apr 20 2023 at 11:09):

On my two feet the Frobenius law doesn't seem to hold

view this post on Zulip Matteo Capucci (he/him) (Apr 20 2023 at 11:10):

To clarify: the functor I'm talking about goes ():Lens(Set)Lens(Set)(-)^* : \bf Lens(Set) \to Lens(Set) and is defined as (X,S)(X,SX)(X, S) \mapsto (X, S^X).

view this post on Zulip Matteo Capucci (he/him) (Apr 20 2023 at 11:16):

Here's the lax monoidal structure:
image.png

view this post on Zulip Matteo Capucci (he/him) (Apr 20 2023 at 11:17):

the oplax monoidal structure is given similarly but the backward map now goes ×:SX×RY(S×R)X×Y\times : S^X \times R^Y \to (S \times R)^{X \times Y} and it given by just putting the maps next to each other

view this post on Zulip Tobias Fritz (Apr 20 2023 at 15:47):

I don't know about this particular situation, but whenever there's a lax and an oplax structure around, they will typically either form a Frobenius monoidal functor or form a bilax monoidal structure, which in particular requires this diagram to commute:
image.png

So you may want to check whether this holds instead of the Frobenius law. This diagram is from Section 3.1.1 of Monoidal functors, species and Hopf algebras, where the full definition is given. When the domain category is trivial, this reproduces the notion of bimonoid, where the multiplication and comultiplication are homomorphisms with respect to each other.

view this post on Zulip Tobias Fritz (Apr 20 2023 at 15:47):

Bilax monoidal structures also occur in probability, and generally on any commutative monad on a cartesian monoidal category.

view this post on Zulip Matteo Capucci (he/him) (Apr 22 2023 at 14:52):

Interesting,I'll check!

view this post on Zulip John Baez (Apr 29 2023 at 19:54):

My first encounter with bilax monoidal functors was the "normalized chain complex" functor from simplicial abelian groups to chain complexes of abelian groups. This functor lies at the heart of homology and cohomology. Both these categories have famous monoidal structures, and this functor is bilax but not strong! The laxator is called the Eilenberg-Zilber map and the oplaxator is called the Alexander-Whitney map. Composing these in the right order we get a retraction!

view this post on Zulip Jules Hedges (Apr 30 2023 at 12:26):

Matteo Capucci (he/him) said:

To clarify: the functor I'm talking about goes ():Lens(Set)Lens(Set)(-)^* : \bf Lens(Set) \to Lens(Set) and is defined as (X,S)(X,SX)(X, S) \mapsto (X, S^X).

I'll record here something that's already joined the heap of Glaswegian folklore: Matteo's functor is a monad that's dual to the "linear exponential comonad" that interprets the ! of linear logic in a dialectica category, explored in lots of detail in Valeria de Paiva's thesis. One of the relevant keywords for this is "Seely category"

view this post on Zulip Jules Hedges (Apr 30 2023 at 12:27):

(I'm in the process of writing an entire codebase structured around this fact)

view this post on Zulip Bruno Gavranović (May 01 2023 at 08:27):

Matteo Capucci (he/him) said:

To clarify: the functor I'm talking about goes ():Lens(Set)Lens(Set)(-)^* : \bf Lens(Set) \to Lens(Set) and is defined as (X,S)(X,SX)(X, S) \mapsto (X, S^X).

Am I understanding it correctly that this is of a different type than the one in the actual paper? Or is it merely that the one from the paper is factored through this

view this post on Zulip Matteo Capucci (he/him) (May 04 2023 at 18:53):

Bruno Gavranović said:

Matteo Capucci (he/him) said:

To clarify: the functor I'm talking about goes ():Lens(Set)Lens(Set)(-)^* : \bf Lens(Set) \to Lens(Set) and is defined as (X,S)(X,SX)(X, S) \mapsto (X, S^X).

Am I understanding it correctly that this is of a different type than the one in the actual paper? Or is it merely that the one from the paper is factored through this

Yes, the one in the paper fails to be oplax monoidal

view this post on Zulip Matteo Capucci (he/him) (May 04 2023 at 18:54):

(unless PP is a monoid)