Formal category theory in augmented virtual double categories

Abstract

In this article we develop formal category theory within augmented virtual double categories. Notably we formalise the classical notions of Kan extension, Yoneda embedding ${\text{y}}_A:A\to \hat{A}$, exact square, total category and 'small' cocompletion; the latter in an appropriate sense. Throughout we compare our formalisations to their corresponding $2$-categorical counterparts. Our approach has several advantages. For instance, the structure of augmented virtual double categories naturally allows us to isolate conditions that ensure small cocompleteness of formal presheaf objects $\hat{A}$. Given a monoidal augmented virtual double category $\mathcal{K}$ with a Yoneda embedding ${\text{y}}_I:I\to \hat{I}$ for its monoidal unit $I$ we prove that, for any 'unital' object $A$ in $\mathcal{K}$ that has a 'horizontal dual' $A^{\circ }$, the Yoneda embedding ${\text{y}}_A:A\to \hat{A}$ exists if and only if the 'inner hom' $[A^{\circ },\hat{I}]$ exists. This result is a special case of a more general result that, given a functor $F:\mathcal{K}\to \mathcal{L}$ of augmented virtual double categories, allows a Yoneda embedding in $\mathcal{L}$ to be "lifted", along a pair of 'universal morphisms' in $\mathcal{L}$, to a Yoneda embedding in $\mathcal{K}$.

arXiv comment126 pages. Comprises a streamlined and much expanded version of Sections 4 and 5 of the draft paper arXiv:1511.04070. v3: Section 5 moved to the end and Proposition 4.26 added. Several other small changes. Major changes in numbering. Final version as published in TAC. v2: many small improvements and small corrections