feat(order/category/CompleteLattice): The category of complete lattices (#12348)

Define `CompleteLattice`, the category of complete lattices with complete lattice homomorphisms.

Author: YaelDillies

src/order/category/CompleteLattice.lean

@@ -0,0 +1,66 @@
+/-
+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
+-/
+import order.category.BoundedLattice
+import order.hom.complete_lattice
+
+/-!
+# The category of complete lattices
+
+This file defines `CompleteLattice`, the category of complete lattices.
+-/
+
+universes u
+
+open category_theory
+
+/-- The category of complete lattices. -/
+def CompleteLattice := bundled complete_lattice
+
+namespace CompleteLattice
+
+instance : has_coe_to_sort CompleteLattice Type* := bundled.has_coe_to_sort
+instance (X : CompleteLattice) : complete_lattice X := X.str
+
+/-- Construct a bundled `CompleteLattice` from a `complete_lattice`. -/
+def of (α : Type*) [complete_lattice α] : CompleteLattice := bundled.of α
+
+instance : inhabited CompleteLattice := ⟨of punit⟩
+
+instance : bundled_hom @complete_lattice_hom :=
+{ to_fun := λ _ _ _ _, coe_fn,
+  id := @complete_lattice_hom.id,
+  comp := @complete_lattice_hom.comp,
+  hom_ext := λ X Y _ _, by exactI fun_like.coe_injective }
+instance : large_category.{u} CompleteLattice := bundled_hom.category complete_lattice_hom
+instance : concrete_category CompleteLattice := bundled_hom.concrete_category complete_lattice_hom
+
+instance has_forget_to_BoundedLattice : has_forget₂ CompleteLattice BoundedLattice :=
+{ forget₂ := { obj := λ X, BoundedLattice.of X,
+               map := λ X Y, complete_lattice_hom.to_bounded_lattice_hom },
+  forget_comp := rfl }
+
+/-- Constructs an isomorphism of complete lattices from an order isomorphism between them. -/
+@[simps] def iso.mk {α β : CompleteLattice.{u}} (e : α ≃o β) : α ≅ β :=
+{ hom := e,
+  inv := e.symm,
+  hom_inv_id' := by { ext, exact e.symm_apply_apply _ },
+  inv_hom_id' := by { ext, exact e.apply_symm_apply _ } }
+
+/-- `order_dual` as a functor. -/
+@[simps] def dual : CompleteLattice ⥤ CompleteLattice :=
+{ obj := λ X, of (order_dual X), map := λ X Y, complete_lattice_hom.dual }
+
+/-- The equivalence between `CompleteLattice` and itself induced by `order_dual` both ways. -/
+@[simps functor inverse] def dual_equiv : CompleteLattice ≌ CompleteLattice :=
+equivalence.mk dual dual
+  (nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
+  (nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
+
+end CompleteLattice
+
+lemma CompleteLattice_dual_comp_forget_to_BoundedLattice :
+  CompleteLattice.dual ⋙ forget₂ CompleteLattice BoundedLattice =
+    forget₂ CompleteLattice BoundedLattice ⋙ BoundedLattice.dual := rfl

src/order/hom/complete_lattice.lean

@@ -29,7 +29,7 @@ be satisfied by itself and all stricter types.
 * `complete_lattice_hom_class`
 -/
 
-open function
+open function order_dual
 
 variables {F α β γ δ : Type*} {ι : Sort*} {κ : ι → Sort*}
 
@@ -149,6 +149,13 @@ instance complete_lattice_hom_class.to_bounded_lattice_hom_class [complete_latti
   bounded_lattice_hom_class F α β :=
 { ..Sup_hom_class.to_bot_hom_class, ..Inf_hom_class.to_top_hom_class }
 
+@[priority 100] -- See note [lower instance priority]
+instance order_iso.complete_lattice_hom_class [complete_lattice α] [complete_lattice β] :
+  complete_lattice_hom_class (α ≃o β) α β :=
+{ map_Sup := λ f s, (f.map_Sup s).trans Sup_image.symm,
+  map_Inf := λ f s, (f.map_Inf s).trans Inf_image.symm,
+  ..rel_iso.rel_hom_class }
+
 instance [has_Sup α] [has_Sup β] [Sup_hom_class F α β] : has_coe_t F (Sup_hom α β) :=
 ⟨λ f, ⟨f, map_Sup f⟩⟩
 
@@ -325,6 +332,26 @@ instance : order_top (Inf_hom α β) := ⟨⊤, λ f a, le_top⟩
 
 end Inf_hom
 
+/-- Reinterpret a `⨆`-homomorphism as an `⨅`-homomorphism between the dual orders. -/
+@[simps] protected def Sup_hom.dual [has_Sup α] [has_Sup β] :
+  Sup_hom α β ≃ Inf_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, { to_fun := to_dual ∘ f ∘ of_dual,
+                   map_Inf' := λ _, congr_arg to_dual (map_Sup f _) },
+  inv_fun := λ f, { to_fun := of_dual ∘ f ∘ to_dual,
+                   map_Sup' := λ _, congr_arg of_dual (map_Inf f _) },
+  left_inv := λ f, Sup_hom.ext $ λ a, rfl,
+  right_inv := λ f, Inf_hom.ext $ λ a, rfl }
+
+/-- Reinterpret an `⨅`-homomorphism as a `⨆`-homomorphism between the dual orders. -/
+@[simps] protected def Inf_hom.dual [has_Inf α] [has_Inf β] :
+  Inf_hom α β ≃ Sup_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, { to_fun := to_dual ∘ f ∘ of_dual,
+                   map_Sup' := λ _, congr_arg to_dual (map_Inf f _) },
+  inv_fun := λ f, { to_fun := of_dual ∘ f ∘ to_dual,
+                   map_Inf' := λ _, congr_arg of_dual (map_Sup f _) },
+  left_inv := λ f, Inf_hom.ext $ λ a, rfl,
+  right_inv := λ f, Sup_hom.ext $ λ a, rfl }
+
 /-! ### Frame homomorphisms -/
 
 namespace frame_hom
@@ -413,6 +440,9 @@ instance : complete_lattice_hom_class (complete_lattice_hom α β) α β :=
   map_Sup := λ f, f.map_Sup',
   map_Inf := λ f, f.map_Inf' }
 
+/-- Reinterpret a `complete_lattice_hom` as a `bounded_lattice_hom`. -/
+def to_bounded_lattice_hom (f : complete_lattice_hom α β) : bounded_lattice_hom α β := f
+
 /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
 directly. -/
 instance : has_coe_to_fun (complete_lattice_hom α β) (λ _, α → β) := ⟨λ f, f.to_fun⟩
@@ -466,4 +496,14 @@ lemma cancel_left {g : complete_lattice_hom β γ} {f₁ f₂ : complete_lattice
   g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
 ⟨λ h, ext $ λ a, hg $ by rw [←comp_apply, h, comp_apply], congr_arg _⟩
 
+/-- Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices. -/
+@[simps] protected def dual :
+   complete_lattice_hom α β ≃ complete_lattice_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, { to_Sup_hom := f.to_Inf_hom.dual,
+                   map_Inf' := λ _, congr_arg to_dual (map_Sup f _) },
+  inv_fun := λ f, { to_Sup_hom := f.to_Inf_hom.dual,
+                    map_Inf' := λ _, congr_arg of_dual (map_Sup f _) },
+  left_inv := λ f, ext $ λ a, rfl,
+  right_inv := λ f, ext $ λ a, rfl }
+
 end complete_lattice_hom