chore(order/rel_iso): rename order_iso and order_embedding to rel_iso…

… and rel_embedding (#3750)

renames `order_iso` and `order_embedding`, to make it clear they apply to all binary relations
makes room for a new definition of `order_embedding` that will deal with order instances

scripts/nolints.txt

@@ -1299,20 +1299,20 @@ apply_nolint fixed_points.prev_fixed doc_blame
 -- order/lexicographic.lean
 apply_nolint lex doc_blame
 
--- order/order_iso.lean
-apply_nolint order_embedding has_inhabited_instance
-apply_nolint order_embedding.lt_embedding_of_le_embedding doc_blame
-apply_nolint order_embedding.refl doc_blame
-apply_nolint order_embedding.trans doc_blame
-apply_nolint order_iso has_inhabited_instance
-apply_nolint order_iso.prod_lex_congr doc_blame
-apply_nolint order_iso.sum_lex_congr doc_blame
-apply_nolint subrel.order_embedding doc_blame
+-- order/rel_iso.lean
+apply_nolint rel_embedding has_inhabited_instance
+apply_nolint rel_embedding.lt_embedding_of_le_embedding doc_blame
+apply_nolint rel_embedding.refl doc_blame
+apply_nolint rel_embedding.trans doc_blame
+apply_nolint rel_iso has_inhabited_instance
+apply_nolint rel_iso.prod_lex_congr doc_blame
+apply_nolint rel_iso.sum_lex_congr doc_blame
+apply_nolint subrel.rel_embedding doc_blame
 
 -- order/order_iso_nat.lean
-apply_nolint order_embedding.nat_gt doc_blame ge_or_gt
-apply_nolint order_embedding.nat_lt doc_blame
-apply_nolint order_embedding.well_founded_iff_no_descending_seq ge_or_gt
+apply_nolint rel_embedding.nat_gt doc_blame ge_or_gt
+apply_nolint rel_embedding.nat_lt doc_blame
+apply_nolint rel_embedding.well_founded_iff_no_descending_seq ge_or_gt
 
 -- order/pilex.lean
 apply_nolint pi.lex doc_blame
@@ -1338,8 +1338,8 @@ apply_nolint free_ring.map doc_blame
 apply_nolint free_ring.of doc_blame
 
 -- ring_theory/ideal/operations.lean
-apply_nolint ideal.le_order_embedding_of_surjective doc_blame
-apply_nolint ideal.lt_order_embedding_of_surjective doc_blame
+apply_nolint ideal.le_rel_embedding_of_surjective doc_blame
+apply_nolint ideal.lt_rel_embedding_of_surjective doc_blame
 apply_nolint ideal.map doc_blame
 apply_nolint ideal.quotient_inf_to_pi_quotient doc_blame
 apply_nolint submodule.annihilator doc_blame
@@ -2057,4 +2057,4 @@ apply_nolint uniform_space.completion.map₂ doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/data/equiv/encodable/basic.lean

@@ -7,7 +7,7 @@ Type class for encodable Types.
 Note that every encodable Type is countable.
 -/
 import data.equiv.nat
-import order.order_iso
+import order.rel_iso
 import order.directed
 
 open option list nat function
@@ -358,11 +358,11 @@ def encode' (α) [encodable α] : α ↪ nat :=
 ⟨encodable.encode, encodable.encode_injective⟩
 
 instance {α} [encodable α] : is_trans _ (encode' α ⁻¹'o (≤)) :=
-(order_embedding.preimage _ _).is_trans
+(rel_embedding.preimage _ _).is_trans
 instance {α} [encodable α] : is_antisymm _ (encodable.encode' α ⁻¹'o (≤)) :=
-(order_embedding.preimage _ _).is_antisymm
+(rel_embedding.preimage _ _).is_antisymm
 instance {α} [encodable α] : is_total _ (encodable.encode' α ⁻¹'o (≤)) :=
-(order_embedding.preimage _ _).is_total
+(rel_embedding.preimage _ _).is_total
 
 end encodable
 

src/data/equiv/list.lean

@@ -59,7 +59,7 @@ variables [encodable α]
 private def enle : α → α → Prop := encode ⁻¹'o (≤)
 
 private lemma enle.is_linear_order : is_linear_order α enle :=
-(order_embedding.preimage ⟨encode, encode_injective⟩ (≤)).is_linear_order
+(rel_embedding.preimage ⟨encode, encode_injective⟩ (≤)).is_linear_order
 
 private def decidable_enle (a b : α) : decidable (enle a b) :=
 by unfold enle order.preimage; apply_instance

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 order_iso_multiset :
-  (has_le.le : (α →₀ ℕ) → (α →₀ ℕ) → Prop) ≃o (has_le.le : (multiset α) → (multiset α) → Prop) :=
+def rel_iso_multiset :
+  (has_le.le : (α →₀ ℕ) → (α →₀ ℕ) → Prop) ≃r (has_le.le : (multiset α) → (multiset α) → Prop) :=
 ⟨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 order_iso_multiset_apply {f : α →₀ ℕ} : order_iso_multiset f = f.to_multiset := rfl
+@[simp] lemma rel_iso_multiset_apply {f : α →₀ ℕ} : rel_iso_multiset f = f.to_multiset := rfl
 
-@[simp] lemma order_iso_multiset_symm_apply {s : multiset α} :
-  order_iso_multiset.symm s = s.to_finsupp :=
-by { conv_rhs { rw ← (order_iso.apply_symm_apply order_iso_multiset) s}, simp }
+@[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 }
 
 variable [partial_order β]
 
 /-- The order on `finsupp`s over a partial order embeds into the order on functions -/
-def order_embedding_to_fun :
-  (has_le.le : (α →₀ β) → (α →₀ β) → Prop) ≼o (has_le.le : (α → β) → (α → β) → Prop) :=
+def rel_embedding_to_fun :
+  (has_le.le : (α →₀ β) → (α →₀ β) → Prop) ↪r (has_le.le : (α → β) → (α → β) → Prop) :=
 ⟨⟨λ (f : α →₀ β) (a : α), f a,  λ f g h, finsupp.ext (λ a, by { dsimp at h, rw h,} )⟩,
   λ a b, le_def⟩
 
-@[simp] lemma order_embedding_to_fun_apply {f : α →₀ β} {a : α} :
-  order_embedding_to_fun f a = f a := rfl
+@[simp] lemma rel_embedding_to_fun_apply {f : α →₀ β} {a : α} :
+  rel_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,7 +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) ≃o
+def correspondence (r : setoid α) : ((≤) : {s // r ≤ s} → {s // r ≤ s} → Prop) ≃r
   ((≤) : setoid (quotient r) → setoid (quotient r) → Prop) :=
 { 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⟩,
@@ -329,7 +329,7 @@ def correspondence (r : setoid α) : ((≤) : {s // r ≤ s} → {s // r ≤ s}
       λ x y h, show s.rel ⟦x⟧ ⟦y⟧, by rw (@eq_rel _ r x y).2 ((ker_mk_eq r) ▸ h) in
     ext' $ λ x y, ⟨λ h, let ⟨a, b, hx, hy, H⟩ := h in hx ▸ hy ▸ H,
       quotient.induction_on₂ x y $ λ w z h, ⟨w, z, rfl, rfl, h⟩⟩,
-  ord' := λ s t, ⟨λ h x y hs, let ⟨a, b, hx, hy, Hs⟩ := hs in ⟨a, b, hx, hy, h Hs⟩,
+  map_rel_iff' := λ s t, ⟨λ h x y hs, let ⟨a, b, hx, hy, Hs⟩ := hs in ⟨a, b, hx, hy, h Hs⟩,
     λ h x y hs, let ⟨a, b, hx, hy, ht⟩ := h ⟨x, y, rfl, rfl, hs⟩ in
       t.1.trans' (t.1.symm' $ t.2 $ eq_rel.1 hx) $ t.1.trans' ht $ t.2 $ eq_rel.1 hy⟩ }
 

src/data/setoid/partition.lean

@@ -175,21 +175,21 @@ instance partition.partial_order : partial_order (subtype (@is_partition α)) :=
 variables (α)
 
 /-- The order-preserving bijection between equivalence relations and partitions of sets. -/
-def partition.order_iso :
-  ((≤) : setoid α → setoid α → Prop) ≃o (@setoid.partition.partial_order α).le :=
+def partition.rel_iso :
+  ((≤) : setoid α → setoid α → Prop) ≃r (@setoid.partition.partial_order α).le :=
 { 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,
   right_inv := λ x, by rw [subtype.ext_iff_val, ←classes_mk_classes x.1 x.2],
-  ord' := λ x y, by conv {to_lhs, rw [←mk_classes_classes x, ←mk_classes_classes y]}; refl }
+  map_rel_iff' := λ x y, by conv {to_lhs, rw [←mk_classes_classes x, ←mk_classes_classes y]}; refl }
 
 variables {α}
 
 /-- A complete lattice instance for partitions; there is more infrastructure for the
     equivalent complete lattice on equivalence relations. -/
 instance partition.complete_lattice : complete_lattice (subtype (@is_partition α)) :=
-galois_insertion.lift_complete_lattice $ @order_iso.to_galois_insertion
-_ (subtype (@is_partition α)) _ (partial_order.to_preorder _) $ partition.order_iso α
+galois_insertion.lift_complete_lattice $ @rel_iso.to_galois_insertion
+_ (subtype (@is_partition α)) _ (partial_order.to_preorder _) $ partition.rel_iso α
 
 end partition
 

src/group_theory/congruence.lean

@@ -516,7 +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) ≃o
+def correspondence : ((≤) : {d // c ≤ d} → {d // c ≤ d} → Prop) ≃r
   ((≤) : con c.quotient → con c.quotient → Prop) :=
 { to_fun := λ d, d.1.map_of_surjective coe _
     (by rw mul_ker_mk_eq; exact d.2) $ @exists_rep _ c.to_setoid,
@@ -531,7 +531,7 @@ def correspondence : ((≤) : {d // c ≤ d} → {d // c ≤ d} → Prop) ≃o
       λ x y h, show d _ _, by rw mul_ker_mk_eq at h; exact c.eq.2 h ▸ d.refl _ in
     ext $ λ x y, ⟨λ h, let ⟨a, b, hx, hy, H⟩ := h in hx ▸ hy ▸ H,
       con.induction_on₂ x y $ λ w z h, ⟨w, z, rfl, rfl, h⟩⟩,
-  ord' := λ s t, ⟨λ h _ _ hs, let ⟨a, b, hx, hy, Hs⟩ := hs in ⟨a, b, hx, hy, h Hs⟩,
+  map_rel_iff' := λ s t, ⟨λ h _ _ hs, let ⟨a, b, hx, hy, Hs⟩ := hs in ⟨a, b, hx, hy, h Hs⟩,
     λ h _ _ hs, let ⟨a, b, hx, hy, ht⟩ := h ⟨_, _, rfl, rfl, hs⟩ in
       t.1.trans (t.1.symm $ t.2 $ eq_rel.1 hx) $ t.1.trans ht $ t.2 $ eq_rel.1 hy⟩ }
 

src/linear_algebra/basic.lean

@@ -1431,29 +1431,29 @@ lemma disjoint_iff_comap_eq_bot {p q : submodule R M} :
 by rw [eq_bot_iff, ← map_le_map_iff' p.ker_subtype, map_bot, map_comap_subtype, disjoint]
 
 /-- If `N ⊆ M` then submodules of `N` are the same as submodules of `M` contained in `N` -/
-def map_subtype.order_iso :
-  ((≤) : submodule R p → submodule R p → Prop) ≃o
+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) :=
 { 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,
   right_inv := λ ⟨q, hq⟩, subtype.ext_val $ by simp [map_comap_subtype p, inf_of_le_right hq],
-  ord'      := λ p₁ p₂, (map_le_map_iff' (ker_subtype p)).symm }
+  map_rel_iff'      := λ p₁ p₂, (map_le_map_iff' (ker_subtype p)).symm }
 
 /-- 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_order_embedding :
-  ((≤) : submodule R p → submodule R p → Prop) ≼o ((≤) : submodule R M → submodule R M → Prop) :=
-(order_iso.to_order_embedding $ map_subtype.order_iso p).trans (subtype.order_embedding _ _)
+def map_subtype.le_rel_embedding :
+  ((≤) : submodule R p → submodule R p → Prop) ↪r ((≤) : submodule R M → submodule R M → Prop) :=
+(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_order_embedding p p' = map p.subtype p' := rfl
+  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_order_embedding :
-  ((<) : submodule R p → submodule R p → Prop) ≼o ((<) : submodule R M → submodule R M → Prop) :=
-(map_subtype.le_order_embedding p).lt_embedding_of_le_embedding
+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
 
 
 /-- The map from a module `M` to the quotient of `M` by a submodule `p` as a linear map. -/
@@ -1527,29 +1527,29 @@ 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.order_iso :
-  ((≤) : submodule R p.quotient → submodule R p.quotient → Prop) ≃o
+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) :=
 { 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,
   right_inv := λ ⟨q, hq⟩, subtype.ext_val $ by simpa [comap_map_mkq p],
-  ord'      := λ p₁ p₂, (comap_le_comap_iff $ range_mkq _).symm }
+  map_rel_iff'      := λ p₁ p₂, (comap_le_comap_iff $ range_mkq _).symm }
 
 /-- The ordering on submodules of the quotient of `M` by `p` embeds into the ordering on submodules
 of `M`. -/
-def comap_mkq.le_order_embedding :
-  ((≤) : submodule R p.quotient → submodule R p.quotient → Prop) ≼o ((≤) : submodule R M → submodule R M → Prop) :=
-(order_iso.to_order_embedding $ comap_mkq.order_iso p).trans (subtype.order_embedding _ _)
+def comap_mkq.le_rel_embedding :
+  ((≤) : submodule R p.quotient → submodule R p.quotient → Prop) ↪r ((≤) : submodule R M → submodule R M → Prop) :=
+(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_order_embedding p p' = comap p.mkq p' := rfl
+  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_order_embedding :
-  ((<) : submodule R p.quotient → submodule R p.quotient → Prop) ≼o ((<) : submodule R M → submodule R M → Prop) :=
-(comap_mkq.le_order_embedding p).lt_embedding_of_le_embedding
+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
 
 end ring
 

src/order/galois_connection.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Johannes Hölzl
 -/
 import order.complete_lattice
-import order.order_iso
+import order.rel_iso
 /-!
 # Galois connections, insertions and coinsertions
 
@@ -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 order_iso.to_galois_connection [preorder α] [preorder β] (oi : @order_iso α β (≤) (≤)) :
-  galois_connection oi oi.symm :=
-λ b g, by rw [oi.ord, order_iso.apply_symm_apply]
+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]
 
 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 order_iso.to_galois_insertion [preorder α] [preorder β] (oi : @order_iso α β (≤) (≤)) :
+protected def rel_iso.to_galois_insertion [preorder α] [preorder β] (oi : @rel_iso α β (≤) (≤)) :
 @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 order_iso.to_galois_coinsertion [preorder α] [preorder β] (oi : @order_iso α β (≤) (≤)) :
+protected def rel_iso.to_galois_coinsertion [preorder α] [preorder β] (oi : @rel_iso α β (≤) (≤)) :
 @galois_coinsertion α β _ _ (oi) (oi.symm) :=
 { choice := λ b h, oi.symm b,
   gc := oi.to_galois_connection,