If adjunction arises everywhere, where is it in the fundamental theorems?
MacLane's slogan "adjunction arises everywhere" is widely known, and adjunction has been identified as a key concept (maybe the key concept?) in category theory, eg, in the books by Goldblatt Topoi, Awodey Category Theory, and others:
The notion of adjoint functor applies everything that we’ve learned up to now to unify and subsume all the different universal mapping properties that we have encountered, from free groups to limits to exponentials. But more importantly, it also captures an important mathematical phenomenon that is invisible without the lens of category theory. Indeed, I will make the admittedly provocative claim that adjointness is a concept of fundamental logical and mathematical importance that is not captured elsewhere in mathematics. -- David Ellerman (quoting Awodey) "Adjoints and emergence: applications of a new theory of adjoint functors" Axiomathes 2007
If adjunction, arises everywhere shouldn't we see more examples across the spectrum of maths?
For the most part, it seems the example of natural isomorphism that is most widely quoted is that between the category of vector spaces, and its double dual, as discussed here.
Even a recent book like Roman's Lattices and Ordered Sets only gives 3 examples, including the one above.
The discussion in reply to the question "A bestiary about adjunctions" asked in Math.SSE a year ago primarily revolves around algebraic structures.
Similarly, much of the research seems to be very abstract and algebraic in nature.
But where is application of adjunction and universal mapping property in any of the fundamental theorems or their generalizations (eg, f.t. algebra --> Bezout's theorem). Here is a short list of fundamental theorems in Wikipedia. Or perhaps it's possible in principle but it would take a lot of effort to identify the categories, functors and related constructions (transposition, unit, counit?).
EDIT
Here by the way is a historical timeline - implemented in Mathematica - of advances in adjunctions, motivated by Qiaochu Yuan's choice of Galois theory to address this question:
My own experience is that adjunction is a way to characterize certain constructions. Often these constructions then appear in theorems, which state properties of them.
E.g. if $f: X \to Y$ is a morphism of varieties, or complex analytic spaces, then the pushforward $f_*$ on sheaves can be characterized as the adjoint to the pullback $f^*$, the latter being in some sense the more intuitive of the two functors. (It is defined so that the stalk of $f^*\mathcal F$ at $x \in X$ is canonically identified with the stalk $\mathcal F_{f(x)}$ of $\mathcal F$ at $f(x)$.) Some of the key theorems in algebraic and analytic geometry are then about $f_*$. (E.g. if $f$ is proper than $f_*$ preserves coherence; the decomposition theorem in the theory of perverse sheaves; ... .)
E.g. in representation theory, induction (in the sense of induced representation, where we induced a representation from a subgroup $H$ to a larger group $G$) can be defined as an adjoint of restriction (from $G$-reps. to $H$-reps.), and there are many theorems in various contexts about the properties of induced representations.
E.g. tensor product is defined by an adjoint property, and there many theorems about tensor products in various contexts.
Describing a certain construction as an adjoint functor normally provides evidence that it is important, and suggests various ways to think about it. But that is often the beginning of the story, not the end ... .
That list includes the fundamental theorem of Galois theory, which happens to be a great example of an adjunction! Galois theory is all about the adjunction
$$F : M \mapsto \text{Gal}(L/M)$$ $$G : H \mapsto L^H$$
between subsets of a Galois extension $L/k$ and subsets of the Galois group $G = \text{Gal}(L/k)$. (The corresponding categories here are posets.) There is a general theorem to the effect that an adjoint pair of functors canonically determines an equivalence between certain subcategories, and the fundamental theorem of Galois theory) in effect identifies these subcategories, namely subextensions and subgroups, and it also identifies a second equivalence, namely normal subextensions and normal subgroups.
A formally similar example is the adjunction
$$F : I \mapsto \{ x \in \mathbb{A}^n : f(x) = 0 \forall f \in I \}$$ $$G : V \mapsto \{ f \in k[x_1, ... x_n] : f(x) = 0 \forall x \in V \}$$
between subsets of $k[x_1, ... x_n]$ and subsets of affine space $\mathbb{A}^n$ (where $k$ is an algebraically closed field). The fundamental theorem in this context (namely the Nullstellensatz) again identifies the equivalent subcategories, namely radical ideals and algebraic subvarieties, and it also identifies a second equivalence, namely prime ideals and irreducible subvarieties.
Paraphrasing Lawvere a bit, semantics and syntax are adjoint on the right. Let's recall some definitions. Assume two strongly inaccessible cardinals – though probably one is enough.
Let $\textbf{FinCard}$ be the category of finite cardinals ($0, 1, 2, \ldots$) and all maps between them. (So $\textbf{FinCard}$ is a small skeleton of the category of finite sets.) A Lawvere theory is a small category $\mathbb{T}$ equipped with a bijective-on-objects functor $\textbf{FinCard} \to \mathbb{T}$ that preserves all finite coproducts. The category of Lawvere theories is the full subcategory $\mathcal{T}$ of the coslice category $(\{ \textbf{FinCard} \} \downarrow \textbf{Cat})$ spanned by Lawvere theories.
An algebra of type $\mathbb{T}$ is a product-preserving functor $\mathbb{T}^\textrm{op} \to \textbf{Set}$. A homomorphism of algebras of type $\mathbb{T}$ is a natural transformation of such functors. Write $\textbf{Mod}(\mathbb{T})$ for the (concrete) category of models of $\mathbb{T}$.
Theorem (Lawvere). Let $\textbf{CAT}$ be the category of locally small categories, and let $\mathcal{K}$ be the full subcategory of the slice category $(\textbf{CAT} \downarrow \{ \textbf{Set} \})$ spanned by those functors $U : \mathcal{C} \to \textbf{Set}$ such that the class of natural transformations $U(-)^n \Rightarrow U(-)$ is small for every natural number $n$. Then, $\textbf{Mod}(-)$ is a functor $\mathcal{T}^\textrm{op} \to \mathcal{K}$, and it has a right adjoint $\textbf{Th}(-) : \mathcal{K}^\textrm{op} \to \mathcal{T}$, which is defined as follows: for a given object $U : \mathcal{C} \to \textbf{Set}$ in $\mathcal{K}$, $\textbf{Th}(U)$ is the opposite of the full subcategory spanned by the image of the unique product-preserving functor $\textbf{FinCard}^\textrm{op} \to [\mathcal{C}, \textbf{Set}]$ given by $1 \mapsto U$. Here, by adjointness we mean there is a bijection $$\mathcal{K}(U, \textbf{Mod}(\mathbb{T})) \cong \mathcal{T}(\mathbb{T}, \textbf{Th}(U))$$ that is natural in $U$ and $\mathbb{T}$.
In a sense, this is a categorification of the folklore Galois correspondence between truth and provability in logic. There's another result along this vein in topos theory, namely Diaconescu's theorem. It is perhaps the closest thing to a fundamental theorem in the subject, and I will now state a special case:
Theorem (Diaconescu). Let $\mathbb{A}$ be a small category with finite limits, and let $\mathcal{E}$ be a locally small and cocomplete topos. Let $\hat{\mathbb{A}}$ be the presheaf topos $[\mathbb{A}^\textrm{op}, \textbf{Set}]$, and let $y : \mathbb{A} \to \hat{\mathbb{A}}$ be the Yoneda embedding.
For each left exact functor $F : \mathbb{A} \to \mathcal{E}$, there is a unique left exact functor $F^* : \hat{\mathbb{A}} \to \mathcal{E}$ such that $F^* y \cong F$, and $F^*$ is the left adjoint to the functor $F_* : \mathcal{E} \to \hat{\mathbb{A}}$ defined by $F_* E = \mathcal{E} (F(-), E)$.
This extends to an equivalence between the category of left exact functors $\mathbb{A} \to \mathcal{E}$ and the category of left exact left adjoint functors $\hat{\mathbb{A}} \to \mathcal{E}$, and this equivalence is pseudonatural in $\mathbb{A}$ and $\mathcal{E}$. (Here $\mathbb{A}$ is regarded as an object in the category of small finitely-complete categories and left exact functors.)
Why is this important? Because it tells us that every presheaf topos $\hat{\mathbb{A}}$ is a classifying topos for the geometric theory of left exact functors $\mathbb{A} \to \textbf{Set}$. This sounds very abstract, but in fact Lawvere already more-or-less showed that all finitary algebraic theories are of this form. To be precise, if $\mathbb{T}$ is a finitary algebraic theory and $\mathbb{A}$ is the opposite of the category of finitely-presented models of $\mathbb{T}$ in $\textbf{Set}$, then the category of left exact functors $\mathbb{A} \to \textbf{Set}$ is equivalent to the category of (not necessarily finitely-presented) $\mathbb{T}$-models in $\textbf{Set}$. We think of $\mathbb{A}$ as the syntactic category of $\mathbb{T}$: its objects can be regarded as certain well-formed formulae in the language of $\mathbb{T}$, whose interpretation in a model of $\mathbb{T}$ is given by the left exact functor $\mathbb{A} \to \textbf{Set}$ that represents the model.
Continuing Matt E's remarks: I would claim that we can see adjunctions in many fundamental properties... which are often the reason an object is introduced in the first place, that is, to achieve a certain desired effect.
Thus, "Frobenius Reciprocity" about induced representations of groups is really the _defining_property_ (or "characterization") of induced representations (not worry about the left/right issue for the moment). Thus, by now, if perhaps not in Frobenius' time, what was once the theorem becomes the definition, and what was once the definition becomes a construction to prove existence.
I hasten to point out, or claim, that very little "formal" category theory is required in order to see adjunction relations. That is, a very small category-theory vocabulary suffices.
Without quite formalizing things as categories and functors, we can give less-common examples: (integration against) Eisenstein series is a kind of adjoint to taking Mellin transform of constant term of automorphic forms. (Integration against) pseudo-Eisenstein series is adjoint to (integration of) constant term against test functions in $y=\Im z$, on the upper half-plane, for example.
Left or right exactness of nice functors is most sanely proven by observing that the functors are right or left adjoints. Many of the functors of sheaf theory (whether on ordinary topological spaces or something fancier) fit into adjoint pairs: global sections functor and constant sheaf functor, sheafification and inclusion of sheaves to presheaf, etc.
Formation of universal enveloping algebra of a Lie algebra is (left) adjoint to the slightly forgetful functor that creates a Lie algebra from an associative algebra by $[x,y]=xy-yx$.
Often adjoints to forgetful functors are important: formation of polynomial rings is left adjoint to the forgetful functor that converts a ring to a set. Formation of free groups similarly. Extension of scalars on a vector space or module is adjoint to forgetting scalars only to the smaller field (or ring).
I anticipate other people will have more things to say! :)