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) : Monotone.functor (_ : Monotone l) ⊣ Monotone.functor (_ : Monotone u)

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 : CategoryTheory.Functor X Y} {R : CategoryTheory.Functor Y X} (adj : L ⊣ R) : GaloisConnection L.obj R.obj

An adjunction between preorder categories induces a galois connection.