Galois connections between preorders are adjunctions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
galois_connection.adjunctionis the adjunction associated to a galois connection.
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
- gc.adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X_1 : X) (Y_1 : Y), {to_fun := λ (f : _.functor.obj X_1 ⟶ Y_1), _.hom, inv_fun := λ (f : X_1 ⟶ _.functor.obj Y_1), _.hom, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}