From 34a3845a00478838367ed51636c677c8b3646656 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 14 Jun 2023 20:20:18 +0000
Subject: [PATCH] feat: port Order.Category.CompleteLatCat (#5019)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
---
 Mathlib.lean                               |   1 +
 Mathlib/Order/Category/BddOrdCat.lean      |   1 +
 Mathlib/Order/Category/CompleteLatCat.lean | 101 +++++++++++++++++++++
 Mathlib/Order/Category/SemilatCat.lean     |   1 +
 4 files changed, 104 insertions(+)
 create mode 100644 Mathlib/Order/Category/CompleteLatCat.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 36d6ce9015e13..ef4d6f6dc1f9b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2273,6 +2273,7 @@ import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Order.Category.BddDistLatCat
 import Mathlib.Order.Category.BddLatCat
 import Mathlib.Order.Category.BddOrdCat
+import Mathlib.Order.Category.CompleteLatCat
 import Mathlib.Order.Category.DistLatCat
 import Mathlib.Order.Category.FinPartOrd
 import Mathlib.Order.Category.FrmCat
diff --git a/Mathlib/Order/Category/BddOrdCat.lean b/Mathlib/Order/Category/BddOrdCat.lean
index 8ac05c1dbcd26..b53bd7e29df2a 100644
--- a/Mathlib/Order/Category/BddOrdCat.lean
+++ b/Mathlib/Order/Category/BddOrdCat.lean
@@ -65,6 +65,7 @@ instance largeCategory : LargeCategory.{u} BddOrdCat where
 #align BddOrd.large_category BddOrdCat.largeCategory
 
 -- Porting note: added.
+-- see https://github.com/leanprover-community/mathlib4/issues/5017
 instance instFunLike (X Y : BddOrdCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
   show FunLike (BoundedOrderHom X Y) X (fun _ => Y) from inferInstance
 
diff --git a/Mathlib/Order/Category/CompleteLatCat.lean b/Mathlib/Order/Category/CompleteLatCat.lean
new file mode 100644
index 0000000000000..7f59b17a9f957
--- /dev/null
+++ b/Mathlib/Order/Category/CompleteLatCat.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+
+! This file was ported from Lean 3 source module order.category.CompleteLat
+! leanprover-community/mathlib commit e8ac6315bcfcbaf2d19a046719c3b553206dac75
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Order.Category.BddLatCat
+import Mathlib.Order.Hom.CompleteLattice
+
+/-!
+# The category of complete lattices
+
+This file defines `CompleteLatCat`, the category of complete lattices.
+-/
+
+set_option linter.uppercaseLean3 false
+
+universe u
+
+open CategoryTheory
+
+/-- The category of complete lattices. -/
+def CompleteLatCat :=
+  Bundled CompleteLattice
+#align CompleteLat CompleteLatCat
+
+namespace CompleteLatCat
+
+instance : CoeSort CompleteLatCat (Type _) :=
+  Bundled.coeSort
+
+instance (X : CompleteLatCat) : CompleteLattice X :=
+  X.str
+
+/-- Construct a bundled `CompleteLatCat` from a `CompleteLattice`. -/
+def of (α : Type _) [CompleteLattice α] : CompleteLatCat :=
+  Bundled.of α
+#align CompleteLat.of CompleteLatCat.of
+
+@[simp]
+theorem coe_of (α : Type _) [CompleteLattice α] : ↥(of α) = α :=
+  rfl
+#align CompleteLat.coe_of CompleteLatCat.coe_of
+
+instance : Inhabited CompleteLatCat :=
+  ⟨of PUnit⟩
+
+instance : BundledHom @CompleteLatticeHom where
+  toFun _ _ f := f.toFun
+  id := @CompleteLatticeHom.id
+  comp := @CompleteLatticeHom.comp
+  hom_ext _ _ _ _ h := FunLike.coe_injective h
+
+deriving instance LargeCategory for CompleteLatCat
+
+instance : ConcreteCategory CompleteLatCat :=
+  by dsimp [CompleteLatCat];  infer_instance
+
+instance hasForgetToBddLat : HasForget₂ CompleteLatCat BddLatCat where
+  forget₂ :=
+    { obj := fun X => BddLatCat.of X
+      map := fun {X Y} => CompleteLatticeHom.toBoundedLatticeHom }
+  forget_comp := rfl
+#align CompleteLat.has_forget_to_BddLat CompleteLatCat.hasForgetToBddLat
+
+/-- Constructs an isomorphism of complete lattices from an order isomorphism between them. -/
+@[simps]
+def Iso.mk {α β : CompleteLatCat.{u}} (e : α ≃o β) : α ≅ β where
+  hom := (e : CompleteLatticeHom _ _) -- Porting note: TODO, wrong?
+  inv := (e.symm : CompleteLatticeHom _ _)
+  hom_inv_id := by ext; exact e.symm_apply_apply _
+  inv_hom_id := by ext; exact e.apply_symm_apply _
+#align CompleteLat.iso.mk CompleteLatCat.Iso.mk
+
+/-- `OrderDual` as a functor. -/
+@[simps]
+def dual : CompleteLatCat ⥤ CompleteLatCat where
+  obj X := of Xᵒᵈ
+  map {X Y} := CompleteLatticeHom.dual
+#align CompleteLat.dual CompleteLatCat.dual
+
+/-- The equivalence between `CompleteLatCat` and itself induced by `OrderDual` both ways. -/
+@[simps functor inverse]
+def dualEquiv : CompleteLatCat ≌ CompleteLatCat where
+  functor := dual
+  inverse := dual
+  unitIso := NatIso.ofComponents fun X => Iso.mk <| OrderIso.dualDual X
+  counitIso := NatIso.ofComponents fun X => Iso.mk <| OrderIso.dualDual X
+#align CompleteLat.dual_equiv CompleteLatCat.dualEquiv
+
+end CompleteLatCat
+
+theorem completeLatCat_dual_comp_forget_to_bddLatCat :
+    CompleteLatCat.dual ⋙ forget₂ CompleteLatCat BddLatCat =
+    forget₂ CompleteLatCat BddLatCat ⋙ BddLatCat.dual :=
+  rfl
+#align CompleteLat_dual_comp_forget_to_BddLat completeLatCat_dual_comp_forget_to_bddLatCat
diff --git a/Mathlib/Order/Category/SemilatCat.lean b/Mathlib/Order/Category/SemilatCat.lean
index cf67a9e0da4b2..079572d6663cd 100644
--- a/Mathlib/Order/Category/SemilatCat.lean
+++ b/Mathlib/Order/Category/SemilatCat.lean
@@ -71,6 +71,7 @@ instance : LargeCategory.{u} SemilatSupCat where
   assoc _ _ _ := SupBotHom.comp_assoc _ _ _
 
 -- Porting note: added
+-- see https://github.com/leanprover-community/mathlib4/issues/5017
 instance instFunLike (X Y : SemilatSupCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
   show FunLike (SupBotHom X Y) X (fun _ => Y) from inferInstance