Galois insertion

Summary

A Galois insertion is a Galois connection $(f, g)$ in which the lower adjoint undoes the upper adjoint: $f(g(y)) = y$ for every $y$. Then $g$ embeds $Q$ into $P$ as the set of closed elements of the closure operator $g \circ f$. Galois insertions describe how a structure such as "subgroups" sits inside a larger ordered set such as "all subsets".