Fibred Adjunction

A fibred adjunction over a pair of Adjoint Functors $L\dashv R:\mathcal{B}\leftrightarrows\mathcal{C}$ is a pair of Fibred Functors $L^{\prime}:\mathcal{F}\to_{L}\mathcal{E}$, $R^{\prime}:\mathcal{E}\to_{R}\mathcal{F}$ along with a pair of Displayed Natural Transformations $\eta^{\prime}:\mathrm{Id}\to_{\eta}R^{\prime}\circ L^{\prime}$, $\varepsilon^{\prime}:L^{\prime}\circ R^{\prime}\to\mathrm{Id}$ that satisfy displayed versions of the zig-zag identities

• $\varepsilon^{\prime}_{R^{\prime}(X)}\circ L^{\prime}(\eta^{\prime}_{X})=mathrm {id}{ifx..lse\par i}$

• $R^{\prime}(\varepsilon^{\prime}_{X})\circ\eta^{\prime}_{L^{\prime}(X)}=mathrm{ id}{ifx..lse\par i}$

Properties

• A fibred adjunction is a Displayed Adjunction in the Displayed Bicategory of Cartesian Fibrations.

• A Fibred Functor

  has a left (resp. right) adjoint if and only if for every $I:\mathcal{B}$, every restriction $F_{I}:\mathcal{E}_{I}\to\mathcal{F}_{I}$ to the corresponding Fibre Categories has a left (resp. right) adjoint $L_{I}$ such that these adjoints satisfy a Beck-Chevalley Condition:

  • The canonical map $L_{I}(u^{*}(X))\xrightarrow{\varepsilon\circ L_{I}(\langle\eta\circ\pi\rangle) }u^{*}(L_{J}(X))$ is invertible.

  The key observation is that when we can extend a family of functors $L_{I}$ between Fibre Categories to a fibred functor by giving a family of Cartesian Morphisms $\alpha_{u}:{{L_{I}(u^{*}(X))}\to_{u}{L_{J}(X)}}$. Our adjoint actually gives us such a family via:

  $\par L_{I}(u^{*}(X))\xrightarrow{\varepsilon\circ L_{I}(\langle\eta\circ\pi \rangle)}u^{*}(L_{J}(X))\xrightarrow{\pi}L_{J}(X)$

  $\pi$ is clearly cartesian, so if $\varepsilon\circ L_{I}\langle\eta\circ\pi\rangle$ is invertible then the composite must be cartesian.

References

• Categorical Logic and Type Theory, 1.8