feat(order/hom/*): equivalences mapping morphisms to their dual (#12888)

Add missing `whatever_hom.dual` equivalences.

src/order/hom/basic.lean

@@ -353,6 +353,14 @@ subsingleton.elim _ _
   left_inv := λ f, ext _ _ rfl,
   right_inv := λ f, ext _ _ rfl }
 
+@[simp] lemma dual_id : (order_hom.id : α →o α).dual = order_hom.id := rfl
+@[simp] lemma dual_comp (g : β →o γ) (f : α →o β) : (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : order_hom.dual.symm order_hom.id = (order_hom.id : α →o α) := rfl
+@[simp] lemma symm_dual_comp (g : order_dual β →o order_dual γ)
+  (f : order_dual α →o order_dual β) :
+  order_hom.dual.symm (g.comp f) = (order_hom.dual.symm g).comp (order_hom.dual.symm f) := rfl
+
 /-- `order_hom.dual` as an order isomorphism. -/
 def dual_iso (α β : Type*) [preorder α] [preorder β] :
   (α →o β) ≃o order_dual (order_dual α →o order_dual β) :=

src/order/hom/bounded.lean

@@ -420,17 +420,74 @@ lemma cancel_left {g : bounded_order_hom β γ} {f₁ f₂ : bounded_order_hom 
 ⟨λ h, bounded_order_hom.ext $ λ a, hg $
   by rw [←bounded_order_hom.comp_apply, h, bounded_order_hom.comp_apply], congr_arg _⟩
 
+end bounded_order_hom
+
+/-! ### Dual homs -/
+
+namespace top_hom
+variables [has_le α] [order_top α] [has_le β] [order_top β] [has_le γ] [order_top γ]
+
+/-- Reinterpret a top homomorphism as a bot homomorphism between the dual lattices. -/
+@[simps] protected def dual : top_hom α β ≃ bot_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, ⟨f, f.map_top'⟩,
+  inv_fun := λ f, ⟨f, f.map_bot'⟩,
+  left_inv := λ f, top_hom.ext $ λ _, rfl,
+  right_inv := λ f, bot_hom.ext $ λ _, rfl }
+
+@[simp] lemma dual_id : (top_hom.id α).dual = bot_hom.id _ := rfl
+@[simp] lemma dual_comp (g : top_hom β γ) (f : top_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : top_hom.dual.symm (bot_hom.id _) = top_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : bot_hom (order_dual β) (order_dual γ))
+  (f : bot_hom (order_dual α) (order_dual β)) :
+  top_hom.dual.symm (g.comp f) = (top_hom.dual.symm g).comp (top_hom.dual.symm f) := rfl
+
+end top_hom
+
+namespace bot_hom
+variables [has_le α] [order_bot α] [has_le β] [order_bot β] [has_le γ] [order_bot γ]
+
+/-- Reinterpret a bot homomorphism as a top homomorphism between the dual lattices. -/
+@[simps] protected def dual : bot_hom α β ≃ top_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, ⟨f, f.map_bot'⟩,
+  inv_fun := λ f, ⟨f, f.map_top'⟩,
+  left_inv := λ f, bot_hom.ext $ λ _, rfl,
+  right_inv := λ f, top_hom.ext $ λ _, rfl }
+
+@[simp] lemma dual_id : (bot_hom.id α).dual = top_hom.id _ := rfl
+@[simp] lemma dual_comp (g : bot_hom β γ) (f : bot_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : bot_hom.dual.symm (top_hom.id _) = bot_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : top_hom (order_dual β) (order_dual γ))
+  (f : top_hom (order_dual α) (order_dual β)) :
+  bot_hom.dual.symm (g.comp f) = (bot_hom.dual.symm g).comp (bot_hom.dual.symm f) := rfl
+
+end bot_hom
+
+namespace bounded_order_hom
+variables [preorder α] [bounded_order α] [preorder β] [bounded_order β] [preorder γ]
+  [bounded_order γ]
+
 /-- Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual
 orders. -/
 @[simps] protected def dual :
    bounded_order_hom α β ≃ bounded_order_hom (order_dual α) (order_dual β) :=
-{ to_fun := λ f, { to_order_hom := f.to_order_hom.dual,
-                   map_top' := congr_arg to_dual (map_bot f),
-                   map_bot' := congr_arg to_dual (map_top f) },
-  inv_fun := λ f, { to_order_hom := order_hom.dual.symm f.to_order_hom,
-                    map_top' := map_bot f,
-                    map_bot' := map_top f },
+{ to_fun := λ f, ⟨f.to_order_hom.dual, f.map_bot', f.map_top'⟩,
+  inv_fun := λ f, ⟨order_hom.dual.symm f.to_order_hom, f.map_bot', f.map_top'⟩,
   left_inv := λ f, ext $ λ a, rfl,
   right_inv := λ f, ext $ λ a, rfl }
 
+@[simp] lemma dual_id : (bounded_order_hom.id α).dual = bounded_order_hom.id _ := rfl
+@[simp] lemma dual_comp (g : bounded_order_hom β γ) (f : bounded_order_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id :
+  bounded_order_hom.dual.symm (bounded_order_hom.id _) = bounded_order_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : bounded_order_hom (order_dual β) (order_dual γ))
+  (f : bounded_order_hom (order_dual α) (order_dual β)) :
+  bounded_order_hom.dual.symm (g.comp f) =
+    (bounded_order_hom.dual.symm g).comp (bounded_order_hom.dual.symm f) := rfl
+
 end bounded_order_hom

src/order/hom/complete_lattice.lean

@@ -339,26 +339,6 @@ 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
@@ -496,17 +476,77 @@ 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 _⟩
 
+end complete_lattice_hom
+
+/-! ### Dual homs -/
+
+namespace Sup_hom
+variables [has_Sup α] [has_Sup β] [has_Sup γ]
+
+/-- Reinterpret a `⨆`-homomorphism as an `⨅`-homomorphism between the dual orders. -/
+@[simps] protected def dual : Sup_hom α β ≃ Inf_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, ⟨to_dual ∘ f ∘ of_dual, f.map_Sup'⟩,
+  inv_fun := λ f, ⟨of_dual ∘ f ∘ to_dual, f.map_Inf'⟩,
+  left_inv := λ f, Sup_hom.ext $ λ a, rfl,
+  right_inv := λ f, Inf_hom.ext $ λ a, rfl }
+
+@[simp] lemma dual_id : (Sup_hom.id α).dual = Inf_hom.id _ := rfl
+@[simp] lemma dual_comp (g : Sup_hom β γ) (f : Sup_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : Sup_hom.dual.symm (Inf_hom.id _) = Sup_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : Inf_hom (order_dual β) (order_dual γ))
+  (f : Inf_hom (order_dual α) (order_dual β)) :
+  Sup_hom.dual.symm (g.comp f) = (Sup_hom.dual.symm g).comp (Sup_hom.dual.symm f) := rfl
+
+end Sup_hom
+
+namespace Inf_hom
+variables [has_Inf α] [has_Inf β] [has_Inf γ]
+
+/-- Reinterpret an `⨅`-homomorphism as a `⨆`-homomorphism between the dual orders. -/
+@[simps] protected def dual : 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 }
+
+@[simp] lemma dual_id : (Inf_hom.id α).dual = Sup_hom.id _ := rfl
+@[simp] lemma dual_comp (g : Inf_hom β γ) (f : Inf_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : Inf_hom.dual.symm (Sup_hom.id _) = Inf_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : Sup_hom (order_dual β) (order_dual γ))
+  (f : Sup_hom (order_dual α) (order_dual β)) :
+  Inf_hom.dual.symm (g.comp f) = (Inf_hom.dual.symm g).comp (Inf_hom.dual.symm f) := rfl
+
+end Inf_hom
+
+namespace complete_lattice_hom
+variables [complete_lattice α] [complete_lattice β] [complete_lattice γ]
+
 /-- Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual
 lattices. -/
 @[simps] protected def dual :
    complete_lattice_hom α β ≃ complete_lattice_hom (order_dual α) (order_dual β) :=
-{ to_fun := λ f, { to_Inf_hom := f.to_Sup_hom.dual,
-                   map_Sup' := λ _, congr_arg to_dual (map_Inf f _) },
-  inv_fun := λ f, { to_Inf_hom := f.to_Sup_hom.dual,
-                    map_Sup' := λ _, congr_arg of_dual (map_Inf f _) },
+{ to_fun := λ f, ⟨f.to_Sup_hom.dual, f.map_Inf'⟩,
+  inv_fun := λ f, ⟨f.to_Sup_hom.dual, f.map_Inf'⟩,
   left_inv := λ f, ext $ λ a, rfl,
   right_inv := λ f, ext $ λ a, rfl }
 
+@[simp] lemma dual_id : (complete_lattice_hom.id α).dual = complete_lattice_hom.id _ := rfl
+@[simp] lemma dual_comp (g : complete_lattice_hom β γ) (f : complete_lattice_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id :
+  complete_lattice_hom.dual.symm (complete_lattice_hom.id _) = complete_lattice_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : complete_lattice_hom (order_dual β) (order_dual γ))
+  (f : complete_lattice_hom (order_dual α) (order_dual β)) :
+  complete_lattice_hom.dual.symm (g.comp f) =
+    (complete_lattice_hom.dual.symm g).comp (complete_lattice_hom.dual.symm f) := rfl
+
 end complete_lattice_hom
 
 /-! ### Concrete homs -/

src/order/hom/lattice.lean

@@ -674,18 +674,6 @@ 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
@@ -797,17 +785,138 @@ lemma cancel_left {g : bounded_lattice_hom β γ} {f₁ f₂ : bounded_lattice_h
   g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
 ⟨λ h, ext $ λ a, hg $ by rw [←comp_apply, h, comp_apply], congr_arg _⟩
 
+end bounded_lattice_hom
+
+/-! ### Dual homs -/
+
+namespace sup_hom
+variables [has_sup α] [has_sup β] [has_sup γ]
+
+/-- Reinterpret a supremum homomorphism as an infimum homomorphism between the dual lattices. -/
+@[simps] protected def dual : sup_hom α β ≃ inf_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, ⟨f, f.map_sup'⟩,
+  inv_fun := λ f, ⟨f, f.map_inf'⟩,
+  left_inv := λ f, sup_hom.ext $ λ _, rfl,
+  right_inv := λ f, inf_hom.ext $ λ _, rfl }
+
+@[simp] lemma dual_id : (sup_hom.id α).dual = inf_hom.id _ := rfl
+@[simp] lemma dual_comp (g : sup_hom β γ) (f : sup_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : sup_hom.dual.symm (inf_hom.id _) = sup_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : inf_hom (order_dual β) (order_dual γ))
+  (f : inf_hom (order_dual α) (order_dual β)) :
+  sup_hom.dual.symm (g.comp f) = (sup_hom.dual.symm g).comp (sup_hom.dual.symm f) := rfl
+
+end sup_hom
+
+namespace inf_hom
+variables [has_inf α] [has_inf β] [has_inf γ]
+
+/-- Reinterpret an infimum homomorphism as a supremum homomorphism between the dual lattices. -/
+@[simps] protected def dual : inf_hom α β ≃ sup_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, ⟨f, f.map_inf'⟩,
+  inv_fun := λ f, ⟨f, f.map_sup'⟩,
+  left_inv := λ f, inf_hom.ext $ λ _, rfl,
+  right_inv := λ f, sup_hom.ext $ λ _, rfl }
+
+@[simp] lemma dual_id : (inf_hom.id α).dual = sup_hom.id _ := rfl
+@[simp] lemma dual_comp (g : inf_hom β γ) (f : inf_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : inf_hom.dual.symm (sup_hom.id _) = inf_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : sup_hom (order_dual β) (order_dual γ))
+  (f : sup_hom (order_dual α) (order_dual β)) :
+  inf_hom.dual.symm (g.comp f) = (inf_hom.dual.symm g).comp (inf_hom.dual.symm f) := rfl
+
+end inf_hom
+
+namespace sup_bot_hom
+variables [has_sup α] [has_bot α] [has_sup β] [has_bot β] [has_sup γ] [has_bot γ]
+
+/-- Reinterpret a finitary supremum homomorphism as a finitary infimum homomorphism between the dual
+lattices. -/
+def dual : sup_bot_hom α β ≃ inf_top_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, ⟨f.to_sup_hom.dual, f.map_bot'⟩,
+  inv_fun := λ f, ⟨sup_hom.dual.symm f.to_inf_hom, f.map_top'⟩,
+  left_inv := λ f, sup_bot_hom.ext $ λ _, rfl,
+  right_inv := λ f, inf_top_hom.ext $ λ _, rfl }
+
+@[simp] lemma dual_id : (sup_bot_hom.id α).dual = inf_top_hom.id _ := rfl
+@[simp] lemma dual_comp (g : sup_bot_hom β γ) (f : sup_bot_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : sup_bot_hom.dual.symm (inf_top_hom.id _) = sup_bot_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : inf_top_hom (order_dual β) (order_dual γ))
+  (f : inf_top_hom (order_dual α) (order_dual β)) :
+  sup_bot_hom.dual.symm (g.comp f) = (sup_bot_hom.dual.symm g).comp (sup_bot_hom.dual.symm f) := rfl
+
+end sup_bot_hom
+
+namespace inf_top_hom
+variables [has_inf α] [has_top α] [has_inf β] [has_top β] [has_inf γ] [has_top γ]
+
+/-- Reinterpret a finitary infimum homomorphism as a finitary supremum homomorphism between the dual
+lattices. -/
+@[simps] protected def dual : inf_top_hom α β ≃ sup_bot_hom (order_dual α) (order_dual β) :=
+{ to_fun := λ f, ⟨f.to_inf_hom.dual, f.map_top'⟩,
+  inv_fun := λ f, ⟨inf_hom.dual.symm f.to_sup_hom, f.map_bot'⟩,
+  left_inv := λ f, inf_top_hom.ext $ λ _, rfl,
+  right_inv := λ f, sup_bot_hom.ext $ λ _, rfl }
+
+@[simp] lemma dual_id : (inf_top_hom.id α).dual = sup_bot_hom.id _ := rfl
+@[simp] lemma dual_comp (g : inf_top_hom β γ) (f : inf_top_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : inf_top_hom.dual.symm (sup_bot_hom.id _) = inf_top_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : sup_bot_hom (order_dual β) (order_dual γ))
+  (f : sup_bot_hom (order_dual α) (order_dual β)) :
+  inf_top_hom.dual.symm (g.comp f) = (inf_top_hom.dual.symm g).comp (inf_top_hom.dual.symm f) := rfl
+
+end inf_top_hom
+
+namespace lattice_hom
+variables [lattice α] [lattice β] [lattice γ]
+
+/-- 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, ⟨f.to_inf_hom.dual, f.map_sup'⟩,
+  inv_fun := λ f, ⟨f.to_inf_hom.dual, f.map_sup'⟩,
+  left_inv := λ f, ext $ λ a, rfl,
+  right_inv := λ f, ext $ λ a, rfl }
+
+@[simp] lemma dual_id : (lattice_hom.id α).dual = lattice_hom.id _ := rfl
+@[simp] lemma dual_comp (g : lattice_hom β γ) (f : lattice_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id : lattice_hom.dual.symm (lattice_hom.id _) = lattice_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : lattice_hom (order_dual β) (order_dual γ))
+  (f : lattice_hom (order_dual α) (order_dual β)) :
+  lattice_hom.dual.symm (g.comp f) = (lattice_hom.dual.symm g).comp (lattice_hom.dual.symm f) := rfl
+
+end lattice_hom
+
+namespace bounded_lattice_hom
+variables [lattice α] [bounded_order α] [lattice β] [bounded_order β] [lattice γ] [bounded_order γ]
+
 /-- Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual
 bounded lattices. -/
 @[simps] protected def dual :
    bounded_lattice_hom α β ≃ bounded_lattice_hom (order_dual α) (order_dual β) :=
-{ to_fun := λ f, { to_lattice_hom := f.to_lattice_hom.dual,
-                   map_top' := congr_arg to_dual f.map_bot',
-                   map_bot' := congr_arg to_dual f.map_top' },
-  inv_fun := λ f, { to_lattice_hom := lattice_hom.dual.symm f.to_lattice_hom,
-                    map_top' := congr_arg of_dual f.map_bot',
-                    map_bot' := congr_arg of_dual f.map_top' },
+{ to_fun := λ f, ⟨f.to_lattice_hom.dual, f.map_bot', f.map_top'⟩,
+  inv_fun := λ f, ⟨lattice_hom.dual.symm f.to_lattice_hom, f.map_bot', f.map_top'⟩,
   left_inv := λ f, ext $ λ a, rfl,
   right_inv := λ f, ext $ λ a, rfl }
 
+@[simp] lemma dual_id : (bounded_lattice_hom.id α).dual = bounded_lattice_hom.id _ := rfl
+@[simp] lemma dual_comp (g : bounded_lattice_hom β γ) (f : bounded_lattice_hom α β) :
+  (g.comp f).dual = g.dual.comp f.dual := rfl
+
+@[simp] lemma symm_dual_id :
+  bounded_lattice_hom.dual.symm (bounded_lattice_hom.id _) = bounded_lattice_hom.id α := rfl
+@[simp] lemma symm_dual_comp (g : bounded_lattice_hom (order_dual β) (order_dual γ))
+  (f : bounded_lattice_hom (order_dual α) (order_dual β)) :
+  bounded_lattice_hom.dual.symm (g.comp f) =
+    (bounded_lattice_hom.dual.symm g).comp (bounded_lattice_hom.dual.symm f) := rfl
+
 end bounded_lattice_hom