Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(order/antisymmetrization): Turning a preorder into a partial ord…
…er (#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`.
- Loading branch information
1 parent
8a286af
commit 6bcb12c
Showing
4 changed files
with
230 additions
and
4 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters