The 2-monad for Grothendieck fibrations

Solution 1:

Well, I eventually figured this out, though it took me longer than I would have liked! It's a bit disorienting working with this 2-monad because you end up thinking in terms of commuting squares, and deciding when to work with the "vertical composition" of the actual categories and the "horizontal composition" of the monad must take some experience. I eventually resorted to trying to write down a minimal counterexample, and then seeing what went wrong!

Since I haven't been able to find this written down anywhere, here's one way to see that the factorizations constructed above are unique, exhibiting $\mathrm{trans}_f(e)$ as a cocartesian lift of $f$.

Notation:

• Write $f^\ast e$ for the object $\mathrm{trans}_f(e)$
• Write $f^\ast$ for the morphism $\mathrm{trans}_f(e) \to e$ (which we want to show is cartesian)

I'm not sure what a good systematic notation would be.

We want to show that if $g,g': e' \to f^\ast e$ have the property that $pg = pg'$ and $f^\ast \circ g = f^\ast \circ g'$, then $g = g'$.

Step 1: (This step is not really necessary, without it just make a few notational tweaks to the next step.) It suffices to show this in the case where $g,g'$ are vertical, i.e. $pg = pg' = 1_b$.

For we could always replace $f$ with $f \circ pg$, $f^\ast$ with $(f \circ pg)^\ast$, and $g,g'$ with their canonical factorizations $\bar g, \bar g'$ through $(f \circ pg)^\ast$. The reduction follows because $(f \circ pg)^\ast = (pg)^\ast \circ f^\ast$ and $g = (pg)^\ast \circ \bar g$, $g' = (pg)^\ast \circ \bar g'$.

Step 2: It suffices to show that

$(\ast) \qquad \mathrm{trans}\big((1_b, f^\ast): \big(b \overset 1 \to p(f^\ast e) \big) \to \big( b \overset f \to p(e)\big)\big) = 1_{f^\ast e}$.

For we have $g = \mathrm{trans}\big((1_b,g): \big(b \overset 1 \to p(e')\big) \to \big(b \overset 1 \to p(f^\ast e)\big)\big)$, and similarly for $g'$. If $(\ast)$ holds, then we can postcopmose with $1_{f^\ast e}$, substitute using $(\ast)$, and by functoriality of $\mathrm{trans}$, we have $g = \mathrm{trans}\big((1_b,f^\ast \circ g): \big(b \overset 1 \to p(e')\big) \to \big(b \overset 1 \to p(f^\ast e)\big)\big)$ and a similar equation for $g'$. Now the result follows since $f^\ast \circ g = f^\ast \circ g'$.

Step 3: $(\ast)$ holds.

This follows by applying the associativity property of the algebra $\mathrm{trans}$ to the diagram

$\require{AMScd} \begin{CD} b @>{1}>> b @>{f}>> p(e) \\ @V{1}VV @VV{f}V @VV{p(1)}V \\ b @>>{f}> pe @>{1}>> p(e) \end{CD}$

viewed as a morphism in $B \downarrow (B \downarrow p)$ from the top row to the bottom.

Solution 2:

So I was thinking about your comment, and it seems like it's actually easier to prove this lax idempotency statement than to actually do your in-depth analysis.

I worked this out in the opposite variance, so replace all of your cartesian stuff with cocartesian. This answer is really just a sketch, but it gives the gist of how to show that being an algebra for the monad is equivalent to the natural map $E\to E\downarrow B$ admitting a left adjoint fibred over B.

Recall that to prove that a 2-monad is (co?)lax-idempotent, it suffices to show that for any algebra $a:TA\to A$, the unit map $A\to TA$ is its right adjoint, and moreover, the counit of this adjunction is an equivalence.

First, we'll consider our two functors:

$$\operatorname{\tau}:E\downarrow B\to E,$$ which is the algebra structure map, and

$$\rho:E\to E\downarrow B,$$

which is the unit functor. It is defined on objects by the formula $$e\mapsto\langle e,p(\operatorname{id}_{e})\rangle,$$ but more specifically, this functor can be expressed as the universal map into the pullback $E\downarrow B=E\times_{B} B^{\Delta^1}$ induced by the pair of maps $$E\xrightarrow{\operatorname{id}}E$$ and $$E\xrightarrow{p} B \xrightarrow{\operatorname{diag}} B^{\Delta^1}.$$

Since $E$ is assumed to be an algebra (or pseudo or whatever), unitality already tells us that we have an equivalence $\tau\rho \simeq \operatorname{id}_E$. We'll take this equivalence to be the counit of our adjunction, so we need to extract a unit. By looking at the diagram

$$\require{AMScd} \begin{CD} p(e) @>{f}>> b \\ @VV{f}V @VV{1}V \\ b @>{1}>> b \end{CD}$$

with the constructed lift

$$e=\tau\langle e,p(\operatorname{id}_e)\rangle \to \tau \langle e,f\rangle$$ lying over the left vertical arrow (this is just an additional datum that I didn't want to typeset in a 3d diagram), we have our prospective unit, and we'll call it $\eta$ (ok, you have to check naturality and stuff, but whatever).

Moreover, since we chose our counit to just be the aforementioned equivalence, it's enough to check by 3-for-2 that the whiskerings $\tau.\eta$ and $\eta.\rho$ are equivalences.

The fact that $\eta.\rho$ is an equivalence is completely trivial using the above square, since in that case, $f=\operatorname{id}_{p(e)}$ and we're left with the interesting case of $\tau.\eta$.

But then as you observed in your Step 3, the fact that $\tau.\eta$ is an equivalence comes from functoriality and associativity with respect to that big rectangle (mine being again dual)

$$\require{AMScd} \begin{CD} p(e) @>{1}>> p(e) @>{f}>> b \\ @V{p(1)}VV @VV{f}V @VV{1}V \\ p(e) @>>{f}> b @>{1}>> b \end{CD}.$$

In particular, this tells us that the whiskering $\tau.\eta$ can be obtained by applying $\tau$ to the outer rectangle, which is a identity map in $E\downarrow B$.

So I think that's a pretty nice and clean way to see it!