@asv it’s an easy exercise to check that the right adjoint of a symmetric monoidal functor is lax symmetric monoidal

@Gabriel I believe this is indeed true, and the same proof works. Essentially, since the category of holonomic D-modules is Artinian, we can reduce to the case where the base is smooth and the sheaf is a connection. Then check that the adjunction map is an iso on fibers using Poincare duality; the fact that the connection might have irregular singularities is immaterial. Thanks for the contact info, I will send a message when I have a chance

Isn’t it also possible to define a sheaf theory a la Gaitsgory-Rozenblyum which sends an affine scheme to its (Ind) category of holonomic D-modules? Unfortunately I don’t know how to define the latter on singular schemes without using embeddings into smooth schemes

Twisted D-modules make sense on any space equipped with a torus bundle (see the accepted answer from this question). To twist D-modules on Bruhat cells just pull $G/N \to G/B$ back along the inclusion. To compute for $SL_2$, in principle you just need a concrete model of the line bundle as well as trivializations over both cells

One can think of twisted D-modules as D-modules on the $T$-bundle $G/N \to G/B$ with fixed monodromy on each fiber. Since the Bruhat cells are affine, every $T$-bundle over them trivializes, so one can think of pushforward as going from ordinary D-modules to twisted ones. Obviously, this depends on a trivialization for each cell, so I'm not sure that's the right way to think about it

@user837898 an equivalence of stacks is an equivalence of categories which preserves Cartesian arrows, if you want to take the Cartesian fibration approach. If you want to take the functorial approach then an equivalence of stacks is a natural isomorphism of functors. Notice this notion of equivalence has nothing to do with descent; after all, the category of stacks is fully faithfully embedded in the category of prestacks

Smoothness is fpqc local on the base

Nice, thanks! I believe this should also encompass the example of $\varphi$ being a coCartesian fibration as I wrote in the comments

@ZhenLin Unless I'm mistaken, I think the result follows for $\varphi$ a coCartesian fibration from Prop. 7.3.4.1 in Kerodon. I'm not sure if one can somehow reduce the general case to this one

@ZhenLin Great, thanks again for the clarification!

@ZhenLin Thanks a bunch! Any chance you have a reference for this? I'm also slightly confused because aren't pullback squares special cases of comma squares?

Isn't $JF=D_{\mathbb{P}^1} \otimes_{\mathcal{O}_{\mathbb{P}^1}} F$? What is the map $JF \to F$?

As @WillSawin points out, I think this is incorrect as stated. For example, how would one obtain a skyscraper D-module at a smooth point using this description?