Hardcore math tweet:

The "projection formula" or "Frobenius law" shows up in many branches of math, from logic to group representation theory to the study of sheaves.

Let's see what it means in an example!

(1/n)

Given any group homomorphism f: G → H you can "restrict" representations of H along f and get representations of G.

But you can also take reps of G and freely turn them into reps of H: this is "induction".

Induction is the left adjoint of restriction.

(2/n)

You can get a lot of stuff just knowing that induction is the left adjoint of restriction: this is called "Frobenius reciprocity".

But you can also take tensor products of representations, and then a new fact shows up: the projection formula!

(3/n)

Where does this mysterious fact come from? It comes from the fact that the category of representations of a group is a symmetric monoidal *closed* category, and restriction preserves not only the tensor product of representations, but also the internal hom!

(4/n)

You get the projection formula whenever you have adjoint functors between symmetric monoidal closed categories and the right adjoint is symmetric monoidal and also preserves the internal hom! The 6-line proof uses the Yoneda lemma:

https://ncatlab.org/nlab/show/Frobenius+reciprocity#InWirthmuellerContexts

(5/n)

This may not help you much unless you know some category theory and/or you've wrestled with the projection formula and wondered where it comes from. But to me it's a tremendous relief. I thank Todd Trimble for getting to the bottom of this and explaining it to me.

(6/n, n=6)