adjunction — Mathlib

English

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

Русский

Связь Галоиса между предварительно порядками индуцирует смежность между соответствующими категориями.

LaTeX

$$$$\\text{ gc }(L,u) \\Rightarrow L_{⋅} \\dashv R_{⋅}. $$$$

Lean4

/-- A Galois connection between preorders induces an adjunction between the associated categories.
-/
def 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 cat_disch
          right_inv := by cat_disch } }

Похожие утверждения