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: Monads and double categories

David Corfield (Oct 23 2024 at 08:44):

Say, I'm convinced of the importance of double categories for categorified logic from reading Lambert and Patterson's Cartesian double theories: A double-categorical framework for categorical doctrines. I note that $\mathbf{Lax}(\mathbb{1}, \mathbb{S}pan)$ is equivalent to $\mathbf{Cat}$. Then recalling that a monad is a lax 2-functor from the terminal 2-category $1$ to $\mathbf{Cat}$, I wonder how to represent the double-categorical theory of monads, $\mathbb{T}$, such that $\mathbf{Lax}(\mathbb{T}, \mathbb{S}pan)$ is equivalent to the 2-category of monads, monad functors, and monad functor transformations

Is there any way from these facts to see how to arrive at the theory of monads they have as Theory 3.8 (p. 21), as though this $\mathbb{T}$ is representing some form of $Lax(1, Lax(1, -))$ after everything's been promoted to some kind of double category?

Matteo Capucci (he/him) (Oct 23 2024 at 09:32):

I asked the same question to Evan once. This should be some kind of Gray tensor of theories, a closed monoidal structure on lax double functors. There is such a tensor for 2-categories and lax functors and for double categories and strict functors, but I'm not aware of something like what we want.

Nathanael Arkor (Oct 23 2024 at 09:41):

There's a subtlety here, in that a lax functor of double categories $\mathbb 1 \to \mathbb D$ is a loose monad, whereas their Theory 3.8 is for tight monads. Note that, to express their theory of tight monads, they really need to work with strict double functors, because the diagrams defining tight monads involve identities, which must be preserved.

Nathanael Arkor (Oct 23 2024 at 09:42):

So there is a theory for loose monads (namely, $\mathbb 1$) whose lax models in any double category $\mathbb D$ are precisely the loose monads in $\mathbb D$. We can strictify this theory to get another whose strict models are precisely loose monads.

Nathanael Arkor (Oct 23 2024 at 09:43):

But this is distinct from the theory for tight monads (and the 2-category of monads in Cat is captured by tight monads, rather than loose monads).

Evan Patterson (Oct 23 2024 at 22:57):

Right. And I think that if you took the theory for loose monads (i.e., the trivial theory), performed the strictification procedure that Nathanael mentions, and then transposed the strictified theory, you would get what is called the "theory of monads" in the paper, i.e., the theory for tight monads. So there is a sense in which the two theories are related by transposition but one has to account for the fact that lax functors are lax in one direction but strict in the other.

David Corfield (Oct 24 2024 at 10:09):

I started thinking about this topic with $M$-graded monads for a monoid $M$ in mind. One common approach is by shifting from lax functors $1 \to Cat$ to lax functors $B M \to Cat$ for the delooped monoid $B M$.

In the double category-theoretic setting, is there a path here that modifies the trivial theory (perhaps with arrows of $B M$ as tight arrows), then strictifies and transposes?

Evan Patterson (Oct 24 2024 at 18:07):

Hi David, yes, I believe that works. Specifically:

1. Start with your monoid $M$
2. View it as a category by taking the delooping $\mathsf{B} M$
3. View that as a strict double category by taking the "horizontal" double category $\mathbb{H}(\mathsf{B} M)$
4. Perform the strictification procedure to get another strict double category
5. Finally, take the transpose of that double category

The result should be a double theory whose models (lax functors into Span) are a category together with an $M$-graded monad on that category.