Understanding the purely formal part of the sheaf theoretic (cohomological) framework for representation theory By now I have the impression that many statements in representation theory can be phrased a lot more elegantly using cohomological language. Therefore I'm trying to understand a bit better the sheaf theoretic framework for representation theory. To be specific I'd like to understand, for example, the purely formal parts (no hard "real" theorems) of the following ideas:


*

*Induction and Coinduction as different pushforwards of sheaves

*Equivariant sheaves as sheaves on quotient stacks and relation to the (Co-)induction functors.
I have some background in algebraic geometry and homological algebra (i'm even fine with some moderate stacky language) so I think I have the nessasary tools to understand this yet unfortunately I'm having a hard time finding references for statements appearing, for example, in the answers to the following question.
Is there a source that tells the overall cohomological story of representation theory with some sketches of proofs for the obviously formal propositions? (for example that thing with induction and pushforward which looks entirely formal to me).
 A: Let $G$ be an affine group scheme (e.g. a finite group). There is a stack $BG$ which is more or less determined by either of the following two properties: 


*

*Maps to $BG$ are the same thing as $G$-torsors. More formally, there's a functor from commutative rings to groupoids sending a commutative ring $R$ to the groupoid of isomorphism classes of $G$-torsors over $\text{Spec } R$; this functor is represented by a stack called $BG$.

*Quasicoherent sheaves on $BG$ are the same thing as representations of $G$. 
If $f : H \to G$ is a map of affine group schemes, it induces a map $Bf : BH \to BG$ of stacks, which further induces a pullback functor $Bf^{\ast} : QC(BG)) \to QC(BH)$; as you might imagine, this is restriction of representations. Pullback has, as usual, a right adjoint, namely pushforward $Bf_{\ast} : QC(BH) \to QC(BG)$; this is one version of induction of representations (I guess it might be "coinduction," but I'm happy to just call it "induction" because this adjoint will, I think, always exist, so it ought to have the more fundamental name). 
To get a better sense of what pushforward is doing, you can think of $BG$ as being the quotient stack $\text{pt}/G$, and $BH$ as being the quotient stack $(G/H)/G$; then you can think of representations of $G$ as $G$-equivariant sheaves on a point, and representations of $H$ as $G$-equivariant sheaves on $G/H$. This lets you interpret push/pull along the map $BH \to BG$ as $G$-equivariant push/pull along $G/H \to \text{pt}$.
In the nicest examples, where $G$ is reductive and $H$ is the Borel subgroup, $G/H$ will be a smooth projective variety (the flag variety of $G$); the significance of this is that $G$-equivariant pushforward from $G/H$ to a point (that is, taking global sections) now sends finite-dimensional representations of $H$ to finite-dimensional representations of $G$. What representations you get is described by the Borel-Weil-Bott theorem, and for the nicest statements you should take the derived pushforward. 
It's unclear to me what part of this story is "purely formal." You can write down adjoints all day, but this feature that sometimes induction sends finite-dimensional things to finite-dimensional things even though $H$ isn't finite index in $G$ doesn't seem formal to me. Also, I don't know a reference for any of this. 
