(Real) Frobenius Reciprocity

Now we come to the real version of Frobenius reciprocity. It takes the form of an adjunction between the functors of induction and restriction:

where is an -module and is a -module.

This is one of those items that everybody (for suitable values of “everybody”) knows to be true, but that nobody seems to have written down. I’ve been beating my head against it for days and finally figured out a way to make it work. Looking back, I’m not entirely certain I’ve ever actually proven it before.

So let’s start on the left with a linear map that intertwines the action of each subgroup element . We want to extend this to a linear map from to that intertwines the actions of all the elements of .

Okay, so we’ve defined . But if we choose a transversal for — like we did when we set up the induced matrices — then we can break down as the direct sum of a bunch of copies of :

So then when we take the tensor product we find

So we need to define a map from each of these summands to . But a vector in looks like for some . And thus a -intertwinor extending must be defined by .

So, is this really a -intertwinor? After all, we’ve really only used the fact that it commutes with the actions of the transversal elements . Any element of the induced representation can be written uniquely as

for some collection of . We need to check that .

Now, we know that left-multiplication by permutes the cosets of . That is, for some . Thus we calculate

and so, since commutes with and with each transversal element

Okay, so we’ve got a map that takes -module morphisms in to -module homomorphisms in . But is it an isomorphism? Well we can get go from back to by just looking at what does on the component

If we only consider the actions elements , they send this component back into itself, and by definition they commute with . That is, the restriction of to this component is an -intertwinor, and in fact it’s the same as the we started with.