CategoryTheory.Adjunction.gc

theorem CategoryTheory.Adjunction.gc : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] {L : CategoryTheory.Functor X Y} {R : CategoryTheory.Functor Y X}, (L ⊣ R) → GaloisConnection L.obj R.obj

This theorem states that, given two types `X` and `Y` which are both preordered, and two functors `L` and `R` from the category theory, if `L` is left adjoint to `R` (denoted as `L ⊣ R`), then these functors induce a Galois connection. Specifically, the functor `L.obj` and `R.obj` will form the pair of functions `l` and `u` such that for all elements `a` in type `X` and `b` in type `Y`, `l a ≤ b` if and only if `a ≤ u b`, which is the definition of a Galois connection. In other words, an adjunction between preorder categories results in a Galois connection.

More concisely: Given two preordered types `X` and `Y` and left adjoint functors `L` and `R` between them, the induced functions `L.obj` and `R.obj` form a Galois connection, i.e., `l(a) ≤ b` if and only if `a ≤ u(b)` for all `a ∈ X` and `b ∈ Y`.