Presentability and topoi in internal higher category theory

Abstract

The goal of this article is to develop the theory of presentable categories and topoi internal to an arbitrary $\infty$-topos $\mathcal{B}$. Our main results are internal analogues of Lurie's and Lurie-Simpson's characterisations of presentable $\infty$-categories and $\infty$-topoi. In the process, we introduce a theory of internal filteredness and accessible internal categories and establish a number of structural results about presentable $\mathcal{B}$-categories such as adjoint functor theorems and the existence of an internal analogue of the Lurie tensor product. We also compare these internal notions with external variants. We show that $\mathcal{B}$-modules embed fully faithfully into presentable $\mathcal{B}$-categories and prove that there is an equivalence between topoi internal to $\mathcal{B}$ and $\infty$-topoi over $\mathcal{B}$. We also include a number of applications of our results, such as a general version of Diaconescu's theorem for $\infty$-topoi and a characterisation of locally contractible geometric morphisms in terms of smoothness.

Theorems & Definitions (752)

• Theorem A
• Theorem B
• Theorem C
• Theorem D
• Definition 1.2.1.1: MYoneda
• Remark 1.2.1.2: MYoneda
• Remark 1.2.1.3
• Proposition 1.2.1.4: MYoneda
• Proposition 1.2.1.5: MYoneda
• Definition 1.2.1.6