Module docstring
{"# Galois connections between preorders are adjunctions.
GaloisConnection.adjunctionis the adjunction associated to a galois connection.
"}
GaloisConnection.adjunction
definition
{l : X → Y} {u : Y → X} (gc : GaloisConnection l u) : gc.monotone_l.functor ⊣ gc.monotone_u.functor
Full source
/-- A galois connection between preorders induces an adjunction between the associated categories.
-/
def GaloisConnection.adjunction {l : X → Y} {u : Y → X} (gc : GaloisConnection l u) :
gc.monotone_l.functor ⊣ gc.monotone_u.functor :=
CategoryTheory.Adjunction.mkOfHomEquiv
{ homEquiv := fun X Y =>
{ toFun := fun f => CategoryTheory.homOfLE (gc.le_u f.le)
invFun := fun f => CategoryTheory.homOfLE (gc.l_le f.le)
left_inv := by aesop_cat
right_inv := by aesop_cat } }Informal description
Given a Galois connection $(l, u)$ between preorders $X$ and $Y$, where $l \colon X \to Y$ and $u \colon Y \to X$ are monotone functions satisfying $l(x) \leq y \leftrightarrow x \leq u(y)$ for all $x \in X$ and $y \in Y$, the associated adjunction is constructed between the functors induced by $l$ and $u$ on the corresponding preorder categories. Specifically, the left adjoint is the functor induced by $l$ and the right adjoint is the functor induced by $u$.
CategoryTheory.Adjunction.gc
theorem
{L : X ⥤ Y} {R : Y ⥤ X} (adj : L ⊣ R) : GaloisConnection L.obj R.obj
Full source
/-- An adjunction between preorder categories induces a galois connection.
-/
theorem Adjunction.gc {L : X ⥤ Y} {R : Y ⥤ X} (adj : L ⊣ R) : GaloisConnection L.obj R.obj :=
fun x y =>
⟨fun h => ((adj.homEquiv x y).toFun h.hom).le, fun h => ((adj.homEquiv x y).invFun h.hom).le⟩Informal description
Given an adjunction $L \dashv R$ between functors $L \colon X \to Y$ and $R \colon Y \to X$ where $X$ and $Y$ are preorders viewed as categories, there is an induced Galois connection between the object mappings $L$ and $R$. Specifically, for all $x \in X$ and $y \in Y$, we have $L(x) \leq y$ if and only if $x \leq R(y)$.