feat: port CategoryTheory.Category.GaloisConnection (#2440)

Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib.lean

@@ -230,6 +230,7 @@ import Mathlib.CategoryTheory.Bicategory.Basic
 import Mathlib.CategoryTheory.Bicategory.Strict
 import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.CategoryTheory.Category.Cat
+import Mathlib.CategoryTheory.Category.GaloisConnection
 import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Category.RelCat

Mathlib/CategoryTheory/Category/GaloisConnection.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
+
+! This file was ported from Lean 3 source module category_theory.category.galois_connection
+! leanprover-community/mathlib commit d82b87871d9a274884dff5263fa4f5d93bcce1d6
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Category.Preorder
+import Mathlib.CategoryTheory.Adjunction.Basic
+import Mathlib.Order.GaloisConnection
+
+/-!
+
+# Galois connections between preorders are adjunctions.
+
+* `GaloisConnection.adjunction` is the adjunction associated to a galois connection.
+
+-/
+
+
+universe u v
+
+section
+
+variable {X : Type u} {Y : Type v} [Preorder X] [Preorder Y]
+
+/-- 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 =>
+        ⟨fun f => CategoryTheory.homOfLE (gc.le_u f.le),
+         fun f => CategoryTheory.homOfLE (gc.l_le f.le), _, _⟩ }
+#align galois_connection.adjunction GaloisConnection.adjunction
+
+end
+
+namespace CategoryTheory
+
+variable {X : Type u} {Y : Type v} [Preorder X] [Preorder Y]
+
+/-- 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⟩
+#align category_theory.adjunction.gc CategoryTheory.Adjunction.gc
+
+end CategoryTheory