feat(order/rel_iso): a new definition of order_iso, using preorder in…

…stances (#3838)

defines (new) `order_embedding` and `order_iso`, which map both < and <=
replaces existing `rel_embedding` and `rel_iso` instances preserving < or <= with the new abbreviations

src/data/finsupp/lattice.lean

@@ -88,29 +88,29 @@ begin
 end
 
 /-- The lattice of `finsupp`s to `ℕ` is order-isomorphic to that of `multiset`s.  -/
-def rel_iso_multiset :
-  (has_le.le : (α →₀ ℕ) → (α →₀ ℕ) → Prop) ≃r (has_le.le : (multiset α) → (multiset α) → Prop) :=
+def order_iso_multiset :
+  (α →₀ ℕ) ≃o multiset α :=
 ⟨finsupp.equiv_multiset, begin
   intros a b, unfold finsupp.equiv_multiset, dsimp,
   rw multiset.le_iff_count, simp only [finsupp.count_to_multiset], refl
 end ⟩
 
-@[simp] lemma rel_iso_multiset_apply {f : α →₀ ℕ} : rel_iso_multiset f = f.to_multiset := rfl
+@[simp] lemma order_iso_multiset_apply {f : α →₀ ℕ} : order_iso_multiset f = f.to_multiset := rfl
 
-@[simp] lemma rel_iso_multiset_symm_apply {s : multiset α} :
-  rel_iso_multiset.symm s = s.to_finsupp :=
-by { conv_rhs { rw ← (rel_iso.apply_symm_apply rel_iso_multiset) s}, simp }
+@[simp] lemma order_iso_multiset_symm_apply {s : multiset α} :
+  order_iso_multiset.symm s = s.to_finsupp :=
+by { conv_rhs { rw ← (rel_iso.apply_symm_apply order_iso_multiset) s}, simp }
 
 variable [partial_order β]
 
 /-- The order on `finsupp`s over a partial order embeds into the order on functions -/
-def rel_embedding_to_fun :
-  (has_le.le : (α →₀ β) → (α →₀ β) → Prop) ↪r (has_le.le : (α → β) → (α → β) → Prop) :=
+def order_embedding_to_fun :
+  (α →₀ β) ↪o (α → β) :=
 ⟨⟨λ (f : α →₀ β) (a : α), f a,  λ f g h, finsupp.ext (λ a, by { dsimp at h, rw h,} )⟩,
   λ a b, le_def⟩
 
-@[simp] lemma rel_embedding_to_fun_apply {f : α →₀ β} {a : α} :
-  rel_embedding_to_fun f a = f a := rfl
+@[simp] lemma order_embedding_to_fun_apply {f : α →₀ β} {a : α} :
+  order_embedding_to_fun f a = f a := rfl
 
 lemma monotone_to_fun : monotone (finsupp.to_fun : (α →₀ β) → (α → β)) := λ f g h a, le_def.1 h a
 

src/data/setoid/basic.lean

@@ -317,8 +317,7 @@ open quotient
 
 /-- Given an equivalence relation r on α, the order-preserving bijection between the set of
     equivalence relations containing r and the equivalence relations on the quotient of α by r. -/
-def correspondence (r : setoid α) : ((≤) : {s // r ≤ s} → {s // r ≤ s} → Prop) ≃r
-  ((≤) : setoid (quotient r) → setoid (quotient r) → Prop) :=
+def correspondence (r : setoid α) : {s // r ≤ s} ≃o setoid (quotient r) :=
 { to_fun := λ s, map_of_surjective s.1 quotient.mk ((ker_mk_eq r).symm ▸ s.2) exists_rep,
   inv_fun := λ s, ⟨comap quotient.mk s, λ x y h, show s.rel ⟦x⟧ ⟦y⟧, by rw eq_rel.2 h⟩,
   left_inv := λ s, subtype.ext_iff_val.2 $ ext' $ λ _ _,

src/data/setoid/partition.lean

@@ -176,7 +176,7 @@ variables (α)
 
 /-- The order-preserving bijection between equivalence relations and partitions of sets. -/
 def partition.rel_iso :
-  ((≤) : setoid α → setoid α → Prop) ≃r (@setoid.partition.partial_order α).le :=
+  setoid α ≃o subtype (@is_partition α) :=
 { to_fun := λ r, ⟨r.classes, empty_not_mem_classes, classes_eqv_classes⟩,
   inv_fun := λ x, mk_classes x.1 x.2.2,
   left_inv := mk_classes_classes,

src/group_theory/congruence.lean

@@ -516,8 +516,7 @@ open quotient
 @[to_additive "Given an additive congruence relation `c` on a type `M` with an addition,
 the order-preserving bijection between the set of additive congruence relations containing `c` and
 the additive congruence relations on the quotient of `M` by `c`."]
-def correspondence : ((≤) : {d // c ≤ d} → {d // c ≤ d} → Prop) ≃r
-  ((≤) : con c.quotient → con c.quotient → Prop) :=
+def correspondence : {d // c ≤ d} ≃o (con c.quotient) :=
 { to_fun := λ d, d.1.map_of_surjective coe _
     (by rw mul_ker_mk_eq; exact d.2) $ @exists_rep _ c.to_setoid,
   inv_fun := λ d, ⟨comap (coe : M → c.quotient) (λ x y, rfl) d, λ _ _ h,

src/linear_algebra/basic.lean

@@ -1432,8 +1432,7 @@ by rw [eq_bot_iff, ← map_le_map_iff' p.ker_subtype, map_bot, map_comap_subtype
 
 /-- If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N` -/
 def map_subtype.rel_iso :
-  ((≤) : submodule R p → submodule R p → Prop) ≃r
-  ((≤) : {p' : submodule R M // p' ≤ p} → {p' : submodule R M // p' ≤ p} → Prop) :=
+  submodule R p ≃o {p' : submodule R M // p' ≤ p} :=
 { to_fun    := λ p', ⟨map p.subtype p', map_subtype_le p _⟩,
   inv_fun   := λ q, comap p.subtype q,
   left_inv  := λ p', comap_map_eq_self $ by simp,
@@ -1442,18 +1441,12 @@ def map_subtype.rel_iso :
 
 /-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
 submodules of `M`. -/
-def map_subtype.le_rel_embedding :
-  ((≤) : submodule R p → submodule R p → Prop) ↪r ((≤) : submodule R M → submodule R M → Prop) :=
+def map_subtype.order_embedding :
+  submodule R p ↪o submodule R M :=
 (rel_iso.to_rel_embedding $ map_subtype.rel_iso p).trans (subtype.rel_embedding _ _)
 
 @[simp] lemma map_subtype_embedding_eq (p' : submodule R p) :
-  map_subtype.le_rel_embedding p p' = map p.subtype p' := rfl
-
-/-- If `p ⊆ M` is a submodule, the ordering of submodules of `p` is embedded in the ordering of
-submodules of `M`. -/
-def map_subtype.lt_rel_embedding :
-  ((<) : submodule R p → submodule R p → Prop) ↪r ((<) : submodule R M → submodule R M → Prop) :=
-(map_subtype.le_rel_embedding p).lt_embedding_of_le_embedding
+  map_subtype.order_embedding p p' = map p.subtype p' := rfl
 
 
 /-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
@@ -1528,8 +1521,7 @@ by rw [ker_liftq, le_antisymm h h', mkq_map_self]
 /-- The correspondence theorem for modules: there is an order isomorphism between submodules of the
 quotient of `M` by `p`, and submodules of `M` larger than `p`. -/
 def comap_mkq.rel_iso :
-  ((≤) : submodule R p.quotient → submodule R p.quotient → Prop) ≃r
-  ((≤) : {p' : submodule R M // p ≤ p'} → {p' : submodule R M // p ≤ p'} → Prop) :=
+  submodule R p.quotient ≃o {p' : submodule R M // p ≤ p'} :=
 { to_fun    := λ p', ⟨comap p.mkq p', le_comap_mkq p _⟩,
   inv_fun   := λ q, map p.mkq q,
   left_inv  := λ p', map_comap_eq_self $ by simp,
@@ -1538,18 +1530,12 @@ def comap_mkq.rel_iso :
 
 /-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
 of `M`. -/
-def comap_mkq.le_rel_embedding :
-  ((≤) : submodule R p.quotient → submodule R p.quotient → Prop) ↪r ((≤) : submodule R M → submodule R M → Prop) :=
+def comap_mkq.order_embedding :
+  submodule R p.quotient ↪o submodule R M :=
 (rel_iso.to_rel_embedding $ comap_mkq.rel_iso p).trans (subtype.rel_embedding _ _)
 
 @[simp] lemma comap_mkq_embedding_eq (p' : submodule R p.quotient) :
-  comap_mkq.le_rel_embedding p p' = comap p.mkq p' := rfl
-
-/-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
-of `M`. -/
-def comap_mkq.lt_rel_embedding :
-  ((<) : submodule R p.quotient → submodule R p.quotient → Prop) ↪r ((<) : submodule R M → submodule R M → Prop) :=
-(comap_mkq.le_rel_embedding p).lt_embedding_of_le_embedding
+  comap_mkq.order_embedding p p' = comap p.mkq p' := rfl
 
 end ring
 

src/order/basic.lean

@@ -77,9 +77,9 @@ theorem linear_order.ext {α} {A B : linear_order α}
 by { haveI this := partial_order.ext H,
      casesI A, casesI B, injection this, congr' }
 
-/-- Given an order `R` on `β` and a function `f : α → β`,
-  the preimage order on `α` is defined by `x ≤ y ↔ f x ≤ f y`.
-  It is the unique order on `α` making `f` an order embedding
+/-- Given a relation `R` on `β` and a function `f : α → β`,
+  the preimage relation on `α` is defined by `x ≤ y ↔ f x ≤ f y`.
+  It is the unique relation on `α` making `f` a `rel_embedding`
   (assuming `f` is injective). -/
 @[simp] def order.preimage {α β} (f : α → β) (s : β → β → Prop) (x y : α) := s (f x) (f y)
 

src/order/galois_connection.lean

@@ -54,9 +54,9 @@ variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a a₁ a₂ :
 def galois_connection [preorder α] [preorder β] (l : α → β) (u : β → α) := ∀a b, l a ≤ b ↔ a ≤ u b
 
 /-- Makes a Galois connection from an order-preserving bijection. -/
-theorem rel_iso.to_galois_connection [preorder α] [preorder β] (ri : @rel_iso α β (≤) (≤)) :
-  galois_connection ri ri.symm :=
-λ b g, by rw [ri.map_rel_iff, rel_iso.apply_symm_apply]
+theorem order_iso.to_galois_connection [preorder α] [preorder β] (oi : α ≃o β) :
+  galois_connection oi oi.symm :=
+λ b g, by rw [oi.map_rel_iff, rel_iso.apply_symm_apply]
 
 namespace galois_connection
 
@@ -241,7 +241,7 @@ def galois_insertion.monotone_intro {α β : Type*} [preorder α] [preorder β]
   choice_eq := λ _ _, rfl }
 
 /-- Makes a Galois insertion from an order-preserving bijection. -/
-protected def rel_iso.to_galois_insertion [preorder α] [preorder β] (oi : @rel_iso α β (≤) (≤)) :
+protected def rel_iso.to_galois_insertion [preorder α] [preorder β] (oi : α ≃o β) :
 @galois_insertion α β _ _ (oi) (oi.symm) :=
 { choice := λ b h, oi b,
   gc := oi.to_galois_connection,
@@ -411,7 +411,7 @@ def galois_insertion.of_dual {α β : Type*} [preorder α] [preorder β] {l : α
 λ x, ⟨x.1, x.2.dual, x.3, x.4⟩
 
 /-- Makes a Galois coinsertion from an order-preserving bijection. -/
-protected def rel_iso.to_galois_coinsertion [preorder α] [preorder β] (oi : @rel_iso α β (≤) (≤)) :
+protected def rel_iso.to_galois_coinsertion [preorder α] [preorder β] (oi : α ≃o β) :
 @galois_coinsertion α β _ _ (oi) (oi.symm) :=
 { choice := λ b h, oi.symm b,
   gc := oi.to_galois_connection,

src/order/ord_continuous.lean

@@ -91,23 +91,15 @@ by simp only [lt_iff_le_not_le, hf.le_iff h]
 
 variable (f)
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_le_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ((≤) : α → α → Prop) ↪r ((≤) : β → β → Prop) :=
+/-- Convert an injective left order continuous function to an order embedding. -/
+def to_order_embedding (hf : left_ord_continuous f) (h : injective f) :
+  α ↪o β :=
 ⟨⟨f, h⟩, λ x y, (hf.le_iff h).symm⟩
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_lt_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ((<) : α → α → Prop) ↪r ((<) : β → β → Prop) :=
-⟨⟨f, h⟩, λ x y, (hf.lt_iff h).symm⟩
-
 variable {f}
 
-@[simp] lemma coe_to_le_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_le_rel_embedding f h) = f := rfl
-
-@[simp] lemma coe_to_lt_rel_embedding (hf : left_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_lt_rel_embedding f h) = f := rfl
+@[simp] lemma coe_to_order_embedding (hf : left_ord_continuous f) (h : injective f) :
+  ⇑(hf.to_order_embedding f h) = f := rfl
 
 end semilattice_sup
 
@@ -194,23 +186,14 @@ hf.order_dual.lt_iff h
 
 variable (f)
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_le_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ((≤) : α → α → Prop) ↪r ((≤) : β → β → Prop) :=
+/-- Convert an injective left order continuous function to a `order_embedding`. -/
+def to_order_embedding (hf : right_ord_continuous f) (h : injective f) : α ↪o β :=
 ⟨⟨f, h⟩, λ x y, (hf.le_iff h).symm⟩
 
-/-- Convert an injective left order continuous function to an order embeddings. -/
-def to_lt_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ((<) : α → α → Prop) ↪r ((<) : β → β → Prop) :=
-⟨⟨f, h⟩, λ x y, (hf.lt_iff h).symm⟩
-
 variable {f}
 
-@[simp] lemma coe_to_le_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_le_rel_embedding f h) = f := rfl
-
-@[simp] lemma coe_to_lt_rel_embedding (hf : right_ord_continuous f) (h : injective f) :
-  ⇑(hf.to_lt_rel_embedding f h) = f := rfl
+@[simp] lemma coe_to_order_embedding (hf : right_ord_continuous f) (h : injective f) :
+  ⇑(hf.to_order_embedding f h) = f := rfl
 
 end semilattice_inf
 
@@ -249,11 +232,11 @@ end conditionally_complete_lattice
 
 end right_ord_continuous
 
-namespace rel_iso
+namespace order_iso
 
 section preorder
 
-variables [preorder α] [preorder β] (e : ((≤) : α → α → Prop) ≃r ((≤) : β → β → Prop))
+variables [preorder α] [preorder β] (e : α ≃o β)
   {s : set α} {x : α}
 
 protected lemma left_ord_continuous : left_ord_continuous e :=
@@ -262,9 +245,8 @@ protected lemma left_ord_continuous : left_ord_continuous e :=
   λ y hy, e.rel_symm_apply.1 $ (is_lub_le_iff hx).2 $ λ x' hx', e.rel_symm_apply.2 $ hy $
     mem_image_of_mem _ hx'⟩
 
-protected lemma right_ord_continuous : right_ord_continuous e :=
-@rel_iso.left_ord_continuous (order_dual α) (order_dual β) _ _ e.rsymm
+protected lemma right_ord_continuous : right_ord_continuous e := order_iso.left_ord_continuous e.osymm
 
 end preorder
 
-end rel_iso
+end order_iso