feat(order/category/Lattice): The category of lattices (#11968)

Define `Lattice`, the category of lattices with lattice homs.

Author: YaelDillies

src/category_theory/concrete_category/bundled_hom.lean

@@ -63,7 +63,7 @@ intros; apply 𝒞.hom_ext;
 
 This instance generates the type-class problem `bundled_hom ?m` (which is why this is marked as
 `[nolint]`). Currently that is not a problem, as there are almost no instances of `bundled_hom`. -/
-@[nolint dangerous_instance] instance : concrete_category.{u} (bundled c) :=
+@[nolint dangerous_instance] instance concrete_category : concrete_category.{u} (bundled c) :=
 { forget := { obj := λ X, X,
               map := λ X Y f, 𝒞.to_fun X.str Y.str f,
               map_id' := λ X, 𝒞.id_to_fun X.str,

src/order/category/Lattice.lean

@@ -0,0 +1,73 @@
+/-
+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.PartialOrder
+import order.hom.lattice
+
+/-!
+# The category of lattices
+
+This defines `Lattice`, the category of lattices.
+
+Note that `Lattice` doesn't correspond to the literature definition of `Lat` as we don't require
+bottom or top elements. Instead, `Lat` corresponds to `BoundedLattice` (not yet in mathlib).
+
+## TODO
+
+The free functor from `Lattice` to `BoundedLattice` is `X → with_top (with_bot X)`.
+-/
+
+universes u
+
+open category_theory
+
+/-- The category of lattices. -/
+def Lattice := bundled lattice
+
+namespace Lattice
+
+instance : has_coe_to_sort Lattice Type* := bundled.has_coe_to_sort
+instance (X : Lattice) : lattice X := X.str
+
+/-- Construct a bundled `Lattice` from a `lattice`. -/
+def of (α : Type*) [lattice α] : Lattice := bundled.of α
+
+instance : inhabited Lattice := ⟨of bool⟩
+
+instance : bundled_hom @lattice_hom :=
+{ to_fun := λ _ _ _ _, coe_fn,
+  id := @lattice_hom.id,
+  comp := @lattice_hom.comp,
+  hom_ext := λ X Y _ _, by exactI fun_like.coe_injective }
+
+instance : large_category.{u} Lattice := bundled_hom.category lattice_hom
+instance : concrete_category Lattice := bundled_hom.concrete_category lattice_hom
+
+instance has_forget_to_PartialOrder : has_forget₂ Lattice PartialOrder :=
+{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y f, f },
+  forget_comp := rfl }
+
+/-- Constructs an isomorphism of lattices from an order isomorphism between them. -/
+@[simps] def iso.mk {α β : Lattice.{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 : Lattice ⥤ Lattice :=
+{ obj := λ X, of (order_dual X), map := λ X Y, lattice_hom.dual }
+
+/-- The equivalence between `Lattice` and itself induced by `order_dual` both ways. -/
+@[simps functor inverse] def dual_equiv : Lattice ≌ Lattice :=
+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 Lattice
+
+lemma Lattice_dual_comp_forget_to_PartialOrder :
+  Lattice.dual ⋙ forget₂ Lattice PartialOrder =
+    forget₂ Lattice PartialOrder ⋙ PartialOrder.to_dual := rfl

src/order/category/LinearOrder.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 
-import order.category.PartialOrder
+import order.category.Lattice
 
 /-!
 # Category of linear orders
@@ -34,8 +34,9 @@ instance : inhabited LinearOrder := ⟨of punit⟩
 
 instance (α : LinearOrder) : linear_order α := α.str
 
-instance has_forget_to_PartialOrder : has_forget₂ LinearOrder PartialOrder :=
-bundled_hom.forget₂ _ _
+instance has_forget_to_Lattice : has_forget₂ LinearOrder Lattice :=
+{ forget₂ := { obj := λ X, Lattice.of X,
+               map := λ X Y f, (order_hom_class.to_lattice_hom X Y f : lattice_hom X Y) } }
 
 /-- Constructs an equivalence between linear orders from an order isomorphism between them. -/
 @[simps] def iso.mk {α β : LinearOrder.{u}} (e : α ≃o β) : α ≅ β :=
@@ -45,17 +46,17 @@ bundled_hom.forget₂ _ _
   inv_hom_id' := by { ext, exact e.apply_symm_apply x } }
 
 /-- `order_dual` as a functor. -/
-@[simps] def to_dual : LinearOrder ⥤ LinearOrder :=
+@[simps] def dual : LinearOrder ⥤ LinearOrder :=
 { obj := λ X, of (order_dual X), map := λ X Y, order_hom.dual }
 
-/-- The equivalence between `PartialOrder` and itself induced by `order_dual` both ways. -/
+/-- The equivalence between `LinearOrder` and itself induced by `order_dual` both ways. -/
 @[simps functor inverse] def dual_equiv : LinearOrder ≌ LinearOrder :=
-equivalence.mk to_dual to_dual
+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 LinearOrder
 
-lemma LinearOrder_dual_equiv_comp_forget_to_PartialOrder :
-  LinearOrder.dual_equiv.functor ⋙ forget₂ LinearOrder PartialOrder
-  = forget₂ LinearOrder PartialOrder ⋙ PartialOrder.dual_equiv.functor := rfl
+lemma LinearOrder_dual_comp_forget_to_Lattice :
+  LinearOrder.dual ⋙ forget₂ LinearOrder Lattice = forget₂ LinearOrder Lattice ⋙ Lattice.dual :=
+rfl

src/order/hom/lattice.lean

@@ -32,7 +32,7 @@ be satisfied by itself and all stricter types.
 Do we need more intersections between `bot_hom`, `top_hom` and lattice homomorphisms?
 -/
 
-open function
+open function order_dual
 
 variables {F α β γ δ : Type*}
 
@@ -114,6 +114,20 @@ instance bounded_lattice_hom_class.to_bounded_order_hom_class [lattice α] [latt
   bounded_order_hom_class F α β :=
 { .. ‹bounded_lattice_hom_class F α β› }
 
+@[priority 100] -- See note [lower instance priority]
+instance order_iso.sup_hom_class [semilattice_sup α] [semilattice_sup β] :
+  sup_hom_class (α ≃o β) α β :=
+{ map_sup := λ f, f.map_sup, ..rel_iso.rel_hom_class }
+
+@[priority 100] -- See note [lower instance priority]
+instance order_iso.inf_hom_class [semilattice_inf α] [semilattice_inf β] :
+  inf_hom_class (α ≃o β) α β :=
+{ map_inf := λ f, f.map_inf, ..rel_iso.rel_hom_class }
+
+@[priority 100] -- See note [lower instance priority]
+instance order_iso.lattice_hom_class [lattice α] [lattice β] : lattice_hom_class (α ≃o β) α β :=
+{ ..order_iso.sup_hom_class, ..order_iso.inf_hom_class }
+
 instance [has_sup α] [has_sup β] [sup_hom_class F α β] : has_coe_t F (sup_hom α β) :=
 ⟨λ f, ⟨f, map_sup f⟩⟩
 
@@ -366,6 +380,18 @@ lemma cancel_left {g : lattice_hom β γ} {f₁ f₂ : lattice_hom α β} (hg :
 ⟨λ h, lattice_hom.ext $ λ a, hg $
   by rw [←lattice_hom.comp_apply, h, lattice_hom.comp_apply], congr_arg _⟩
 
+/-- Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices. -/
+@[simps] protected def dual :
+   lattice_hom α β ≃ lattice_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, { to_fun := to_dual ∘ f ∘ of_dual,
+                   map_sup' := λ _ _, congr_arg to_dual (map_inf f _ _),
+                   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 _ _),
+                   map_inf' := λ _ _, congr_arg of_dual (map_sup f _ _) },
+  left_inv := λ f, ext $ λ a, rfl,
+  right_inv := λ f, ext $ λ a, rfl }
+
 end lattice_hom
 
 namespace order_hom_class