feat(order/hom/*): more superclass instances for order_iso_class (#12889)

 * Weaken hypotheses on `order_hom_class` and some subclasses
 * Add more instances deriving specific order hom classes from `order_iso_class`

Author: YaelDillies

src/order/hom/basic.lean

@@ -93,7 +93,7 @@ abbreviation order_iso (α β : Type*) [has_le α] [has_le β] := @rel_iso α β
 infix ` ≃o `:25 := order_iso
 
 /-- `order_hom_class F α b` asserts that `F` is a type of `≤`-preserving morphisms. -/
-abbreviation order_hom_class (F : Type*) (α β : out_param Type*) [preorder α] [preorder β] :=
+abbreviation order_hom_class (F : Type*) (α β : out_param Type*) [has_le α] [has_le β] :=
 rel_hom_class F ((≤) : α → α → Prop) ((≤) : β → β → Prop)
 
 /-- `order_iso_class F α β` states that `F` is a type of order isomorphisms.
@@ -111,7 +111,7 @@ instance [has_le α] [has_le β] [order_iso_class F α β] : has_coe_t F (α ≃
 ⟨λ f, ⟨f, λ _ _, map_le_map_iff f⟩⟩
 
 @[priority 100] -- See note [lower instance priority]
-instance order_iso_class.to_order_hom_class [preorder α] [preorder β] [order_iso_class F α β] :
+instance order_iso_class.to_order_hom_class [has_le α] [has_le β] [order_iso_class F α β] :
   order_hom_class F α β :=
 { map_rel := λ f a b, (map_le_map_iff f).2, ..equiv_like.to_embedding_like }
 

src/order/hom/bounded.lean

@@ -65,7 +65,7 @@ class bot_hom_class (F : Type*) (α β : out_param $ Type*) [has_bot α] [has_bo
 /-- `bounded_order_hom_class F α β` states that `F` is a type of bounded order morphisms.
 
 You should extend this class when you extend `bounded_order_hom`. -/
-class bounded_order_hom_class (F : Type*) (α β : out_param $ Type*) [preorder α] [preorder β]
+class bounded_order_hom_class (F : Type*) (α β : out_param $ Type*) [has_le α] [has_le β]
   [bounded_order α] [bounded_order β]
   extends rel_hom_class F ((≤) : α → α → Prop) ((≤) : β → β → Prop) :=
 (map_top (f : F) : f ⊤ = ⊤)
@@ -76,32 +76,34 @@ export top_hom_class (map_top) bot_hom_class (map_bot)
 attribute [simp] map_top map_bot
 
 @[priority 100] -- See note [lower instance priority]
-instance bounded_order_hom_class.to_top_hom_class [preorder α] [preorder β]
+instance bounded_order_hom_class.to_top_hom_class [has_le α] [has_le β]
   [bounded_order α] [bounded_order β] [bounded_order_hom_class F α β] :
   top_hom_class F α β :=
 { .. ‹bounded_order_hom_class F α β› }
 
 @[priority 100] -- See note [lower instance priority]
-instance bounded_order_hom_class.to_bot_hom_class [preorder α] [preorder β]
+instance bounded_order_hom_class.to_bot_hom_class [has_le α] [has_le β]
   [bounded_order α] [bounded_order β] [bounded_order_hom_class F α β] :
   bot_hom_class F α β :=
 { .. ‹bounded_order_hom_class F α β› }
 
 @[priority 100] -- See note [lower instance priority]
-instance order_iso.top_hom_class [partial_order α] [partial_order β] [order_top α] [order_top β] :
-  top_hom_class (α ≃o β) α β :=
-{ map_top := λ f, f.map_top, ..rel_iso.rel_hom_class }
+instance order_iso_class.to_top_hom_class [has_le α] [order_top α] [partial_order β] [order_top β]
+  [order_iso_class F α β] :
+  top_hom_class F α β :=
+⟨λ f, top_le_iff.1 $ (map_inv_le_iff f).1 le_top⟩
 
 @[priority 100] -- See note [lower instance priority]
-instance order_iso.bot_hom_class [partial_order α] [partial_order β] [order_bot α] [order_bot β] :
-  bot_hom_class (α ≃o β) α β :=
-{ map_bot := λ f, f.map_bot, ..rel_iso.rel_hom_class }
+instance order_iso_class.to_bot_hom_class [has_le α] [order_bot α] [partial_order β] [order_bot β]
+  [order_iso_class F α β] :
+  bot_hom_class F α β :=
+⟨λ f, le_bot_iff.1 $ (le_map_inv_iff f).1 bot_le⟩
 
 @[priority 100] -- See note [lower instance priority]
-instance order_iso.bounded_order_hom_class [partial_order α] [partial_order β]
-  [bounded_order α] [bounded_order β] :
-  bounded_order_hom_class (α ≃o β) α β :=
-{ ..order_iso.top_hom_class, ..order_iso.bot_hom_class }
+instance order_iso_class.to_bounded_order_hom_class [has_le α] [bounded_order α] [partial_order β]
+  [bounded_order β] [order_iso_class F α β] :
+  bounded_order_hom_class F α β :=
+{ ..order_iso_class.to_top_hom_class, ..order_iso_class.to_bot_hom_class }
 
 instance [has_top α] [has_top β] [top_hom_class F α β] : has_coe_t F (top_hom α β) :=
 ⟨λ f, ⟨f, map_top f⟩⟩

src/order/hom/complete_lattice.lean

@@ -142,11 +142,22 @@ instance complete_lattice_hom_class.to_bounded_lattice_hom_class [complete_latti
 { ..Sup_hom_class.to_sup_bot_hom_class, ..Inf_hom_class.to_inf_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 order_iso_class.to_Sup_hom_class [complete_lattice α] [complete_lattice β]
+  [order_iso_class F α β] :
+  Sup_hom_class F α β :=
+⟨λ f s, eq_of_forall_ge_iff $ λ c, by simp only [←le_map_inv_iff, Sup_le_iff, set.ball_image_iff]⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_iso_class.to_Inf_hom_class [complete_lattice α] [complete_lattice β]
+  [order_iso_class F α β] :
+  Inf_hom_class F α β :=
+⟨λ f s, eq_of_forall_le_iff $ λ c, by simp only [←map_inv_le_iff, le_Inf_iff, set.ball_image_iff]⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_iso_class.to_complete_lattice_hom_class [complete_lattice α] [complete_lattice β]
+  [order_iso_class F α β] :
+  complete_lattice_hom_class F α β :=
+{ ..order_iso_class.to_Sup_hom_class, ..order_iso_class.to_lattice_hom_class }
 
 instance [has_Sup α] [has_Sup β] [Sup_hom_class F α β] : has_coe_t F (Sup_hom α β) :=
 ⟨λ f, ⟨f, map_Sup f⟩⟩

src/order/hom/lattice.lean

@@ -168,24 +168,39 @@ instance bounded_lattice_hom_class.to_bounded_order_hom_class [lattice α] [latt
 { .. ‹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 }
+instance order_iso_class.to_sup_hom_class [semilattice_sup α] [semilattice_sup β]
+  [order_iso_class F α β] :
+  sup_hom_class F α β :=
+⟨λ f a b, eq_of_forall_ge_iff $ λ c, by simp only [←le_map_inv_iff, sup_le_iff]⟩
 
 @[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 }
+instance order_iso_class.to_inf_hom_class [semilattice_inf α] [semilattice_inf β]
+  [order_iso_class F α β] :
+  inf_hom_class F α β :=
+⟨λ f a b, eq_of_forall_le_iff $ λ c, by simp only [←map_inv_le_iff, le_inf_iff]⟩
+
+@[priority 100] -- See note [lower instance priority]
+instance order_iso_class.to_sup_bot_hom_class [semilattice_sup α] [order_bot α] [semilattice_sup β]
+  [order_bot β] [order_iso_class F α β] :
+  sup_bot_hom_class F α β :=
+{ ..order_iso_class.to_sup_hom_class, ..order_iso_class.to_bot_hom_class }
+
+@[priority 100] -- See note [lower instance priority]
+instance order_iso_class.to_inf_top_hom_class [semilattice_inf α] [order_top α] [semilattice_inf β]
+  [order_top β] [order_iso_class F α β] :
+  inf_top_hom_class F α β :=
+{ ..order_iso_class.to_inf_hom_class, ..order_iso_class.to_top_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 order_iso_class.to_lattice_hom_class [lattice α] [lattice β] [order_iso_class F α β] :
+  lattice_hom_class F α β :=
+{ ..order_iso_class.to_sup_hom_class, ..order_iso_class.to_inf_hom_class }
 
 @[priority 100] -- See note [lower instance priority]
-instance order_iso.bounded_lattice_hom_class [lattice α] [lattice β] [bounded_order α]
-  [bounded_order β] :
-  bounded_lattice_hom_class (α ≃o β) α β :=
-{ ..order_iso.lattice_hom_class, ..order_iso.bounded_order_hom_class }
+instance order_iso_class.to_bounded_lattice_hom_class [lattice α] [lattice β] [bounded_order α]
+  [bounded_order β] [order_iso_class F α β] :
+  bounded_lattice_hom_class F α β :=
+{ ..order_iso_class.to_lattice_hom_class, ..order_iso_class.to_bounded_order_hom_class }
 
 @[simp] lemma map_finset_sup [semilattice_sup α] [order_bot α] [semilattice_sup β] [order_bot β]
   [sup_bot_hom_class F α β] (f : F) (s : finset ι) (g : ι → α) :