# 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.

## Instances For

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.