# Proof in the realm of $\infty$ categories

I have recently started learning the language of $$\infty$$-categories. My approach is more to their use, rather than for their own sake. For this reason, as I feel I reached a good understanding of the basic notions (the definition, functors, adjoints, stable categories, etc.), I have now turned my attention to some papers which work in the framework of stable $$\infty$$-categories to solve the functoriality issues we encounter when we work with triangulated categories. However, I am having problems understanding what can be proved and what can't using techniques similar to the triangulated world. For example, I am reading Noncommutative homological projective duality by Alexander Perry (arXiv:1804.00132), and in the first part some results about $$S$$-linear categories (where $$S$$ is a scheme satisfying some assumptions) are proved. The formal definition is that the categories of $$S$$-linear categories is the categories of module objects $$\text{Mod}_{\mathfrak{Perf}(S)}(\text{Cat}_{\text{st}})$$, where $$\text{Cat}_{\text{st}}$$ is the $$\infty$$-category of stable, idempotent complete $$\infty$$-categories with exact functors. The author then wants to prove that if we have an $$S$$-linear functor $$\phi : \mathcal{C} \rightarrow \mathcal{D}$$ between $$S$$-linear categories which has a left adjoint when considered as a plain functor of $$\infty$$-categories, then $$\phi^{L}$$ is automatically an $$S$$-linear functor. The proof which is given in the paper uses the internal hom for $$S$$-linear categories, and the adjunction properties $$\mathcal{H}om_{S}(\phi^L(C \otimes F), D) \simeq \mathcal{H}om_{S}(C \otimes F, \phi(D)) \simeq \mathcal{H}om_S(C, \phi(D) \otimes F^{\vee}) \simeq \dots \mathcal{H}om_S(\phi^{L}(C) \otimes F,D)$$ where $$C \in \mathcal{C}, D \in \mathcal{D}, F \in \mathfrak{Perf}(S)$$, and $$\otimes$$ denotes the module structure. Then the proof is concluded using the Yoneda lemma. This is the proof I would write if I were working in the triangulated setting, and I don't understand why one is allowed to use it in the $$\infty$$-categorical framework as well. Adjunction in this case as far more tricky (even if they imply the obvious isomorphism on mapping spaces), and the structure of $$S$$-linear functor implies $$\phi^L(C \otimes F) \simeq \phi^L(C) \otimes F$$ up to contractible choices, but it is not equivalent to this isomorphism, is it? It would be very helpful is some could help me understanding to which point one can transport proofs from the triangulated world to the stable $$\infty$$-categorical framework. Thanks.

• That proof doesn't give the full details, but it doesn't do so in the 1-categorical world either: being S-linear is additional structure on a functor, not just a property. However, for the left adjoint of an S-linear functor you have canonical oplax structure maps $\phi^L(C \otimes F) \rightarrow \phi^L(C) \otimes F$ (adjoint to the map $C \otimes F \rightarrow \phi\phi^L(C) \otimes F \simeq \phi(\phi^L(C) \otimes F)$ defined by the unit of the adjunction and the linearity of $\phi$). So what you're really showing is that this particular map is an equivalence. – Rune Haugseng Jul 14 '20 at 9:28
• The same is true in the $\infty$-categorical setting, it's just a bit trickier to set up the oplax structure maps in a coherent way. In this particular case (and many others) this is best dealt with using cocartesian fibrations (for the details see Corollary 7.3.2.12 in Higher Algebra). – Rune Haugseng Jul 14 '20 at 9:37
• This illustrates a common feature of working with $\infty$-categories: if you're checking a property you can often reason just as in the 1-categorical setting, but to obtain structures you usually have to figure out a canonical reason why they exist (though this can often give cleaner proofs for 1-categories too than you get by writing them out explicitly). – Rune Haugseng Jul 14 '20 at 9:41
• @Federico I would say the thing that is generally swept under the rug is why two maps are the same. i.e. you claim that a map is an isomorphism because its a map between isomorphic objects. This problem clearly appears in the proof you presented, and it is the same to infinity categories as to 1-categories. It is just culturally excepted to ignore it in 1-categorical settings for basically no good reason. Once you note it, the difference between the theories become much smaller in practice I believe. – S. carmeli Jul 14 '20 at 14:04
• As illustrated in this discussion, the details are often clear to experts. But as $\infty$-categorical methods are (for good reason) adopted by a greater number of non-experts, I (as a novice) worry when these issues are brushed under the rug. – Phil Tosteson Jul 14 '20 at 14:52