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: Transporting a lax algebra structure across an adjunction

Brendan Murphy (Oct 22 2023 at 19:03):

Let $\mathsf{C}$ be a strict $2$-category; I'm going to write composition of both $1$ and $2$-cells with $\circ$, write $1$-cell identities as $\operatorname{id}$, and write both left and right whiskering as a binary operator $\#$. Suppose $T$ is a strict $2$-monad on $\mathsf{C}$ (i.e. a $\mathsf{Cat}$-enriched monad) with unit $\eta : \operatorname{Id}_{\mathsf{C}} \to T$ and multiplication $\mu : T^2 \to T$. For an object $X$ of $\mathsf{C}$, define a $T$-prealgebra structure on $X$ to be the data of a $1$-cell $\theta : T(X) \to X$ and $2$-cells $\zeta : \operatorname{id}_X \to \theta \circ \eta_X$, $\omega : \theta \circ T(\theta) \to \theta \circ \mu_X$. A prealgebra structure is a lax algebra if the data satisfies some coherence axioms. For another object $Y$ define a preadjunction from $X$ to $Y$ to be the data of $1$-cells $g : X \to Y$, $f : Y \to X$ and $2$-cells $\alpha : \operatorname{id}_Y \to g\circ f$, $\beta : f \circ g \to \operatorname{id}_X$. Such a thing is an adjunction if $\alpha, \beta$ satisfy the triangle identities. Given a prealgebra structure on $X$ and a preadjunction from $X$ to $Y$ I can define a prealgebra structure on $Y$ by

$$\begin{align*} \overline{\theta} &: T(Y) \to Y \\ \overline{\theta} &= g \circ \theta \circ T(f) \\ \overline{\zeta} &: \operatorname{id}_Y \to \overline{\theta} \circ \eta_Y \\ \overline{\zeta} &= (g \mathbin{\#} \zeta \mathbin{\#} f) \mathbin{\circ} \alpha \\ \overline{\omega} &: \overline{\theta} \circ T(\overline{\theta}) \to \overline{\theta} \circ \mu_Y \\ \overline{\omega} &= (g \mathbin{\#} \omega \mathbin{\#} T^2(f)) \mathbin{\circ} ((g\circ \theta) \mathbin{\#} T(\beta) \mathbin{\#} (T(\theta) \circ T^2(f))) \end{align*}$$

I haven't checked the coherence axioms, but it seems very likely to me that if the prealgebra is a lax algebra and the preadjunction is an adjunction, this data should give a lax algebra structure on $Y$. Does anyone know a reference for this, if correct? I'd also like a higher level pov on this construction if possible

Brendan Murphy (Oct 22 2023 at 19:27):

fe95fb90-5e7f-41ea-ab94-1aa7ce3cbd2d.png
Maybe this description enables the kind of high level argument I'm looking for? But I'm not totally sure what the codensity monad of an object (internal to a $2$-category) is

Brendan Murphy (Oct 22 2023 at 19:41):

(the application I have in mind is transporting a double category structure on a graph of categories, understood as a normalized pseudo-algebra structure over an appropriate monad, down to a coreflective subcategory of the vertices/edges; normality would be preservex because in my application the coreflection is strictly idempotent)

Brendan Murphy (Oct 22 2023 at 23:45):

It seems like this is basically a "doctrinal adjunction" thing, but that's for strict (or pseudo) algebras (and also i don't understand doctrinal adjunction)

Kevin Arlin (Oct 23 2023 at 17:42):

I'm not strongly recommending it, but to flesh out one of your ideas: there is a simple explicit description for the codensity 2-monads: we have $\langle X,X\rangle Y=\mathsf C(Y,X)\pitchfork X.$ Now considering the lax morphism $T\to \langle X,X\rangle,$ this rephrases your question as whether an adjunction induces a lax morphism $\langle X,X\rangle\to \langle Y,Y\rangle.$ Or, in other words again, you want to know whether this adjunction makes $Y$ into an $X$ (i.e. an $\langle X,X\rangle$-algebra. I don't immediately see that this is any better than checking the proposal you already have by hand, though.

Kevin Arlin (Oct 23 2023 at 17:43):

I'm dubious whether doctrinal adjunction is of much use here because you don't start out knowing that either adjoint does anything like what you want, laxly or oplaxly.

Brendan Murphy (Oct 23 2023 at 18:31):

Ah you're right, I misunderstood something on the nlab page for doctrinal adjunction. It describes it double categorically by saying the forgetful (double) functor U : T-Alg -> QK "creates conjunctions". But my problem isn't about lifting isn't about lifting conjoints to some U(u), it's about lifting conjoint pairs where only the source of the horizontal morphism is assumed to be of the form U(X)

Brendan Murphy (Oct 23 2023 at 18:32):

I'd only been talking about lifting the algebra structure on Y previously, but I think the adjunction itself should also lift to a lax/oplax adjunction of lax T algebras

Brendan Murphy (Oct 23 2023 at 18:35):

The reason I thought the codensity idea might be better would be that I hoped we could exploit functorality of the codensity 2 monad. It seems like your description would immediately show how to endow it with the structure of a pseudofunctor into End(C) at least? "pseudo" because the tensor isn't a strict 2-functor Cat × C -> C

Brendan Murphy (Oct 23 2023 at 18:38):

I found the approach sort of unappealing because it relies on the existence of the codensity 2-monad, though, while my explicit construction seems to work for any strict 2-category (what I wrote so for should even work for weak ones with appropriate associators and unitors inserted, I just didn't want to get bogged down in them)

Kevin Arlin (Oct 23 2023 at 19:00):

Eh, I mean, do you really have a 2-category you want to do monads on that isn't even complete? 2-categories companion section 5 has a number of comments on functoriality of codensity you might find useful if you haven't seen them.

Brendan Murphy (Oct 23 2023 at 19:09):

No, that's a good point haha. Just feels unsatisfying

Brendan Murphy (Oct 23 2023 at 19:09):

I'll take a look there

Kengo Hirata (Oct 25 2023 at 11:49):

I think that is the dual of Theorem 8.3. in https://arxiv.org/abs/1209.4436, or Lemma4.3.1 in my thesis https://arxiv.org/abs/2301.06420 . But you might be able to find another older reference.

Kevin Arlin (Oct 25 2023 at 17:13):

At a glance it looks like your lemma also just gives the structure maps, probably the same as Brendan's, without writing anything out about checking the axioms (naturally enough.) The Lack citation is only about strict algebras, but the citation in the Lack citation to Kelly-Lack, monoidal functors and transport of structure, theorem 3.5, looks more promising for a big fancy clean proof.

Brendan Murphy (Oct 27 2023 at 02:37):

Thanks to both of you!

Brendan Murphy (Oct 27 2023 at 02:38):

If I do end up writing this up I'll probably just give the structure maps and then link to a formally verified proof that they satisfy coherence, or something. Not sure it would be enlightening to give it on paper