Origin and context of adjunctions inducing equivalences between full subcategories

Question

The following is well-known.

Theorem. Let $F\dashv U$ be a pair of adjoint functors $$F\colon \mathcal C\to \mathcal D, \qquad U\colon \mathcal D\to\mathcal C$$ with unit $(\eta_A\colon A\to U(F(A)))_{A\in\mathcal C}$ und counit $(\varepsilon_B\colon F(U(B)) \to B)_{B\in\mathcal D}$. Then $F$ and $G$ restrict to equivalences $\mathcal C'\to\mathcal D'$ and $\mathcal D'\to\mathcal C'$ between the full subcategories $\mathcal C'$ and $\mathcal D'$ given by $$\mathcal C':=\{A\in\mathcal C\mid \eta_A\text{ is an isomorphism}\}$$ and $$\mathcal D':=\{B\in\mathcal D\mid \varepsilon_B\text{ is an isomorphism}\}.$$

Posets can be considered as categories. This yields:

Corollary. Let $P$ and $Q$ be posets, and $f\colon P\to Q$ and $u\colon Q\to P$ monotone maps with $$\forall a\in P.\, \forall b\in Q.\,a\leq u(b)\iff f(a)\leq b.$$ Then $f$ and $u$ restrict to isomorphisms between the induced sub-posets $P'$ and $Q'$ given by $$P':=\{a \in P\mid a = u(f(a))\}$$ and $$Q':=\{b\in Q\mid f(u(b))=b\}.$$

Questions.

1. Can someone give me the original references for the theorem and the corollary above? Of course, in some sense, the corollary must be hidden in the works of Galois (or in the works of people who cleaned up his theory), since taking $P$ to be $(\mathcal P(F), \subseteq)$ for any field $F$, $Q$ to be $(\mathcal P(G), \supseteq)$ for any group $G$ of automorphisms of $F$, and considering $$f\colon \mathcal P(F) \to \mathcal P(G),\, a\mapsto\{g\in G\mid \forall x\in a. \, g(x)=x\}$$ and $$u\colon \mathcal P(G) \to \mathcal P(F), \, b\mapsto \{x\in F\mid \forall g\in b. \, g(x)=x\}$$ yields the fundamental theorem of Galois theory up to a concrete characterization of $P'$ and $Q'$. But I'm interested in who extracted the "abstract content" of this proof in the sense of the corollary and who, after that, formulated the generalization to categories in the sense of the theorem.

2. Not just the relation "$g(x)=x$" between field elements $x$ in $F$ and automorphisms $g$ in $G$ yields a pair of functions $f\colon \mathcal P(F) \to \mathcal P(G)$ and $u\colon \mathcal P(G) \to \mathcal P(F)$ satisfying the conditions of the corollary, but in fact any relation $R\subseteq A\times B$ yields such a pair of functions $f\colon \mathcal P(A) \to \mathcal P(B)$ and $u\colon \mathcal P(B) \to \mathcal P(A)$. (Such a pair functions constituting an adjunction between posets is called a Galois connection, by the way.) Thus relations are a powerful tool to generate Galois connections. Is there an analogue of relations that allows one to generate pairs of adjoint functors between categories?

3. Not just the fundamental theorem of Galois theory can be formulated as an instance of the above theorem, but also the Gelfand–Naimark theorem, the Stone duality, the duality between affine schemes and commutative rings, and the Pontrjagin duality are corollaries of the above theorem up to concrete characterization of $\mathcal C'$ and $\mathcal D'$. I guess most of them are recast as applications of the above theorem only with hindsight. But can the above theorem be also used as a guide that helps and inspires proving completely new equivalences?

Answer 1

Question 1

I don't know if they are the first publications, but two very early references are

1. Garrett Birkhoff (1940). Lattice Theory.
2. Øystein Ore (1944). "Galois Connexions". (see Theorem 2 for a formulation of the "Corollary")

Remarks in these texts indicate that Galois connections between power set lattices $\mathcal P(X)$ and $\mathcal P(Y)$ induced by relations $R\subseteq X\times Y$ are due to Birkhoff, while Ore introduced the theory of Galois connections between arbitrary posets. From 2:

It has already been pointed out by Garrett Birkhoff that any binary relation defines a correspondence of the type of a Galois connexion between the subsets of two sets

In the 1948 revised edition of 1, Birkhoff remarks in a footnote that the "Corollary" in the special case of Galois connections induced by relations is due to himself, while he refers to 2 as the origin of a particular axiomatization of Galois connections between arbitrary posets that he gives in the text.

As remarked by Marc Olschok in the comments, the "Theorem" occurs implicitly in

3. Saunders Mac Lane. Categories for the Working Mathematician.

in the form of an exercise (Exercise 2, §IV-5). I don't have the first edition of that book to check whether this exercise already appears in the first edition. Given the similarity between adjunctions (due to Kan) and Galois connections, the generalization from the "Corollary" to the "Theorem" may well be a "folklore result", if not due to Mac Lane.