We are interested in -modules for a Lie group . The famous Beilinson-Bernstein localization theorem states it is equivalent to -modules on the flag variety .
A great reference is this survey by Gurbir Dhillon and its associated lecture series.
We want to upgrade the Beilinson-Bernstein localization theorem to something concerning Harish-Chandra modules on which another subgroup acts. Note that this just means the action of is integrable, so it is a property rather than an extra structure. An important example is the Verma module which is a -module (since acts by weight-raising operators).
For Beilinson-Bernstein in the case , see this note. For more examples and illustration, I strongly recommend the note by Anna Romanov.
For why B-B localization exchanges -equivariant -modules with -module, see 3.3.21-3.3.23 of the survey. For the localization functor , the point is that the induced action of on is by (the derivative of conjugation), the reason being that a differential operator can be seen as , so , and this is not the action of on itself by left multiplication. Tensoring by a -module fixes this problem.
The idea is that there should be more structures underlying the B-B equivalence. For starters, note that acts on both categories -mod (induced by adjoint action of on ) and , and so the equivalence should be that of -modules. But this observation only uses that viewed as an abstract group. We get more structrure by equipping both sides by action of , the categorification of the group algebra under the function-sheaf correspondence.
Note that while the discussion of the automorphisms and worked equally well with abelian or derived categories, for this monoidal structure to behave in the desired way, i.e., to even have a reasonable -module pushforward, it is essential we work with derived categories. So far, the corresponding triangulated category is enough, but we will be forced to ask for more.
The idea is that the intertwining of Harish-Chandra modules with equivariant -modules should follow from taking categorical invariants of both sides of the B-B equivalence. Taking invariant amounts to look at Hom from the trivial categorical representation, so the next goal is to realize the intertwiners where are categorical representations of also as a triangulated category. The problem is that the cone construction is not functorial. For example, given triangulated functors equipped with a morphism , it is not clear how to complete it to an exact triangle.
The basic idea of dg-categories is to remember not only the cohomology of these complexes but also all the complexes themselves, up to simultaneous quasi-isomorphism. The reader familiar with derived categories should not find this maneuver so surprising. After all, derived categories arise from the usefulness of remembering not only individual derived functors, but also the complex computing them. Passing from triangulated to dg-categories simply repeats this idea not only for objects, but also for morphisms.
Under this formalism, we have . Similarly for .
The proof of B-B breaks up into three parts by Beck’s monadicity theorem. See Gannon’s note. The fist statement is proving the derived localization functor is -exact, i.e. is exact. The argument presented in Gannon’s note is essentially due to Frenkel & Gaitsgory. Then we need to show is conservative, i.e. if a -module , then its global section . This also amounts to showing the localization functor is essentially surjective. For this, the idea is that the coherent sheaves for dominant integral and a fixed generates the derived categories in the sense that their right orthogonal is zero (this is essentially Borel-Weil-Bott). Hence hence the objects (or, in fact, a finite subset of this set) generate the derived category of -modules. Thus it suffices to show lies in the image of . The key is that by considering the action of Casimir on (where is highest weight representation of weight ) we see that is a summand of , hence lies in the image of .
The Springer map is a semiclassical shadow of Beilinson-Bernstein, and various properties of the Springer map (birational, proper, symplectic resolution of rational singularities) translates into the Beilinson-Bernstein equivalence. See here for an explanation. The reason why the categorical representation framework is useful is explained in this paper by Ben-zvi and Nadler.
Reference: Roman’s note