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.
