From 6bcb12c1ecbf061f5b8f1616cc089be4817164a3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 16 Feb 2022 17:16:25 +0000
Subject: [PATCH] feat(order/antisymmetrization): Turning a preorder into a
 partial order (#11728)

Define `antisymmetrization`, the quotient of a preorder by the "less than both ways" relation. This effectively turns a preorder into a partial order, and this operation is functorial as shown by the new `Preorder_to_PartialOrder`.
---
 src/data/quot.lean                   |   2 +-
 src/order/antisymmetrization.lean    | 193 +++++++++++++++++++++++++++
 src/order/category/PartialOrder.lean |  33 ++++-
 src/order/rel_classes.lean           |   6 +-
 4 files changed, 230 insertions(+), 4 deletions(-)
 create mode 100644 src/order/antisymmetrization.lean

diff --git a/src/data/quot.lean b/src/data/quot.lean
index 886ca6a9c97cf..1141ddceb8b91 100644
--- a/src/data/quot.lean
+++ b/src/data/quot.lean
@@ -31,7 +31,7 @@ namespace quot
 variables {ra : α → α → Prop} {rb : β → β → Prop} {φ : quot ra → quot rb → Sort*}
 local notation `⟦`:max a `⟧` := quot.mk _ a
 
-instance [inhabited α] : inhabited (quot ra) := ⟨⟦default⟧⟩
+instance (r : α → α → Prop) [inhabited α] : inhabited (quot r) := ⟨⟦default⟧⟩
 
 instance [subsingleton α] : subsingleton (quot ra) :=
 ⟨λ x, quot.induction_on x (λ y, quot.ind (λ b, congr_arg _ (subsingleton.elim _ _)))⟩
diff --git a/src/order/antisymmetrization.lean b/src/order/antisymmetrization.lean
new file mode 100644
index 0000000000000..c32579bc4f4b5
--- /dev/null
+++ b/src/order/antisymmetrization.lean
@@ -0,0 +1,193 @@
+/-
+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.hom.basic
+
+/-!
+# Turning a preorder into a partial order
+
+This file allows to make a preorder into a partial order by quotienting out the elements `a`, `b`
+such that `a ≤ b` and `b ≤ a`.
+
+`antisymmetrization` is a functor from `Preorder` to `PartialOrder`. See `Preorder_to_PartialOrder`.
+
+## Main declarations
+
+* `antisymm_rel`: The antisymmetrization relation. `antisymm_rel r a b` means that `a` and `b` are
+  related both ways by `r`.
+* `antisymmetrization α r`: The quotient of `α` by `antisymm_rel r`. Even when `r` is just a
+  preorder, `antisymmetrization α` is a partial order.
+-/
+
+open function order_dual
+
+variables {α β : Type*}
+
+section relation
+variables (r : α → α → Prop)
+
+/-- The antisymmetrization relation. -/
+def antisymm_rel (a b : α) : Prop := r a b ∧ r b a
+
+lemma antisymm_rel_swap : antisymm_rel (swap r) = antisymm_rel r :=
+funext $ λ _, funext $ λ _, propext and.comm
+
+@[refl] lemma antisymm_rel_refl [is_refl α r] (a : α) : antisymm_rel r a a := ⟨refl _, refl _⟩
+
+variables {r}
+
+@[symm] lemma antisymm_rel.symm {a b : α} : antisymm_rel r a b → antisymm_rel r b a := and.symm
+
+@[trans] lemma antisymm_rel.trans [is_trans α r] {a b c : α} (hab : antisymm_rel r a b)
+  (hbc : antisymm_rel r b c) :
+  antisymm_rel r a c :=
+⟨trans hab.1 hbc.1, trans hbc.2 hab.2⟩
+
+instance antisymm_rel.decidable_rel [decidable_rel r] : decidable_rel (antisymm_rel r) :=
+λ _ _, and.decidable
+
+@[simp] lemma antisymm_rel_iff_eq [is_refl α r] [is_antisymm α r] {a b : α} :
+  antisymm_rel r a b ↔ a = b := antisymm_iff
+
+alias antisymm_rel_iff_eq ↔ antisymm_rel.eq _
+
+end relation
+
+section is_preorder
+variables (α) (r : α → α → Prop) [is_preorder α r]
+
+/-- The antisymmetrization relation as an equivalence relation. -/
+@[simps] def antisymm_rel.setoid : setoid α :=
+⟨antisymm_rel r, antisymm_rel_refl _, λ _ _, antisymm_rel.symm, λ _ _ _, antisymm_rel.trans⟩
+
+/-- The partial order derived from a preorder by making pairwise comparable elements equal. This is
+the quotient by `λ a b, a ≤ b ∧ b ≤ a`. -/
+def antisymmetrization : Type* := quotient $ antisymm_rel.setoid α r
+
+variables {α}
+
+/-- Turn an element into its antisymmetrization. -/
+def to_antisymmetrization : α → antisymmetrization α r := quotient.mk'
+
+/-- Get a representative from the antisymmetrization. -/
+noncomputable def of_antisymmetrization : antisymmetrization α r → α := quotient.out'
+
+instance [inhabited α] : inhabited (antisymmetrization α r) := quotient.inhabited _
+
+@[elab_as_eliminator]
+protected lemma antisymmetrization.ind {p : antisymmetrization α r → Prop} :
+  (∀ a, p $ to_antisymmetrization r a) → ∀ q, p q :=
+quot.ind
+
+@[elab_as_eliminator]
+protected lemma antisymmetrization.induction_on {p : antisymmetrization α r → Prop}
+  (a : antisymmetrization α r) (h : ∀ a, p $ to_antisymmetrization r a) : p a :=
+quotient.induction_on' a h
+
+@[simp] lemma to_antisymmetrization_of_antisymmetrization (a : antisymmetrization α r) :
+  to_antisymmetrization r (of_antisymmetrization r a) = a := quotient.out_eq' _
+
+end is_preorder
+
+section preorder
+variables {α} [preorder α] [preorder β] {a b : α}
+
+lemma antisymm_rel.image {a b : α} (h : antisymm_rel (≤) a b) {f : α → β} (hf : monotone f) :
+  antisymm_rel (≤) (f a) (f b) :=
+⟨hf h.1, hf h.2⟩
+
+instance : partial_order (antisymmetrization α (≤)) :=
+{ le := λ a b, quotient.lift_on₂' a b (≤) $ λ (a₁ a₂ b₁ b₂ : α) h₁ h₂,
+    propext ⟨λ h, h₁.2.trans $ h.trans h₂.1, λ h, h₁.1.trans $ h.trans h₂.2⟩,
+  lt := λ a b, quotient.lift_on₂' a b (<) $ λ (a₁ a₂ b₁ b₂ : α) h₁ h₂,
+    propext ⟨λ h, h₁.2.trans_lt $ h.trans_le h₂.1, λ h, h₁.1.trans_lt $ h.trans_le h₂.2⟩,
+  le_refl := λ a, quotient.induction_on' a $ le_refl,
+  le_trans := λ a b c, quotient.induction_on₃' a b c $ λ a b c, le_trans,
+  lt_iff_le_not_le := λ a b, quotient.induction_on₂' a b $ λ a b, lt_iff_le_not_le,
+  le_antisymm := λ a b, quotient.induction_on₂' a b $ λ a b hab hba, quotient.sound' ⟨hab, hba⟩ }
+
+-- TODO@Yaël: Make computable by adding the missing decidability instances for `quotient.lift` and
+-- `quotient.lift₂`
+noncomputable instance [is_total α (≤)] : linear_order (antisymmetrization α (≤)) :=
+{ le_total := λ a b, quotient.induction_on₂' a b $ total_of (≤),
+  decidable_eq := classical.dec_rel _,
+  decidable_le := classical.dec_rel _,
+  decidable_lt := classical.dec_rel _,
+  ..antisymmetrization.partial_order }
+
+@[simp] lemma to_antisymmetrization_le_to_antisymmetrization_iff :
+  to_antisymmetrization (≤) a ≤ to_antisymmetrization (≤) b ↔ a ≤ b := iff.rfl
+
+@[simp] lemma to_antisymmetrization_lt_to_antisymmetrization_iff :
+  to_antisymmetrization (≤) a < to_antisymmetrization (≤) b ↔ a < b := iff.rfl
+
+@[simp] lemma of_antisymmetrization_le_of_antisymmetrization_iff {a b : antisymmetrization α (≤)} :
+  of_antisymmetrization (≤) a ≤ of_antisymmetrization (≤) b ↔ a ≤ b :=
+by convert to_antisymmetrization_le_to_antisymmetrization_iff.symm;
+  exact (to_antisymmetrization_of_antisymmetrization _ _).symm
+
+@[simp] lemma of_antisymmetrization_lt_of_antisymmetrization_iff {a b : antisymmetrization α (≤)} :
+  of_antisymmetrization (≤) a < of_antisymmetrization (≤) b ↔ a < b :=
+by convert to_antisymmetrization_lt_to_antisymmetrization_iff.symm;
+  exact (to_antisymmetrization_of_antisymmetrization _ _).symm
+
+@[mono] lemma to_antisymmetrization_mono : monotone (@to_antisymmetrization α (≤) _) := λ a b, id
+
+/-- `to_antisymmetrization` as an order homomorphism. -/
+@[simps] def order_hom.to_antisymmetrization : α →o antisymmetrization α (≤) :=
+⟨to_antisymmetrization (≤), λ a b, id⟩
+
+private lemma lift_fun_antisymm_rel (f : α →o β) :
+  ((antisymm_rel.setoid α (≤)).r ⇒ (antisymm_rel.setoid β (≤)).r) f f :=
+λ a b h, ⟨f.mono h.1, f.mono h.2⟩
+
+/-- Turns an order homomorphism from `α` to `β` into one from `antisymmetrization α` to
+`antisymmetrization β`. `antisymmetrization` is actually a functor. See `Preorder_to_PartialOrder`.
+-/
+protected def order_hom.antisymmetrization (f : α →o β) :
+  antisymmetrization α (≤) →o antisymmetrization β (≤) :=
+⟨quotient.map' f $ lift_fun_antisymm_rel f, λ a b, quotient.induction_on₂' a b $ f.mono⟩
+
+@[simp] lemma order_hom.coe_antisymmetrization (f : α →o β) :
+  ⇑f.antisymmetrization = quotient.map' f (lift_fun_antisymm_rel f) := rfl
+
+@[simp] lemma order_hom.antisymmetrization_apply (f : α →o β) (a : antisymmetrization α (≤)) :
+  f.antisymmetrization a = quotient.map' f (lift_fun_antisymm_rel f) a := rfl
+
+@[simp] lemma order_hom.antisymmetrization_apply_mk (f : α →o β) (a : α) :
+  f.antisymmetrization (to_antisymmetrization _ a) = (to_antisymmetrization _ (f a)) :=
+quotient.map'_mk' f (lift_fun_antisymm_rel f) _
+
+variables (α)
+
+/-- `of_antisymmetrization` as an order embedding. -/
+@[simps] noncomputable def order_embedding.of_antisymmetrization : antisymmetrization α (≤) ↪o α :=
+{ to_fun := of_antisymmetrization _,
+  inj' := λ _ _, quotient.out_inj.1,
+  map_rel_iff' := λ a b, of_antisymmetrization_le_of_antisymmetrization_iff }
+
+/-- `antisymmetrization` and `order_dual` commute. -/
+def order_iso.dual_antisymmetrization :
+  order_dual (antisymmetrization α (≤)) ≃o antisymmetrization (order_dual α) (≤) :=
+{ to_fun := quotient.map' id $ λ _ _, and.symm,
+  inv_fun := quotient.map' id $ λ _ _, and.symm,
+  left_inv := λ a, quotient.induction_on' a $ λ a, by simp_rw [quotient.map'_mk', id],
+  right_inv := λ a, quotient.induction_on' a $ λ a, by simp_rw [quotient.map'_mk', id],
+  map_rel_iff' := λ a b, quotient.induction_on₂' a b $ λ a b, iff.rfl }
+
+@[simp] lemma order_iso.dual_antisymmetrization_apply (a : α) :
+  order_iso.dual_antisymmetrization _ (to_dual $ to_antisymmetrization _ a) =
+    to_antisymmetrization _ (to_dual a) := rfl
+
+@[simp] lemma order_iso.dual_antisymmetrization_symm_apply (a : α) :
+  (order_iso.dual_antisymmetrization _).symm (to_antisymmetrization _ $ to_dual a) =
+    to_dual (to_antisymmetrization _ a) := rfl
+
+end preorder
+
+section partial_order
+variables
+
+end partial_order
diff --git a/src/order/category/PartialOrder.lean b/src/order/category/PartialOrder.lean
index d4507db920c13..c22721d514545 100644
--- a/src/order/category/PartialOrder.lean
+++ b/src/order/category/PartialOrder.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-
+import order.antisymmetrization
 import order.category.Preorder
 
 /-!
@@ -58,3 +58,34 @@ end PartialOrder
 lemma PartialOrder_to_dual_comp_forget_to_Preorder :
   PartialOrder.to_dual ⋙ forget₂ PartialOrder Preorder =
     forget₂ PartialOrder Preorder ⋙ Preorder.to_dual := rfl
+
+/-- `antisymmetrization` as a functor. It is the free functor. -/
+def Preorder_to_PartialOrder : Preorder.{u} ⥤ PartialOrder :=
+{ obj := λ X, PartialOrder.of (antisymmetrization X (≤)),
+  map := λ X Y f, f.antisymmetrization,
+  map_id' := λ X,
+    by { ext, exact quotient.induction_on' x (λ x, quotient.map'_mk' _ (λ a b, id) _) },
+  map_comp' := λ X Y Z f g,
+    by { ext, exact quotient.induction_on' x (λ x, order_hom.antisymmetrization_apply_mk _ _) } }
+
+/-- `Preorder_to_PartialOrder` is left adjoint to the forgetful functor, meaning it is the free
+functor from `Preorder` to `PartialOrder`. -/
+def Preorder_to_PartialOrder_forget_adjunction :
+  Preorder_to_PartialOrder.{u} ⊣ forget₂ PartialOrder Preorder :=
+adjunction.mk_of_hom_equiv
+  { hom_equiv := λ X Y, { to_fun := λ f,
+      ⟨f ∘ to_antisymmetrization (≤), f.mono.comp to_antisymmetrization_mono⟩,
+    inv_fun := λ f, ⟨λ a, quotient.lift_on' a f $ λ a b h, (antisymm_rel.image h f.mono).eq, λ a b,
+      quotient.induction_on₂' a b $ λ a b h, f.mono h⟩,
+    left_inv := λ f, order_hom.ext _ _ $ funext $ λ x, quotient.induction_on' x $ λ x, rfl,
+    right_inv := λ f, order_hom.ext _ _ $ funext $ λ x, rfl },
+  hom_equiv_naturality_left_symm' := λ X Y Z f g,
+    order_hom.ext _ _ $ funext $ λ x, quotient.induction_on' x $ λ x, rfl,
+  hom_equiv_naturality_right' := λ X Y Z f g, order_hom.ext _ _ $ funext $ λ x, rfl }
+
+/-- `Preorder_to_PartialOrder` and `order_dual` commute. -/
+@[simps] def Preorder_to_PartialOrder_comp_to_dual_iso_to_dual_comp_Preorder_to_PartialOrder :
+ (Preorder_to_PartialOrder.{u} ⋙ PartialOrder.to_dual) ≅
+    (Preorder.to_dual ⋙ Preorder_to_PartialOrder) :=
+nat_iso.of_components (λ X, PartialOrder.iso.mk $ order_iso.dual_antisymmetrization _) $
+  λ X Y f, order_hom.ext _ _ $ funext $ λ x, quotient.induction_on' x $ λ x, rfl
diff --git a/src/order/rel_classes.lean b/src/order/rel_classes.lean
index 7d31544d225ac..12f1a8f1e433c 100644
--- a/src/order/rel_classes.lean
+++ b/src/order/rel_classes.lean
@@ -21,8 +21,10 @@ variables {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β 
 open function
 
 lemma comm [is_symm α r] {a b : α} : r a b ↔ r b a := ⟨symm, symm⟩
-lemma antisymm' {r : α → α → Prop} [is_antisymm α r] {a b : α} : r a b → r b a → b = a :=
-λ h h', antisymm h' h
+lemma antisymm' [is_antisymm α r] {a b : α} : r a b → r b a → b = a := λ h h', antisymm h' h
+
+lemma antisymm_iff [is_refl α r] [is_antisymm α r] {a b : α} : r a b ∧ r b a ↔ a = b :=
+⟨λ h, antisymm h.1 h.2, by { rintro rfl, exact ⟨refl _, refl _⟩ }⟩
 
 /-- A version of `antisymm` with `r` explicit.