A comonad for Grothendieck fibrations

We would like to produce a free Grothendieck fibration on a functor F:\ensuremath{\mathpzc{A}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}}\ensuremath{\mathpzc{B}}. So, for every object a in A and map f:b\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} F(a), we want to force the existence of a cartesian lifting of f to a. The idea is then to freely add all pairs \@ifnextchar[{\CCO}{\CCO[6ex]}{b}{f}{a}{F(a)}, and thus to consider the comma category \ensuremath{\mathpzc{B}}/F.(We shall often write an object in a comma category \ensuremath{\mathpzc{B}}/F as a pair [ bfaF(a) instead of the appropriate triple (b,a,\xymatrix@1@=6ex{b\ar[r]|-{f}&F(a)}) when no confusion arises.) This can be compared for example to the construction of the free monoid on a set.

Clearly the functor underlying the 2-monad \ensuremath{\mathbf{M}}\xspace is polynomial, see [GambinoN:polfap].

The 2-monad \ensuremath{\mathbf{M}}\xspace extends to a colax idempotent 2-monad on the 2-category \ensuremath{\mathpzc{Cat}}^2 of arrows of \ensuremath{\mathpzc{Cat}}, that applies \ensuremath{\mathpzc{Cat}}/B into itself and commutes with change-of-base functors. However, such extension does not seem to work well with the rest of the theory. See for example Remark 2.7 and Remark 3.5.

(a) Recall from [StreetR:fibbic] that a functor F :\ensuremath{\mathpzc{A}} \mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} \ensuremath{\mathpzc{B}} is a Street fibration if, for every object a in \ensuremath{\mathpzc{A}} and arrow f:b \mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} F(a), there are an isomorphism h_a:b_a \mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} b and a cartesian arrow into a over the composite fh_a : b_a \mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} F(a). Street fibrations can be characterized as pseudo-algebras for the “same” monad Mof Grothendieck fibrations, but lifted to the pseudo-fibre \ensuremath{\mathpzc{Cat}}/\!/\ensuremath{\mathpzc{B}}, see [StreetR:fibbic]. The 2-category \ensuremath{\mathpzc{Cat}}/\!/\ensuremath{\mathpzc{B}} has the same objects as \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}}, 1-cells are triangles filled with a natural isomorphism, and 2-cells are those 2-cells in \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}} which commute with the two natural isomorphisms. For the characterization of Street fibrations, it is enough to observe that the underlying functor of Mlifts, and that unit and counit are still natural. The rest of the proof works the same as for Proposition 2.6.

(b) As Mis a monad also on the whole 2-category \ensuremath{\mathpzc{Cat}}^2, we can also look at the pseudo-algebras there. It is easy to see that the strict algebras are again split Grothendieck fibrations. Following [KockA:monfws], pseudo-algebras for Mon \ensuremath{\mathpzc{Cat}}^2 can also be characterized as those functors F such that the unit (\ensuremath{\mathrm{Id}_{}},\eta_F) has a right adjoint in \ensuremath{\mathpzc{Cat}}^2. Let

be such a right adjoint. In particular, the functor B is isomorphic to the identity on \ensuremath{\mathpzc{B}} via an isomorphism \zeta:B\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}}\ensuremath{\mathrm{Id}_{\ensuremath{\mathpzc{B}}}}. Unfolding the other conditions one sees that for every object a in A and arrow f:b \mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} F(a), there is a cartesian arrow into a over f\zeta_b:B(b) \mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} F(a). It follows that a pseudo-algebra for Min \ensuremath{\mathpzc{Cat}}^2 is a Street fibration. However, the converse does not seem to hold. Indeed, in both cases, given a in A and f:b\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} F(a), we can choose an isomorphism h such that the composite fh has a cartesian lift to a. But in a Street fibration the choice of h depends on the object a, whereas in a pseudo-algebra in \ensuremath{\mathpzc{Cat}}^2 the choice is given uniformly for every object a by the isomorphism \zeta_b.

Notice also that a normal pseudo-algebra in \ensuremath{\mathpzc{Cat}}^2, being a right adjoint right inverse to the unit, is in particular an arrow in \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}} and, in fact, a right adjoint right inverse to the unit in \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}}. It follows that a normal pseudo-algebra in \ensuremath{\mathpzc{Cat}}^2 is a normal Grothendieck fibration. This fact suggests that (normal) Street fibrations are strictly more general than pseudo-algebras in \ensuremath{\mathpzc{Cat}}^2.

The 2-monad \ensuremath{\mathbf{M}}\xspace can thus be expressed as the composition of left adjoint 2-functors. This observation is original.

The adjunction \mathord{{{\operator@font{dom}}}}_\bullet\dashv\mathord{{{\operator@font{dom}}}}^* is the usual change of base. And the functor \mathord{{{\operator@font{cod}}}}^* has indeed a right 2-adjoint \mathord{{{\operator@font{cod}}}}_* because \mathord{{{\operator@font{cod}}}} is an opfibration. Hence it is 2-exponentiable as stated in [GiraudJ:metdld, Théorème 4.4] and in [ConducheF:sujdea, 2nd Proposition on p. 894], but for an explicit proof of the characterisation of exponentiable functors, see [StreetR:powf] where such functors are called powerful. See also [StreetR:comfat, Theorem 2.16] for the extension to the case of internal categories in a cartesian closed category with pullbacks.

For the comonadicity of fibrations, it is essential to restrict to fibrations over a fixed base \ensuremath{\mathpzc{B}}. The factorization of Proposition 3.1 indeed only holds for the 2-monad restricted to \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}}.

We can calculate the 2-comonad \ensuremath{\mathbf{N}}\xspace=(\mathord{{{\operator@font{cod}}}}_*\mathord{{{\operator@font{dom}}}}^*,\mu',\eta') more explicitly. Indeed, as observed by [GiraudJ:metdld], the isomorphism between homsets that gives the adjunction \mathord{{{\operator@font{cod}}}}^*\dashv\mathord{{{\operator@font{cod}}}}_* determines the explicit definition of \mathord{{{\operator@font{cod}}}}_*, up to isomorphism. Notice that \mathord{{{\operator@font{dom}}}}^* sends every functor F:\ensuremath{\mathpzc{A}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}}\ensuremath{\mathpzc{B}} to the forgetful F/\ensuremath{\mathpzc{B}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} \ensuremath{\mathpzc{B}}^{\ensuremath{\mathpzc{2}}}. Since the fibre of \mathord{{{\operator@font{cod}}}} over b in B is \ensuremath{\mathpzc{B}}/b, we find that N(F) is the projection on the first component \ensuremath{\mathpzc{G}}_F\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} \ensuremath{\mathpzc{B}}, where \ensuremath{\mathpzc{G}}_F is the category defined as follows. Its objects are pairs b,X where b is an object in B and X is a functor such that

commutes. An arrow

consists of an arrow

in B and a natural transformation

with vertical components.

N then sends every morphism H:F\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} F' in \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}} to \ple{\ensuremath{\mathrm{Id}_{}},H\circ -}:\ensuremath{\mathpzc{G}}_F\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}}\ensuremath{\mathpzc{G}}_{F'}, which is over \ensuremath{\mathpzc{B}}. And the action of N on 2-cells is analogous.

By the mating calculus, the counit \eta' of the 2-comonad \ensuremath{\mathbf{N}}\xspace is the composite

where \xi is the counit of \mathord{{{\operator@font{cod}}}}^*\dashv\mathord{{{\operator@font{cod}}}}_*, whose components are evaluation functors, and \zeta is the counit of \mathord{{{\operator@font{dom}}}}_\bullet\dashv\mathord{{{\operator@font{dom}}}}^*. Given a functor F:\ensuremath{\mathpzc{A}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}}\ensuremath{\mathpzc{B}}, the component of \eta' on F is then given by “evaluating at the identity”

The comultiplication \mu' of the 2-comonad \ensuremath{\mathbf{N}}\xspace has component \mu'_F on F:\ensuremath{\mathpzc{A}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} \ensuremath{\mathpzc{B}} given by the functor \ensuremath{\mathpzc{G}}_F\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} \ensuremath{\mathpzc{G}}_{N(F)} that sends \ple{b,X} to \ple{b,\overline{X})} with

After Remark 3.8, we will be able to see \mu'_F as the coalgebra structure map of the split fibration N(F).

The pseudo-coalgebra structure map of a cloven fibration p:\ensuremath{\mathpzc{E}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}}\ensuremath{\mathpzc{B}} is, explicitly,

where \alpha sends E in E to the triangle

with (-)^* E calculating the domains of the chosen cartesian liftings to E, and is extended by cartesianity to a functor \alpha:\ensuremath{\mathpzc{E}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} \ensuremath{\mathpzc{G}}_F.

The rest of the pseudo-coalgebra structure of p is given by the isomorphisms \alpha_{\eta'} and \alpha_{\mu'} that regulate respectively liftings in the chosen cleavage of p of an identity and of a composite.

The well-known observation that the component at F of the comultiplication \mu'_F of the comonad N is precisely the coalgebra structure map of the split fibration N(F) translates, in the notation of Remark 3.6, as

That is, \overline{X} shows the explicit chosen cartesian liftings for the split fibration N(F), which can be read from Proposition 3.7.

The fact that N gives a right adjoint to U could also be proved directly, showing that the counit \eta' is 2-universal. The component on p of the unit of the adjunction is given by the coalgebra structure map of the split fibration p, described in Remark 3.8. However a direct proof is considerably more involved than the one that just follows from the factorization of the 2-monad as the composite of two left adjoint 2-functors. It is indeed much easier to calculate the right adjoint to the monad Mthan the right adjoint to U.

We briefly describe a strategy for a direct proof of the comonadicity of U.

In order to prove that a coalgebra (F:\ensuremath{\mathpzc{A}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} \ensuremath{\mathpzc{B}},\alpha:F\tikz[baseline=-0.5ex, shorten <=2pt, shorten >=2pt] \draw[->] (0,0) -- (1.4em,0); N(F)) for the 2-comonad \ensuremath{\mathbf{N}}\xspace is a split fibration, start from a diagram

and construct a cartesian lifting of f to a. The idea is to apply \alpha to such a diagram and compute the cartesian lifting with respect to the split fibration N(F) of f to \alpha(a)=\ple{F(a),X:\ensuremath{\mathpzc{B}}/(F(a))\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} \ensuremath{\mathpzc{A}}}. Next, applying the counit \eta'_F recovers the starting data of the diagram above and exhibits a lifting of f to a:

Note that, by Remark 3.6,

One is left with proving directly that such a lifting of f to a is cartesian, whose proof is lengthy. The proof of Theorem 3.4 uses instead what was already known for the 2-monad \ensuremath{\mathbf{M}}\xspace.

Using the explicit construction of descent objects in \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}} given in Proposition 5.2, one can recover the explicit construction of the right splitting of fibrations of [GiraudJ:cohna]. Let p:\ensuremath{\mathpzc{E}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}}\ensuremath{\mathpzc{B}} be a cloven fibration, with pseudo-coalgebra structure for the 2-comonad \ensuremath{\mathbf{N}}\xspace given by a map \alpha:p\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} N(p) and isomorphisms \alpha_{\eta'} and \alpha_{\mu'} (see Remark 3.8). Following the concrete recipe of [Lack:codoc] to strictify pseudo-coalgebras, we have that R(p) is the descent object in \ensuremath{\mathpzc{SpFib}}(\ensuremath{\mathpzc{B}}) of the coherence data

By Proposition 5.2 and Proposition 5.3, such descent object is calculated in \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}}, as an inserter followed by two equifiers. The first step is to calculate the iso-inserter of

By Proposition 5.2, such iso-inserter is given by the category whose objects are all pairs ({\ple{b,X}},\phi) with {\ple{b,X}} in \ensuremath{\mathpzc{G}}_p and \phi:\mu'_p(\ple{b,X})\cong (N\alpha)(\ple{b,X}) an isomorphism in \ensuremath{\mathpzc{G}}_{Np} over the identity, and whose morphisms ({\ple{b,X}},\phi)\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} ({\ple{b',X'}},\phi') are morphisms \ple{h,\lambda} in \ensuremath{\mathpzc{G}}_p such that (N\alpha)(\ple{h,\lambda})\circ \phi=\phi'\circ \mu'_p(\ple{h,\lambda}).

In the notation of Remark 3.6, \phi is a natural isomorphism

over \ensuremath{\mathpzc{B}}. For every f:a\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} b in \ensuremath{\mathpzc{B}}, the component \phi_f of \phi on f is given by a natural isomorphism

over \ensuremath{\mathpzc{B}}. For every u:a'\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} a in \ensuremath{\mathpzc{B}}, the component \phi_{f,u} of \phi_f on u is given by an isomorphism

in \ensuremath{\mathpzc{E}} over \ensuremath{\mathrm{id}_{a'}}. Naturality of \phi_f on u yields in particular a commutative triangle

where \mathord{{{\operator@font{Cart}}}}(u,X(f)) is the chosen cartesian lifting of u to X(f). This triangle subsumes all the other conditions \phi needs to satisfy, by cartesianity arguments.

So an arbitrary object of the iso-inserter is equivalently given by \ple{b,X} equipped with chosen isomorphisms \phi_{f,u} that satisfy the commutative triangle above. Under the axiom of choice, this is equivalent to restrict to those \ple{b,X} in \ensuremath{\mathpzc{G}}_p such that X is a cartesian functor, i.e.a functor that preserves the cleavage up to isomorphism.

The naturality-like condition that the morphisms of the iso-inserter need to satisfy is equally subsumed under the commutative triangle above. So that morphisms in the iso-inserter are simply all morphisms \ple{h,\lambda} in \ensuremath{\mathpzc{G}}_p.

In order to produce a descent object, we should then take two equifiers to force the following two conditions (the second one is a cocycle condition):

where the isomorphisms \alpha_{\eta'} and \alpha_{\mu'} are those of the pseudo-coalgebra structure \alpha on p, i.e.those given by the chosen cleavage of p (see Remark 3.8). Both conditions are however true for all (\ple{b,X},\phi), as they are subsumed by the commutative triangle above, by cartesianity arguments. So the iso-inserter calculated above is already the descent object we needed.

We conclude that the concrete recipe of [Lack:codoc] to strictify pseudo-coalgebras translates as taking R(p) to be the restriction of N(p) to those objects \ple{b,X} with X that preserves the cleavage up to isomorphism (actually with chosen isomorphisms), without any further condition on morphisms. This is precisely the right splitting construction of [GiraudJ:cohna].

We note another way to recover the right adjoint splitting of fibrations. By Theorem 3.4, the pseudo-coalgebra structure \alpha of a cloven fibration p is a right adjoint right inverse of the counit \eta'_F:N(F)\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}} F. This \alpha is a homomorphism of fibrations which embeds F into the split fibration N(F). Closing under isomorphism the image of F into N(F) provides a split fibration equivalent to F.

This recovers also the right splitting construction of [GiraudJ:cohna], as by Remark 3.8 such image is made of triangles

and (-)^*E preserves the cleavage up to isomorphism.

Recall that a factorization system on a 2-category is enhanced when squares which are pseudo morphisms in \ensuremath{\mathpzc{Cat}}^{\ensuremath{\mathpzc{2}}} with domain in E and codomain in M—so they commute up to an invertible 2-cell \alpha—can be filled with a unique diagonal such that the upper triangle commutes strictly and the lower one commutes up to a unique invertible 2-cell which coincides with \alpha on the whole square.

The factorization system on \ensuremath{\mathpzc{Cat}} where E consists of the bijective-on-objects functors and M consists of the fully-faithful functors, is enhanced. This lifts to a factorization system on the 2-category \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}}, which is easily seen to be enhanced.

The other two assumptions of Theorem 5.7 are easily verified for the 2-monad \ensuremath{\mathbf{M}}\xspace. Indeed a fully faithful functor with a right quasi-inverse is clearly an equivalence. And it is easily seen from the definition of the 2-monad \ensuremath{\mathbf{M}}\xspace (see Proposition 2.3) that M preserves bijective-on-objects functors. In fact, the action of M on morphisms in \ensuremath{\mathpzc{Cat}}/\ensuremath{\mathpzc{B}}, induced by the universal property of the comma object, is almost trivial.

Power’s insight is that an enhanced factorization system can be used to extract a strict algebra from a pseudo one. In particular, the underlying object of the strict algebra can be computed factoring the pseudo-algebra map.

Let p:\ensuremath{\mathpzc{E}}\xymatrix@1@C=1.6em{{}\ar@<-.2ex>[r]&{}}\ensuremath{\mathpzc{B}} be a cloven fibration, with pseudo-algebra structure for the 2-monad \ensuremath{\mathbf{M}}\xspace given by a map \alpha:M(p)\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} p and isomorphisms \alpha_\eta and \alpha_\mu that regulate respectively liftings in the chosen cleavage of p of an identity and of a composite. Using (the proof of) Theorem 5.7, we obtain that the underlying object of the left splitting L(p) of p is the full image of the pseudo-algebra map \alpha:M(p)\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} p. That is, the objects are the same of M(p), but an arrow from (f,a) to (f',a') is an arrow \alpha(f,a) \mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} \alpha(f',a') in \ensuremath{\mathpzc{E}} and thus an arrow f^*a\mathrel{\xymatrix@1@=2.5ex{*=0{}\ar[];[r]&*=0{}}} (f')^*a' in \ensuremath{\mathpzc{E}}. This is precisely the left splitting construction of [GiraudJ:cohna].