Geometric representation-theoretic equivalence from formality

Assume the Formality Conjecture, and let $\widecheck{G}/B_q$ be the half-quantum flag variety. Let $\widetilde{\mathcal{N}}$ be the Springer resolution, let $\operatorname{QCoh}_{\mathrm{dg}}$ denote dg quasi-coherent sheaves, and let $\operatorname{DG}(\operatorname{FK}{G}_q)_0$ denote the principal block of coherent dg sheaves for the small quantum group. Consider the pushforward functor

$$\xi_*:=\mathscr{R\!H}om_{\widecheck{G}/B_q}(\1,-):\operatorname{QCoh}_{\mathrm{dg}}(\widecheck{G}/B_q)\to \operatorname{QCoh}_{\mathrm{dg}}(\widetilde{\mathcal{N}}).$$

Formality-implies-equivalence conjecture. If the Formality Conjecture holds, then this non-monoidal pushforward restricts, via the Kempf embedding, to an equivalence

$$\xi_*|_{\operatorname{block}_0}:\operatorname{DG}(\operatorname{FK}{G}_q)_0\overset{\sim}\longrightarrow \operatorname{Coh}_{\mathrm{dg}}(\widetilde{\mathcal{N}}),$$

and this equivalence can be identified with the equivalences of Arkhipov–Bezrukavnikov–Ginzburg and Bezrukavnikov–Lachowska.

This is a conditional geometric realization of the principal block of small quantum-group representations. Its truth is presented as depending on the preceding formality conjecture, and the source gives no unconditional resolution.