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: learning: questions

Topic: enriching double categories by double categories

Flavien Breuvart (Oct 27 2021 at 12:32):

Hi all,
Does any of you knows about the enrichment of a category over a double category, of a double category over category our (ultimately) of a double category over a double category ?
I have been investigated the idea since two weeks (using a specific example as intuition that we can also discuss in a second time), and I managed to find interesting behaviors. By the way, I am new to the theory of enriched categories, so I may have made an obvious mistake, do not hesitate to contradict me.

Enriching a category over a double category
Let $\mathbb D$ be a double category, with $\mathbb V$ the vertical category, $\mathbb A$ the arrow category and $\mathbb H$ the horizontal category.
One can consider, the usual notion $\mathbb V$-enriched categories and $\mathbb V$-enriched functors. Less usual, one can also consider $\mathbb H$-enriched lax-functors $F$ between $\mathbb V$-enriched categories where the "laxity" diagrams are the obvious 2-cells of $\mathbb D$:

$$\begin{CD} 1 @= 1 \\ @VIVV \alpha @VIVV \\ \mathbb B(X,X) @>F>> \mathbb C(X,X) \end{CD} \begin{CD} \mathbb B (X,Y)\otimes\mathbb B(Y,Z) @>F\otimes F>> \mathbb C (X,Y)\otimes\mathbb C(Y,Z) \\ @V\_;\_VV \beta @V\_;\_VV \\ \mathbb B(X,Z) @>F>> \mathbb C(X,Z) \end{CD}$$

Unfortunately, I could not find any interesting structures surrounding this construction. But this is not surprising as lax-functors, in the 1-categorical context, do dot behave so well, however they do behave well for 2-categories :

Lax double functors
In http://www.tac.mta.ca/tac/volumes/20/18/20-18abs.html , the authors describe a nice notion of lax double functor which is strict in the vertical category, strict in the arrow category, but lax in the horizontal category.
Those lax functors have a good notion of natural transformations making the whole thing a 3 category (that is what is claimed here : https://golem.ph.utexas.edu/category/2009/12/the_problem_with_lax_functors.html , if anyone know of a published proof I would be interested.
However, this structures is not even enriched, let alone enriched into a double category.

Double categories enriched over a category
Following the above intuition, we would like to enrich the horizontal category but not the vertical one. I was not able to find much literature and I had to build my own version (related to framed double categories) :
Let $\mathbb E$ be a monoidal 2-category onto which we want the enrichment.
An $\mathbb E$-enriched double category $\mathbb D$ is given by

• a vertical category $\mathbb W$
• an arrow functor $\mathbb D : \mathbb W\times\mathbb W \rightarrow \mathbb E$ (The arrow category is then then given by the Grothiendieck construction on $\mathbb D$$ with the Grothiendieck projection corresponding to the source and target functors.)
• an iddentity $I_X \in \mathbb E(1,\mathbb D(X,X))$ natural in $X$
• a composition $(\_;\_) \in \mathbb E(\mathbb D(X,Y)\otimes\mathbb D(Y,Z),\mathbb D(X,Z))$ natural in $X,Y,Z$
• two 2-cells

$$\begin{CD} 1 @= 1 \\ @VIVV \alpha @VIVV \\ \mathbb D(X,X) @>\mathbb D(f,f)>> \mathbb D(X',X') \end{CD} \begin{CD} \mathbb D (X,Y)\otimes\mathbb D(Y,Z) @>\mathbb D(f,g)\otimes \mathbb D(g,h)>> \mathbb D (X',Y')\otimes\mathbb C(Y',Z') \\ @V\_;\_VV \beta @V\_;\_VV \\ \mathbb D(X,Z) @>\mathbb D(f,h)>> \mathbb D(X',Z') \end{CD}$$

(those 2-cells are oriented in the 2-category $\mathbb E$ following the grothendieck construction but I do not know how to write 2-arrow in this library)

• plus equalities of two cells for the associativity and the unity.

Putting everything together
These 3 constructions seems to behave quite well together by using $\mathbb V$ and globular cells in place of $\mathbb E$ above and enriching the diagrams of lax double functors.
This way we should obtain notions of vertical and horizontal $\mathbb D$-enriched lax functors, and $\mathbb D$-enriched natural transformations between verticals and between horizontal. I haven't checked yet, but I expect to have a triple category.

Do you know of similar constructions ?

Nathanael Arkor (Oct 27 2021 at 12:35):

Don't have time to read in detail now, but just wanted to give a quick pointer to this nLab section on enrichment in a double category. You may also be interested in Leinster's Generalized enrichment of categories , which goes even more general than this.

Nathanael Arkor (Oct 27 2021 at 12:36):

(I don't think I've seen enrichment of double categories anywhere, though.)

Flavien Breuvart (Oct 27 2021 at 12:39):

That was fast ! I did not see this specific sub-section of the nlab, I will have a look on both links. Thanks !
Edit : I have already had a look at Leinster article. This is not exactly the same point of view : I do not enrich over object, but just over arrows (like in standard enriched categories). There may be a link but I was not able to express it.

Mike Shulman (Oct 27 2021 at 16:26):

I'd like to hear the example(s) you have in mind. There are all sorts of things one could write down, with lots of slight variations that may look different, but the point of any categorical structure is to capture examples.

Flavien Breuvart (Oct 28 2021 at 07:54):

I did not want to write too long a ticket, but if you insist I will gladly agree in giving details :p
My goal is the understanding indexed extensions of multiplicative exponential logics such as gadded exponentials or Bounded Linear Logic. We already have a semantics (mostly that of https://doi.org/10.1007/978-3-030-71995-1_12 with some obvious generalizations), but the result is just a bunch of axioms with no clear picture, arbitrary restrictions and without any notion of higher order isomorphism.
This semantics require :

• two categories of indexes $\mathbb I$, and $\mathbb J$ with the same object and $\mathbb I$ a sub category of $\mathbb J$,
• a $\mathtt{SymMonPoset_{strict}}$-enrichment on $\mathbb J$ we use additive notations as the 1-bject versions are ordered semirings.
• a functor $L :\mathbb I \rightarrow \mathtt{SMCC_{strict}}$ representing the "reindexings"
• an oplax functor $E : \mathbb J \rightarrow \mathtt{SMCC_{lax}}$ representing the exponentials (for those that know linear logic : the colaxness of the functor correspond to the comonoidal laws of the exponential and the laxness of the targeted functors correspond to the monoidality of the exponential)
• two additional transformations $w : E(0) \rightarrow 1$ and $c : E(f+g)\rightarrow E(f)\times E(g)$ called weakening and contraction,
• plus a buch of diagrams

A few remarks :

• $\mathbb I$ and $\mathbb J$ form a framed double category as well as $\mathtt{SMCC_{strict}}$ and $\mathtt{SMCC_{lax}}$, but I can't use it by lake of framework,
• the enrichment of $\mathbb J$ seems to be generalizable to $\mathtt{SymeticMonoidalPoset_{lax}}$ (or maybe a version where the right composition is lax but not the left...) but it complexity things, examples of usage are few and there is no understanding of this generalization
• the category $\mathtt{SMCC_{lax}}$ is $\mathtt{SMC_{lax}}$-enrished (once again, the left composition is strict, which puzzles me)
• the weakening and contractions seems originated from an $\mathtt{SMC}$ enrichement of the functor $E$, but they are oplax while the source and target of $E$ are lax...
• as shown in https://doi.org/10.1007/978-3-319-89366-2_6 , the diagrams relating all these are reminiscence of the double category structure formed by $\mathtt{SMC_{lax}}$ and $\mathtt{SMC_{oplax}}$

In the end, I would expect that there would be a way to wrap it as a kind of $(\mathtt{SMC_{lax}},\mathtt{SMC_{oplax}}$-enriched double oplax functor tageting $(\mathtt{SMCC_{strict}},\mathtt{SMCC_{lax}})$.

Mike Shulman (Oct 28 2021 at 20:14):

Some of your math is missing the ending double-dollar-sign.

Flavien Breuvart (Oct 28 2021 at 22:23):

Oups, thanks !

Tim Hosgood (Oct 28 2021 at 23:34):

I think you might find the #seminar: Topos Colloquium talk from today interesting/relevant!

Mike Shulman (Oct 29 2021 at 06:15):

How are $L$ and $E$ related? Since $\mathbb I \subseteq \mathbb J$, both $L$ and $E$ can be applied to any morphism of $\mathbb I$; are those images supposed to coincide? That seems a very important point when trying to combine the two categories into a double category of some sort.

Flavien Breuvart (Oct 29 2021 at 06:56):

@Tim Hosgood Indeed ! too bad I missed it, I will definitely have a look at the recording

Flavien Breuvart (Oct 29 2021 at 06:58):

@Mike Shulman Sorry I forgot to mention that L and E agree on objects (but not on morphisms), otherwise the double-categoric point of view would indeed make no sens. In addition, there is the equality :
$L(f);E(u);L(g) = E(f;u;g)$

Mike Shulman (Oct 29 2021 at 14:40):

So what are the squares in the double category, and what do they get sent to under your functor?

Mike Shulman (Oct 29 2021 at 14:41):

If the squares are commutative diagrams in $\mathbb J$, then a double functor out of it into most any double category I can think of would force $L$ and $E$ to agree on morphisms as well, at least up to isomorphism.

Flavien Breuvart (Oct 31 2021 at 15:30):

Hi Mike,
Sorry for the late answer. The morphisms neerly agree since $E(f)=L(f);E(id)=E(id)L(f)$ but they are not isomoph since $E$ si a colax functor (and thus $E(id)\neq id$).
For example, given a comonad $W$ on $\mathtt{SMCC}$, one can consider $\mathbb I = \mathtt{SMCC}$ and $\mathbb J=\mathtt{SMCC}_W$ the (co-)Kleisli category with $L= id$ and $E$ being the inclusion (not the right adjoin). Then despite having $-^\dagger : \mathbb I \hookrightarrow\mathbb J$, the only equality we have is $E(f^\dagger)= L(f);\epsilon$.

Mike Shulman (Nov 01 2021 at 16:53):

Ah right, of course, the functor is colax.

Mike Shulman (Nov 02 2021 at 17:02):

This is an intriguing structure, but I agree it's not obvious how to represent it double-categorically. I'll be interested to hear what you come up with though. (-: