Presentability and topoi in internal higher category theory

TL;DR

This paper develops the theory of presentable categories and topoi internal to an arbitrary ∞-topos, establishing internal analogues of key characterizations and structural results in higher category theory.

Contribution

It introduces internal filteredness and accessible categories, proves structural theorems, and compares internal and external notions, advancing the understanding of internal higher category theory.

Findings

Internal analogues of Lurie's characterizations established

Full embedding of ∞-modules into presentable ∞-categories shown

Equivalence between internal topoi and ∞-topoi over a base topos proved

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.