mathlib documentation

category_theory.category.galois_connection

Galois connections between preorders are adjunctions. #

def galois_connection.adjunction {X : Type u} {Y : Type v} [preorder X] [preorder Y] {l : X Y} {u : Y X} (gc : galois_connection l u) :

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

Equations
theorem category_theory.adjunction.gc {X : Type u} {Y : Type v} [preorder X] [preorder Y] {L : X Y} {R : Y X} (adj : L R) :

An adjunction between preorder categories induces a galois connection.