Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 33 of 33
On page 15 of Kelly, he says that we can easily verify axioms 1.3 and 1.4 by the “relation of $e$ to $\pi$” that the “Definition of M is equivalent to $e(M \otimes 1)=e(1\otimes e)a$. Could someone explain what that means and maybe do a quick example? I’ve got no idea.
Sure: it’s just restating how $M$ is defined by universality, via the counit $e$ of the hom-tensor adjunction. When we say that $f: A \to [B, C]$ is uniquely determined by some map $g: A \otimes B \to C$, we mean precisely that $f$ is the unique map such that
$g = (A \otimes B \stackrel{f \otimes 1_B}{\to} [B, C] \otimes B \stackrel{e_{B, C}}{\to} C)$That’s the recipe. Then, applied to page 15, $f = M$, and $g = e(1 \otimes e)a$.
Hopefully that makes sense without an example.
Okay, so in general, if L is left adjoint to R,
f:A->R(C) is uniquely determined by a map g:L(A)->C when
$g = L(A) \stackrel{L(f)}{\to} L(R(C)) \stackrel{\varepsilon_C}{\to} C.$Could you explain the reasoning behind that? I have very little experience with the unit/counit formulations of adjoints. The Hom-set definition has served me well until now.
Edit: Actually, I’m looking at it, and I just don’t see how to do the computation that we have that equality (in yours).
Heh, probably you should read Mac Lane. :-) Okay, anyway, it’s good you ask.
You are probably much more familiar with examples coming from the dual direction. Let $U: Grp \to Set$ from groups to sets be the usual forgetful functor. When we say “$F(X)$ is the free group generated by a set $X$”, we mean there is a function $\eta_X: X \to U(F(X))$ which is universal among functions from $X$ to the underlying set of a group, which means in turn that given a function $f: X \to U(G)$, there is a unique group homomorphism $g: F(X) \to G$ such that
$f = (X \stackrel{\eta_X}{\to} U(F(X)) \stackrel{U(g)}{\to} U(G))$So here $\eta_X$ is a component of the unit of the adjunction $F \dashv U$, and we are giving the dual recipe for the relationship between the map $g: F(X) \to G$ and the map $f: X \to U(G)$ in terms of the unit.
Now let’s work more generally. Suppose given functors $L: C \to D$, $R: D \to C$ and the structure of an adjunction in the form of a natural isomorphism
$\Psi_{c, d}: \hom_D(L(c), d) \cong \hom_C(c, R(d))$Now the idea is that, a la Yoneda, $\Psi$ should be completely describable in terms of what it does to identity maps. With that in mind, define the unit $\eta : 1_C \to R L$ by the formula $\eta_c = \Psi_{c, L(c)}(1_{L(c)})$. Dually, define the counit $\varepsilon : L R \to 1_D$ by the formula $\varepsilon_d = \Psi^{-1}_{R(d), d}(1_{R(d)})$. Then given $g: L(c) \to d$, the claim is that
$\Psi_{c, d}(g) = (c \stackrel{\eta_c}{\to} R(L(c)) \stackrel{R(g)}{\to} R(d))$and I’ll leave that as an exercise in Yoneda yoga, applied to $\hom_D(L(c), -) \to \hom_C(c, R(-))$. By duality, given $f: c \to R(d)$,
$\Psi^{-1}_{c, d}(f) = (L(c) \stackrel{L(f)}{\to} L(R(d)) \stackrel{\varepsilon_d}{\to} d)$Finally, these operations should obviously be mutually inverse, but that can again be entirely encapsulated Yoneda-wise in terms of the effect on identity maps. Thus, if $\eta_c \coloneqq \Psi_{c, L(c)}(1_{L(c)})$, the recipe just given for $\Psi^{-1}$ yields back
$1_{L(c)} = (L(c) \stackrel{L(\eta_c)}{\to} L R L(c) \stackrel{\varepsilon_{L(c)}}{\to} L(c))$and this is one of the famous triangular equations: $1_L = (L \stackrel{L \eta}{\to} L R L \stackrel{\varepsilon L}{\to} L)$. By duality, we have the other triangular equation $1_R = (R \stackrel{\eta R}{\to} R L R \stackrel{R \varepsilon}{\to} R)$. These two triangular equations are enough to guarantee that the recipes for $\Psi$ and $\Psi^{-1}$ are indeed mutually inverse.
One thing that you often hear is that the definition of adjunctions via units and counits is an “elementary” definition (so that by implication, the formulation in terms of hom-functors is not elementary). This means that whereas the hom-functor formulation relies on a background category of sets, the formulation in terms of units and counits is purely in the first-order language of categories and makes no reference to a background model of set theory. Thus, it would be a perfectly serviceable definition of adjunction without assumptions of local smallness.
Edit: back to your last edit at 3, hopefully this comment will clear everything up, possibly with the aid of pencil and paper in hand.
To forestall some possible frustration with my waving a wand of duality in the last comment (which is perfectly legitimate of course, since the principle of duality is an explicit formal statement), I’ll say more explicitly how it works for the equation that seemed to be bothering you in comment #2.
The claim is that $\Psi^{-1}_{c, d}: \hom_C(c, R(d)) \to \hom_D(L(c), d)$ can be defined by the formula
$\Psi^{-1}_{c, d}(f: c \to R(d)) = (L(c) \stackrel{L(f)}{\to} L(R(d)) \stackrel{\varepsilon_d}{\to} d)$where $\varepsilon_d \coloneqq \Psi^{-1}_{R(d), d}(1_{R(d)})$. This is by appeal to the proof of the Yoneda lemma applied to the transformation
$\Psi^{-1}_{-, d}: \hom_C(-, R(d)) \to \hom_D(L(-), d)$For the naturality of $\Psi^{-1}$ in the argument $(-)$ would imply that given $f: c \to R(d)$, we have a commutative square
$\array{ \hom_C(R(d), R(d)) & \stackrel{\Psi^{-1}_{R(d), d}}{\to} & \hom_D(L(R(d)), d) \\ \hom_C(f, R(d)) \downarrow & & \downarrow \hom_D(L(f), d) \\ \hom_C(c, R(d)) & \underset{\Psi^{-1}_{c, d}}{\to} & \hom_D(L(c), d) }$Chasing the element $1_{R(d)}$ down and then across, we get $f: c \to R(d)$ and then $\Psi^{-1}_{c, d}(f)$. Chasing across and then down, we get $\varepsilon_d$ and then $\varepsilon_d \circ L(f)$. This completes the verification of the claim.
Thanks for the help, Todd! You should add that to the page on adjunctions.
Also, when I was looking at the computation, in the book, I was getting confused by the suppression of subscripts. I think that we need better notation.
By the way, something along these lines I had started adding recently to adjoint functor in the section In terms of universal morphisms.
I wrote:
By the way, something along these lines I had started adding recently to adjoint functor in the section In terms of universal morphisms.
But I hope Todd finds the time and energy to expand and improve all this. Also it would be great to see the extranatural proof of the co-Yoneda lemma in the relevant nLab entry.
I just entered the proof of the co-Yoneda lemma I gave above at co-Yoneda lemma. More could be added there (including links), but I did this in a hurry.
Added content to adjunction based on comments above. Links still needed.
@Todd: I’m sorry, but I still dont understand how to do the computation
$e(M\otimes 1)=e(1\otimes e)a$. I have the diagram drawn out, but it’s the matter of showing that it commutes that I guess I’m not getting.
Unless… since M is the map $\psi(e(1\otimes e)a)$, then $psi^{-1}(M)=L([y,z]\otimes [x,y])\stackrel{L(M)}{\to}L([x,z]) \stackrel{e}{\to} z$, but $psi^{-1}(M)=e(1\otimes e)a$?
Edit: all clear nevermind.
Alright, I’ve gotten all of the above stuff, but now how do we check axiom 1.3? What does that whole thing tell us about $1\otimes M$?
We’re trying to show now that $M(M\otimes 1)=M(1\otimes M)a$.
Right. Here goes.
Preliminaries: by Mac Lane’s coherence theorem, we may assume the closed symmetric monoidal $M$ is strict monoidal, to avoid the nuisance of shuffling around associativities. (I am prepared to discuss this point further if needed.) To save typographical space, I’ll denote the internal hom $[b, a]$ in $V$ by $a^b$. Thus the composition $M$ takes the form $a^b \otimes b^c \to a^c$, and we have an adjunction isomorphism of the form
$\Phi_{y d z}: \hom_V(y, z^d) \cong \hom_V(y \otimes d, z).$A handy lemma we will need is that $\Phi(x \stackrel{f}{\to} y \stackrel{g}{\to} z^d) = (x \otimes d \stackrel{f \otimes d}{\to} y \otimes d \stackrel{\Phi(g)}{\to} z)$. That can be proven using the recipe for $\Phi$ in terms of the counit, that we discussed above.
We are trying to prove that the following diagram “D” commutes:
$\array{ a^b \otimes b^c \otimes c^d & \stackrel{a^b \otimes M}{\to} & a^b \otimes b^d \\ M \otimes c^d \downarrow & & \downarrow M \\ a^c \otimes c^d & \underset{M}{\to} & a^d }$It is enough to check that we get the same result on applying $\Phi$ to both legs of D. First, hit the leg going across and then down with $\Phi$. By the lemma, this is the composite
$a^b \otimes b^c \otimes c^d \otimes d \stackrel{1 \otimes M \otimes d}{\to} a^b \otimes b^d \otimes d \stackrel{1 \otimes e}{\to} a^b \otimes b \stackrel{e}{\to} a \qquad (1)$The first two arrows in (1) go across then down in a square:
$\array{ a^b \otimes b^c \otimes c^d \otimes d & \stackrel{1 \otimes M \otimes 1}{\to} & a^b \otimes b^d \otimes d \\ 1 \otimes 1 \otimes e \downarrow & & \downarrow 1 \otimes e \\ a^b \otimes b^c \otimes c & \underset{1 \otimes e}{\to} & a^b \otimes b }$which commutes (just hit the equation $e(M \otimes 1) = e(1 \otimes e)$ with $1 \otimes -$, here $a^b \otimes -$). So we can replace the composite of the first two arrows in (1) with the leg which goes down then across; thus the composite in (1) equals the following composite:
$a^b \otimes b^c \otimes c^d \otimes d \stackrel{1 \otimes 1 \otimes e}{\to} a^b \otimes b^c \otimes c \stackrel{1 \otimes e}{\to} a^b \otimes b \stackrel{e}{\to} a \qquad (2)$Okay, now hit the other leg of D with $\Phi$. Applying the lemma again, the result is
$a^b \otimes b^c \otimes c^d \otimes d \stackrel{M \otimes 1 \otimes d}{\to} a^c \otimes c^d \otimes d \stackrel{1 \otimes e}{\to} a^c \otimes c \stackrel{e}{\to} a \qquad (3)$Now the composites of (2) and (3) form the outer perimeter of a diagram
$\array{ a^b \otimes b^c \otimes c^d \otimes d & \stackrel{1 \otimes 1 \otimes e}{\to} & a^b \otimes b^c \otimes c & \stackrel{1 \otimes e}{\to} & a^b \otimes b \\ M \otimes 1 \otimes 1 \downarrow & & M \otimes 1 \downarrow & & \downarrow e \\ a^c \otimes c^d \otimes d & \underset{1 \otimes e}{\to} & a^c \otimes c & \underset{e}{\to} & a }$which commutes: the left square commutes by functoriality of $\otimes$, and the right square is another instance of the all-important equation $e(M \otimes 1) = e(1 \otimes e)$. Hence the composites (2) and (3) are equal, and we are done.
(You owe me one. :-) )
(You owe me one. :-) )
I owe you a bunch already =p.
If we didn’t use the coherence theorem, is the proof pretty similar?
If we didn’t use the coherence theorem, is the proof pretty similar?
Very similar, yes. But probably much harder to typeset.
You probably didn’t know this, but the topic of my dissertation was coherence theorems. Specifically the coherence problem for closed symmetric monoidal categories (which formal diagrams commute?) and related structures like star-autonomous categories.
So Todd, when you’re working things out when you have coherence diagrams, do you do something like prove the strict version first, then worry about keeping track of coherence afterwards?
I’m trying to figure out strategies to get the hang of this, and I wonder if it’s possible to do a strict proof, then weaken it.
The all-too-brief reply is that you never have to worry or weaken later: if the sentence to be decided is a non-evil sentence in the language of monoidal categories, then the truth value is automatically reflected and preserved by monoidal equivalences. So insofar as any monoidal category is monoidally equivalent to a strictified monoidal category, one may as well assume that the model in which one is working is strict monoidal, and let Mac Lane’s theorem worry about the rest so to speak – you never need to go back and “improve” the proof to take care of weakening. Commutativity of diagrams (i.e., equality of morphisms belonging to the same hom-set) falls under that heading of non-evil sentences.
I began to write out a longer reply to say this much more convincingly; what is really needed is to develop a clear picture of how monoidal strictifications work, something I learned by reading stuff by Joyal and/or Street (as in Braided Tensor Categories or Geometry of Tensor Calculus I). But I realized I won’t have time to do this now, and it may be a while before I can return to it (very busy day tomorrow). I should have time by Wednesday if not before to explain it further.
Okay, I found a bit more time, so let me make some remarks on how monoidal strictification works and how it leads to an elegant resolution of the concerns about reinstating associativities in diagrams.
Most people, when they first hear about strictifications, imagine that strictifying a monoidal category is like taking a quotient, in order to identify associativities with identities. That’s actually the wrong picture, and it leads to a lot of confusion. The right picture is that a monoidal category $M$ can be monoidally embedded in a strict monoidal category $M^{st}$, in which associativity and unit isomorphisms of $M$ are assembled into what Joyal calls “contractible networks”, or cliques (aka anaobjects). The cliques that so arise are then the objects of the strictification.
So, for example, a 4-fold tensor product like $(a^b \otimes (b^c \otimes c^d)) \otimes d$ is a vertex in a clique which consists of all five ways of bracketing $a^b \otimes b^c \otimes c^d \otimes d$ and the groupoid of associativities between them. Or more precisely, it consists of the infinitely many such bracketings with units inserted (e.g., $((a^b \otimes I) \otimes (b^c \otimes c^d)) \otimes (I \otimes d)$), as objects of the groupoid generated by associativity and unit isomorphisms between them. By Mac Lane’s coherence theorem (“all diagrams commute”), there is exactly one morphism between any two vertices in the clique, meaning that the groupoid is equivalent to a terminal groupoid, and therefore contractible.
Formally, a clique in a category $C$ consists of a contractible groupoid $G$ and a functor $F: G \to C$. A morphism between two cliques $(G, F: G \to C)$, $(G', F': G' \to C)$ is a collection of morphisms $F(g) \to F'(g')$, where $(g, g')$ ranges over $Ob(G) \times Ob(G')$, making all triangles in sight commute. (In fact, by contractibility, any one of the $F(g) \to F'(g')$ uniquely determines all the rest.) To form the monoidal strictification $M^{st}$, we take as objects those cliques in the monoidal category $M$ which arise by application of the “all diagrams commute” formulation of Mac Lane’s coherence theorem (which specifies the structure of the free monoidal category on one generator as a disjoint sum of contractible groupoids), and the morphisms in $M^{st}$ are defined to be morphisms of cliques. The precise description is laid out here, where it is indicated that the evident embedding $i: M \to M^{st}$ is an equivalence in $MonCat$.
In any case, because $M$ is embedded in $M^{st}$, any diagram we are trying to prove commutative in $M$ is physically there in $M^{st}$, but any associativities and units in the diagram get absorbed into cliques, or rather: any such associativity is one of the components $F(g) \to F'(g')$ of, and uniquely determines, an identity morphism of cliques. Therefore any such associativity in $M$ is reinterpreted as an identity in $M^{st}$, and the diagram we are trying to prove commutative in $M$ uniquely generates a corresponding “larger” diagram of cliques in the strict monoidal category $M^{st}$. So it is enough to prove the diagram commutes when interpreted in a strict monoidal category: we can then interpret the result in $M^{st}$, and the original diagram in $M$, which is embedded in the clique diagram, is then automatically commutative as well.
One may have to practice visualizing this before it all sinks in, but it’s a tremendously potent principle.
That’s precisely the way I imagined doing it, believe it or not.
That’s a great explanation, Todd; maybe it should go on the nlab at coherence theorem for monoidal categories. It’s not the way I usually think of strictification, though. In my head, the fundamental functor is not the strong monoidal embedding $M\to M^{st}$, but a strict monoidal functor $M^{st} \to M$, which happens to have a strong monoidal section forming a monoidal equivalence. From this point of view, the way coherence works with diagrams is that you draw the diagram in the strict world $M^{st}$, where it commutes, and then then map it forward into $M$ to get a corresponding diagram that also commutes there. Moreover, these two functors are the unit and counit of a strict 2-adjunction
$(-)^{st} : MonCat \rightleftarrows StrMonCat : incl$where the left adjoint is strictification and the right adjoint is the inclusion. In particular, the strictification has a universal property: strict monoidal functors out of $M^{st}$ are the same as strong monoidal functors out of $M$.
Strong monoidal functor = weak monoidal functor?
Yes, “strong” always means up to isomorphism (as opposed to lax/colax). It’s unfortunate that when people say “weak” to mean up to isomorphism (as opposed to strict), then it means that strong=weak. (-:
@Mike #20: sorry, I’m confused. I think I agree that we have the adjunction you gave at the bottom (so that my explanation involved the unit of the adjunction, $M \to i(M^{st})$). So if $M$ starts out being strict, we have a counit $(i(M))^{st} \to M$ which is strict monoidal. But I don’t see a strict monoidal $M^{st} \to M$ for non-strict $M$. I do see strong monoidal retractions $M^{st} \to M$ of the unit which are non-canonical.
So is the page on the lab incorrect?
What statement on what page?
Oh, I thought for some reason that your previous post was something along the lines of, “Oh, Mike, I guess I was wrong”, but rereading it now, it appears that you were confused with Mike’s statement, not that you were confused and that he was right.
Hmm, sorry, Todd, you’re right and I was wrong. I think what I should have said is that there are two adjunctions:
$MonCat\; \underoverset{incl}{(-)'}{\rightleftarrows} \;MonCat_s \;\underoverset{incl}{quot}{\rightleftarrows} \;StrMonCat_s$where $MonCat_s$ denotes non-strict monoidal categories and strict monoidal functors. The left adjoint $quot$ is the “wrong way to prove coherence” by taking a quotient, but its composite with the “pseudo morphism classifier” $(-)'$ is a correct strictification functor $(-)^{st}$, i.e. $M^{st} = quot(M')$. The strict functor I was thinking of is the counit $M'\to M$, which is a surjective equivalence in $MonCat$ (but not in $MonCat_s$).
How do you describe the pseudo morphism classifier?
The quick and dirty way is to say that its objects are formal parenthesized strings of objects of M, and the functor $M' \to M$ is fully faithful. The elegant way is to say that it’s a codescent object, as described in Steve Lack’s paper “codescent objects and coherence.”
@Mike #27 – thanks; that makes sense.
I made a little beginning for coherence theorem for monoidal categories. Rather a lot more to be filled in.
I think I don’t understand the relationship between the “all diagrams commute” coherence theorem and the strictification theorem as well as I thought I did. A naive version of the “all diagrams commute” theorem of course follows from the strictification theorem since all diagrams commute in a strict monoidal category, while your description shows where the all-diagrams-commute theorem comes into proving the strictification theorem. (In other versions of the strictification theorem, it comes in in other places.) But there’s a more abstract version of the all-diagrams-commute theorem which says that the free strict monoidal category on some data is equivalent to the free non-strict one; how is that related to the string of adjunctions I just wrote down?
Sorry for the delay in responding to your question, Mike. I’m not sure how well the following observations answer it, but here goes.
Let’s see: the free monoidal category $F[C]$ generated by a category $C$ is, in the notation at club, $F[1] \circ C$, where $F[1]$ is the free monoidal category on one generator. When I say “free monoidal” here, this means the left adjoint to the forgetful functor
$MonCat_s \to Cat$It looks like your $(-)': MonCat \to MonCat_s$ can be described as taking a monoidal category $M$, which has an underlying endospan $M_0 \leftarrow M_1 \to M_0$, to a monoidal category $M'$ whose underlying endospan is the span composite
$F[M]_0 \stackrel{p_0}{\to} M_0 \stackrel{M_1}{\to} M_0 \stackrel{(p_0)^*}{\to} F[M]_0$where $p: F[M] \to M$ is the counit at $M$ of the adjunction for the monadic functor $MonCat_s \to Cat$, and $p_0$ is the underlying function between object-sets. So in other words, this endospan may be equivalently written $(M')_1 \to F[m]_0 \times F[M]_0$.
The free strict monoidal category on a category $C$ would be $\mathbb{N} \circ C$. There is a quotient functor $q: F[C] = F[1] \circ C \to \mathbb{N} \circ C$ (induced from the obvious functor $F[1] \to \mathbb{N}$) which is a monoidal equivalence, as you hinted in speaking of the abstract version of the all-diagrams-commute theorem. This induces a quotient function $q_0: F[C]_0 \to (\mathbb{N} \circ C)_0$. Now if $M$ is a monoidal category, then according to what you wrote in #27, $(\mathbb{N} \circ M)_0$ is the underlying object-set $(M^{st})_0$. The underlying morphism-set is $quot(M')_1 = (M^{st})_1$.
Adopting the clique point of view on the construction of the monoidal category $M^{st}$, one connection between the string of adjunctions you wrote down and the abstract all-diagrams-commute theorem is concentrated in the statement that the following diagram is a pullback:
$\array{ (M')_1 & \stackrel{\langle dom_{M'}, cod_{M'} \rangle}{\to} & F[m]_0 \times F[M]_0 \\ \pi \downarrow & & \downarrow q_0 \times q_0 \\ (M^{st})_1 & \underset{\langle dom, cod \rangle}{\to} & (M^{st})_0 \times (M^{st})_0 }$where $\pi$ is the quotient map $(M')_1 \to quot(M')_1$, where $quot$ is your functor $MonCat_s \to StrMonCat_s$.
I think this can be understood by viewing $M'$ as a monoidal category of pointed cliques. (A pointed clique is exactly what one might think: a triple $(g, G, F: G \to C)$ where $G$ is a contractible groupoid and $g$ is an object of $G$. A morphism $(g, G, F: G \to C) \to (g', G', F': G' \to C)$ is just the component $h_{g, g'}$ of a morphism of cliques $h: (G, F: G \to C) \to (G', F': G' \to C)$, or rather the pair $(h_{g g'}, h)$.)
Then the functor $M' \to quot(M')$ can be understood as the process of forgetting the point of the pointed clique.
Thanks Todd! Let me rephrase some of that in language more familiar to me. I think what you wrote about span composites is correct, but I’d be more inclined to say the same thing by saying that $M'$ is the (bo,ff) factorization of the counit $p\colon F[M] \to M$. And similarly, saying that that square is a pullback is just saying that the functor $M' \to M^{st}$ is fully faithful. (In fact, of course, it is an equivalence, since both $M'$ and $M^{st}$ are equivalent to $M$.)
I don’t quite understand the pointed cliques yet. Partly I don’t see why my $M^{st}$, being the left adjoint as above, should necessarily the same as your $M^{st}$ constructed using cliques – is it?
But let me say something different which this triggered in my head, namely how to deduce strictification from coherence. Suppose we know that $F[M] \to F_s[M]$ is an equivalence (where $F_s$ denotes the free strict monoidal category). Then from some inverse to it we obtain a map $F_s[M] \to F[M] \to M$, and we can define $M^{st}$ to be the (bo,ff) factorization of this. It inherits a strict monoidal structure from $F_s[M]$, and its map to $M$ is fully faithful by definition, and surjective on objects since we have $M$ sitting inside $F_s[M]$; thus every monoidal category $M$ is equivalent to a strict monoidal category. This is essentially Power’s “general coherence result” for pseudoalgebras over 2-monads, composed with the equivalence $F \simeq F_s$ to turn an $F$-algebra (a monoidal category) into a pseudo $F_s$-algebra (an unbiased monoidal category).
I think a proof of coherence from strictification can also be derived with a little more work. The 2-monad morphism $F \to F_s$ induces a functor $StrMonCat \to MonCat$ over $Cat$, where in both 2-categories we include pseudo morphisms (i.e. strong=weak monoidal functors). This functor is clearly 2-fully-faithful, and assuming strictification, it is also essentially surjective up to equivalence; hence it is a biequivalence. Moreover, each forgetful functor $MonCat \to Cat$ and $StrMonCat \to Cat$ has a left biadjoint, namely $F$ and $F_s$ respectively, so the fact of this equivalence over $Cat$ means that these biadjunctions must induce equivalent (pseudo)monads, i.e. $F\simeq F_s$. (The proof that $F$ and $F_s$ are left biadjoints landing in the 2-categories of pseudo morphisms, not just strict ones, is in Blackwell-Kelly-Power and uses properties of the pseudo morphism classifier $(-)'$.)
1 to 33 of 33