Galois connections between preorders are adjunctions.

• GaloisConnection.adjunction is the adjunction associated to a Galois connection.

def GaloisConnection.adjunction {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {l : X → Y} {u : Y → X} (gc : GaloisConnection l u) : ⋯.functor ⊣ ⋯.functor

A Galois connection between preorders induces an adjunction between the associated categories.

Equations

• One or more equations did not get rendered due to their size.

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

An adjunction between preorder categories induces a Galois connection.