ScalingStacks

Proof. To begin, consider the case $Y=\Spec k$, so $X_{1}\times_{Y}X_{2}=X_{1}\times X_{2}$. By Proposition 4.6 and the fact that $\operatorname{Ind}:{st}\to\mathcal{P}r^{\rm L}$ is symmetric monoidal, the external product functor provides an equivalence $\boxtimes:\qc(X_{1})\otimes\qc(X_{2})\stackrel{{\scriptstyle\sim}}{{\rightarrow}}\qc(X_{1}\times X_{2})$.

To begin the case of a general perfect stack $Y$, consider the augmented cosimplicial diagram

with the obvious maps constructed from the given maps $p_{1},p_{2}$.

Applying the (contravariant) functor $\qc$, we obtain an augmented simplicial $\infty$-category

with structure maps given by pullbacks. By the absolute case of the theorem when $Y=\Spec k$, if we forget the augmentation, we obtain the simplicial $\infty$-category with simplices

$$\qc(X_{1})\otimes\qc(Y)\otimes\cdots\otimes\qc(Y)\otimes\qc(X_{2})$$

and structure maps given by tensor contractions. This is precisely the two-sided bar construction [L4, 4.5] whose geometric realization, by definition [L5, 5], calculates the tensor product of $\qc(Y)$-modules $\qc(X_{1})\otimes_{\qc(Y)}\qc(X_{2})$. Furthermore, the augmentation provides the natural map

which we will prove is an equivalence.

The above geometric realization is a colimit in $\mathcal{P}r^{\rm L}$, and hence (as observed prior to the statement of the theorem) may be evaluated as a limit in the opposite category $\mathcal{P}r^{\rm R}$. Thus we find that $\qc(X_{1})\otimes_{\qc(Y)}\qc(X_{2})$ is also the totalization of the cosimplicial $\infty$-category

with structure maps given by pushforwards. (We note for future reference that these structure maps are pushforwards along affine morphisms, hence are also colimit preserving, i.e., left adjoints.)

In particular, pushforward along the augmentation provides a natural functor

which is an equivalence if and only if $\tilde{\pi}^{*}$ is an equivalence.

To summarize some of the above structure, we have a diagram of commuting left (lower arrows) and right (upper arrows) adjoints

where $\tau_{*}$ is the universal map from the totalization to the zero cosimplices, and likewise, $\tau^{*}$ is the universal map from the zero simplices to the geometric realization. Thus we obtain a map of monads

acting on $\qc(X_{1}\times X_{2})$.

The geometric pushforward $\pi_{*}$ is conservative and preserves colimits since $\pi$ is affine. Hence by the Barr-Beck theorem, we have a canonical equivalence

$$\qc(X_{1}\times_{Y}X_{2})\simeq\Mod_{T_{geom}}(\qc(X_{1}\times X_{2})).$$

We also claim that the universal map $\tau_{*}$ is conservative and preserves colimits. For the first assertion, recall that $\tau_{*}$ is nothing more than the forgetful map from the totalization to the zero cosimplices. Since the $\infty$-categories involved are all stable, evaluating conservatism of a functor is equivalent to determining if nonzero objects are sent to zero. But an object sent to zero in the zeroth cosimplices is sent to zero in all cosimplices, and hence is equivalent to the zero object in the limit $\infty$-category.

To see $\tau_{*}$ preserves colimits, recall that the structure maps of our cosimplicial diagram are both right and left adjoints. It then follows (as observed prior to the statement of the theorem) that the totalization may be evaluated equivalently back in the category $\mathcal{P}r^{\rm L}$. In particular, the universal functor $\tau_{*}$ is a morphism in $\mathcal{P}r^{\rm L}$, and hence a left adjoint and so preserves colimits.

We may now apply the Barr-Beck theorem, giving a canonical equivalence

$$\qc(X_{1})\otimes_{\qc(Y)}\qc(X_{2})\simeq\Mod_{T_{alg}}(\qc(X_{1}\times X_{2})).$$

Thus it remains to show that the above morphism of monads is an equivalence. It is a straightforward diagram chase to check that the monad $T_{alg}=\tau_{*}\tau^{*}$ is nothing more than the composition $\pi_{1}^{*}\pi_{0*}$ of the geometric functors associated to the initial cosimplicial maps

Thus by base change, it is equivalent to the monad $T_{geom}=\pi_{*}\pi^{*}$. This concludes the proof of the theorem. ∎