Cartesian exponentiation and monadicity

TL;DR

This paper explores the exponentiation of fibrations in quasi-category theory, proving that pullbacks form oplax colimits and applying these results to construct adjoints and reflections of fibrations.

Contribution

It provides a detailed proof that pullbacks along cocartesian fibrations form oplax colimits, extending classical results and applying them to construct adjoints and reflections in quasi-categories.

Findings

Pullback along cocartesian fibrations forms the oplax colimit of its straightening.

The forgetful functor from cartesian fibrations is monadic and comonadic.

Constructs the reflection of a cartesian fibration into a groupoidal one.

Abstract

An important result in quasi-category theory due to Lurie is the that cocartesian fibrations are exponentiable, in the sense that pullback along a cocartesian fibration admits a right Quillen right adjoint that moreover preserves cartesian fibrations; the same is true with the cartesian and cocartesian fibrations interchanged. To explicate this classical result, we prove that the pullback along a cocartesian fibration between quasi-categories forms the oplax colimit of its "straightening," a homotopy coherent diagram valued in quasi-categories, recovering a result first observed by Gepner, Haugseng, and Nikolaus. As an application of the exponentiation operation of a cartesian fibration by a cocartesian one, we use the Yoneda lemma to construct left and right adjoints to the forgetful functor that carries a cartesian fibration over B to its obB-indexed family of fibers, and prove that this forgetful functor is monadic and comonadic. This monadicity is then applied to construct the reflection of a cartesian fibration into a groupoidal cartesian fibration, whose fibers are Kan complexes rather than quasi-categories.