Gabriel-Ulmer duality for $\infty$-categories

Question

Gabriel-Ulmer duality states that 2-categories $\mathrm{Lex}$ (of small finitely complete categories and functors preserving finite limits) and $\mathrm{LFP}$ (of locally finitely presentable categories and finitary right adjoints) are dual. This duality should be true in the setting of $\infty$-categories if we replace $\mathrm{Lex}$ with the $\infty$-category of finitely complete and idempotent complete $\infty$-categories and $\mathrm{LFP}$ with the $\infty$-category of locally finitely presentable $\infty$-categories. Is there a proof of this fact in the literature?

Answer 1

I'm not aware of anyone writing the proof down, but I think we can patch it together as an easy consequence of several facts in Lurie's Higher Topos Theory (henceforth HTT).

The statement, as I understand it, is that the functor $$\mathrm{Fun}^{lex}(-,\mathrm{Space}):(\mathrm{Cat}_\infty^{lex,\natural})^{op}\to\mathrm{Pr}^R_\omega$$ is an equivalence of $\infty$-categories (in fact we'd like it to be an equivalence of $(\infty,2)$-categories, but I'm not going to address that now), where

• $\mathrm{Cat}_\infty^{lex,\natural}$ is the $\infty$-category of small idempotent complete and finitely complete $\infty$-categories and right exact functors;
• $\mathrm{Pr}^R_\omega$ is the $\infty$-category of presentable compactly generated $\infty$-categories and $\omega$-accessible right adjoint functors ($\omega$-accessible just means that the functor preserve cofiltered limits).

I'm going to factor this functor as the composition of functors that HTT proves to be equivalences. We can write it as $$ (\mathrm{Cat}_\infty^{lex,\natural})^{op}\xrightarrow{(-)^{op}}(\mathrm{Cat}_\infty^{rex,\natural})^{op}\xrightarrow{Ind(-)}(\mathrm{Pr}^L_\omega)^{op}\cong \mathrm{Pr}^R_\omega$$

Note that by HTT.5.3.5.4, $\mathrm{Ind}(C)=\mathrm{Fun}^{lex}(C^{op},\mathrm{Space})$, so this composition is exactly the functor we wanted to study.

Now let us check that all functors in this diagram are equivalences:

• The first functor simply sends an idempotent complete, finitely complete ∞-category to its opposite, which is an idempotent complete and finitely cocomplete ∞-category.
• The second functor is the (inverse of the) equivalence of HTT.5.5.7.8 for $\kappa=\omega$
• The third functor is just the equivalence of HTT.5.5.3.4 that sends every presentable ∞-category to itself and every functor to its right adjoint (in fact it is the restriction of this to the subcategory of compactly generated ∞-categories and $\omega$-accessible functors).

Finally, I'd like to remark that the first and third functors are also evidently an equivalence of $(\infty,2)$-categories (once you precisely defined what you mean by $op$). I believe the second functor is too, once you have stared carefully at HTT.5.3.5.10, but that would require a little bit of attention.