Adjoint Functor Theorem The Freyd's Adjoint Theorem states that given a complete locally small category $\mathcal{C}$, a continuous functor $G: \mathcal{C} \to \mathcal{D}$ has a left adjoint if and only if it satisfies a certain condition (which is called a Solution Set Condition in Maclane's book), which is equivalent, under our assumptions, to say that for each $X \in \mathcal{D}$ the category $(X \downarrow G)$ has an initial object.
This theorem seems to be central in classical Category Theory, since it allow us to show the existence of a left adjoint for $G$ by checking the given Solution Set Condition. 
However, this condition seems to be difficult to check, except in some easy cases. 
Question 1. Is there any fundamental result in which Freyd's Adjoint Theorem plays a crucial role to show the existence of a left adjoint?
Question 2. It is frequently asked (in Maclane's book) to construct a left adjoint functor in some special cases, using Freyd's Adjoint Theorem. However, except these special cases, I do not see how this result allows the explicit construction a left adjoint.
 A: It is trivial that $G : C \to D$ admits a left adjoint iff for every $X \in D$ the category $(X \downarrow G)$ has an initial object (namely, $X \to G(F(X))$ is an initial object iff $\hom(X,G(-))$ is represented by $F(X)$). However, if $C$ is complete and $G$ is continuous, then $(X \downarrow G)$ is also complete and we may use Freyd's criterion for the existence of an initial object:

If $C$ is a complete category such that there is a set of objects $S$ which is "weakly initial" i.e. such that every object of $C$ admits a morphism from some object in $S$, then $C$ has an initial object.

The proof is direct and constructive (but not very useful in applications). First, we consider the product $p$ of all objects in $S$. This admits a morphism to any object of $C$. In order to enforce uniqueness, we have to make $p$ smaller: One considers the equalizer $e$ of all endomorphisms of $p$. Then one easily checks that $e$ is an initial object of $C$.
From this we derive Freyd's adjoint functor theorem: If $C$ is complete and $G : C \to D$ is a continuous functor such that for every $X \in D$ the category $(X \downarrow G)$ has a weakly initial set (often called solution set), then $G$ admits a left adjoint.
The existence of a solution set is often easy to verify. Freyd's adjoint functor theorem has lots of applications (existence of tensor products, Stone-Cech compactifications, existence of free algebras of any type such as free groups, free rings, tensor algebras, symmetric algebras etc., but also of colimits of algebras of any type). I think that in any of these applications we can also give a more direct proof, but usually this proof requires more calculations. Freyd's adjoint theorem allows us to unify all these examples. I think this is one of the main purposes of category theory: unification. And this leads to simplification. But I don't know if there are any results which really depend on Freyd's adjoint functor theorem (i.e. there are no proofs without it).
Notice: In Freyd's criterion for the existence of an initial object, and hence for the existence of a left adjoint, we may obviously replace "set" by "essentially small class" (which means that there is a set such that every object of the class is isomorphic to an object in this set).
Now let us look at some specific example. The forgetful functor $U : \mathsf{Grp} \to \mathsf{Set}$ has a left adjoint. First of all, $U$ creates limits. If $X$ is a set, a solution set for $X \downarrow U$ consists of all maps $i : X \to U(G)$ where $G$ is generated by the image of $i$. The class of these groups is essentially small, since $U(G)$ admits a surjection from $\coprod_n (X \times \mathbb{N})^n$, namely $((x_1,e_1),\dotsc,(x_n,e_n)) \mapsto x_1^{e_1} \dotsc x_n^{e_n}$. If $G$ is any group and $X \to U(G)$ is a map, then we may consider the subgroup $G'$ which is generated by the image, so that $X \to U(G)$ factors through $U(G')$. Thus we have a solution set, and  $U$ has a left adjoint $F : \mathsf{Set} \to \mathsf{Grp}$ (free groups).
We can use the proof of Freyd's adjoint functor theorem to write it down "explicitly". Let $$P = \prod_{\substack{i : X \to U(G) \\ i \text{ generates } G}} G$$ with the obvious map $X \to U(P)$ and let $X \to F(X)$ be the equalizer of all endomorphisms of $(X \to U(P),P)$. Then $F(X)$ is the free group on $X$. Alternatively, we may define $F(X)$ (this is what Lang does in his Algebra book!) as the subgroup of $P$ which is generated by the image of $X \to U(P)$ - this gives uniqueness in the universal propert of $F(X)$, remember that this was the only purpose of taking the big equalizer. This abstract construction is usually not considered to be explicit (although it is explicit), because it doesn't tell us what the elements of $F(X)$ are (because it is still a widespread belief that elements describe a mathematical object). The element structure of $F(X)$ can be derived from the universal property, using an action of $F(X)$ on the set of reduced words (see Serre's book Trees).
