gc — Mathlib · SciLib

English

The adjunction constructed from a Galois connection provides a natural correspondence between hom-sets.

Русский

Смежность, построенная из связи Галоиса, обеспечивает естественную соотнесенность множеств гомоморфизмов.

LaTeX

$$$$\\operatorname{adjunction}(gc) : L \\dashv R.$$$$

Lean4

/-- An adjunction between preorder categories induces a Galois connection.
-/
theorem 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⟩

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