Turning a preorder into a partial order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

def antisymm_rel {α : Type u_1} (r : α → α → Prop) (a b : α) :

Prop

The antisymmetrization relation.

Equations

antisymm_rel r a b = (r a b ∧ r b a)

Instances for antisymm_rel

antisymm_rel.decidable_rel

source

theorem antisymm_rel_swap {α : Type u_1} (r : α → α → Prop) :

antisymm_rel (function.swap r) = antisymm_rel r

source

@[refl]

theorem antisymm_rel_refl {α : Type u_1} (r : α → α → Prop) [is_refl α r] (a : α) :

antisymm_rel r a a

source

@[symm]

theorem antisymm_rel.symm {α : Type u_1} {r : α → α → Prop} {a b : α} :

antisymm_rel r a b → antisymm_rel r b a

source

@[trans]

theorem antisymm_rel.trans {α : Type u_1} {r : α → α → Prop} [is_trans α r] {a b c : α} (hab : antisymm_rel r a b) (hbc : antisymm_rel r b c) :

antisymm_rel r a c

source

@[protected, instance]

def antisymm_rel.decidable_rel {α : Type u_1} {r : α → α → Prop} [decidable_rel r] :

decidable_rel (antisymm_rel r)

Equations

antisymm_rel.decidable_rel = λ (_x _x_1 : α), and.decidable

source

@[simp]

theorem antisymm_rel_iff_eq {α : Type u_1} {r : α → α → Prop} [is_refl α r] [is_antisymm α r] {a b : α} :

antisymm_rel r a b ↔ a = b

source

theorem antisymm_rel.eq {α : Type u_1} {r : α → α → Prop} [is_refl α r] [is_antisymm α r] {a b : α} :

antisymm_rel r a b → a = b

Alias of the forward direction of antisymm_rel_iff_eq.

source

def antisymm_rel.setoid (α : Type u_1) (r : α → α → Prop) [is_preorder α r] :

setoid α

The antisymmetrization relation as an equivalence relation.

Equations

antisymm_rel.setoid α r = {r := antisymm_rel r, iseqv := _}

source

@[simp]

theorem antisymm_rel.setoid_r (α : Type u_1) (r : α → α → Prop) [is_preorder α r] (a b : α) :

a ≈ b = antisymm_rel r a b

source

def antisymmetrization (α : Type u_1) (r : α → α → Prop) [is_preorder α r] :

Type u_1

The partial order derived from a preorder by making pairwise comparable elements equal. This is the quotient by λ a b, a ≤ b ∧ b ≤ a.

Equations

antisymmetrization α r = quotient (antisymm_rel.setoid α r)

Instances for antisymmetrization

source

def to_antisymmetrization {α : Type u_1} (r : α → α → Prop) [is_preorder α r] :

α → antisymmetrization α r

Turn an element into its antisymmetrization.

Equations

to_antisymmetrization r = quotient.mk'

source

noncomputable def of_antisymmetrization {α : Type u_1} (r : α → α → Prop) [is_preorder α r] :

antisymmetrization α r → α

Get a representative from the antisymmetrization.

Equations

of_antisymmetrization r = quotient.out'

source

@[protected, instance]

def antisymmetrization.inhabited {α : Type u_1} (r : α → α → Prop) [is_preorder α r] [inhabited α] :

inhabited (antisymmetrization α r)

Equations

antisymmetrization.inhabited r = quotient.inhabited (antisymm_rel.setoid α r)

source

@[protected]

theorem antisymmetrization.ind {α : Type u_1} (r : α → α → Prop) [is_preorder α r] {p : antisymmetrization α r → Prop} :

(∀ (a : α), p (to_antisymmetrization r a)) → ∀ (q : antisymmetrization α r), p q

source

@[protected]

theorem antisymmetrization.induction_on {α : Type u_1} (r : α → α → Prop) [is_preorder α r] {p : antisymmetrization α r → Prop} (a : antisymmetrization α r) (h : ∀ (a : α), p (to_antisymmetrization r a)) :

p a

source

@[simp]

theorem to_antisymmetrization_of_antisymmetrization {α : Type u_1} (r : α → α → Prop) [is_preorder α r] (a : antisymmetrization α r) :

to_antisymmetrization r (of_antisymmetrization r a) = a

source

theorem antisymm_rel.image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {a b : α} (h : antisymm_rel has_le.le a b) {f : α → β} (hf : monotone f) :

antisymm_rel has_le.le (f a) (f b)

source

@[protected, instance]

def antisymmetrization.partial_order {α : Type u_1} [preorder α] :

partial_order (antisymmetrization α has_le.le)

Equations

antisymmetrization.partial_order = {le := λ (a b : antisymmetrization α has_le.le), quotient.lift_on₂' a b has_le.le antisymmetrization.partial_order._proof_1, lt := λ (a b : antisymmetrization α has_le.le), quotient.lift_on₂' a b has_lt.lt antisymmetrization.partial_order._proof_2, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

theorem antisymmetrization_fibration {α : Type u_1} [preorder α] :

relation.fibration has_lt.lt has_lt.lt (to_antisymmetrization has_le.le)

source

theorem acc_antisymmetrization_iff {α : Type u_1} [preorder α] {a : α} :

acc has_lt.lt (to_antisymmetrization has_le.le a) ↔ acc has_lt.lt a

source

theorem well_founded_antisymmetrization_iff {α : Type u_1} [preorder α] :

well_founded has_lt.lt ↔ well_founded has_lt.lt

source

@[protected, instance]

def antisymmetrization.well_founded_lt {α : Type u_1} [preorder α] [well_founded_lt α] :

well_founded_lt (antisymmetrization α has_le.le)

source

@[protected, instance]

def antisymmetrization.linear_order {α : Type u_1} [preorder α] [decidable_rel has_le.le] [decidable_rel has_lt.lt] [is_total α has_le.le] :

linear_order (antisymmetrization α has_le.le)

Equations

antisymmetrization.linear_order = {le := partial_order.le antisymmetrization.partial_order, lt := partial_order.lt antisymmetrization.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (_x _x_1 : antisymmetrization α has_le.le), quotient.lift_on₂'.decidable _x _x_1 (λ (a₁ : α), has_le.le a₁) antisymmetrization.partial_order._proof_1, decidable_eq := quotient.decidable_eq antisymm_rel.decidable_rel, decidable_lt := λ (_x _x_1 : antisymmetrization α has_le.le), quotient.lift_on₂'.decidable _x _x_1 (λ (a₁ : α), has_lt.lt a₁) antisymmetrization.partial_order._proof_2, max := max_default (λ (a b : antisymmetrization α has_le.le), quotient.lift_on₂'.decidable a b (λ (a₁ : α), has_le.le a₁) antisymmetrization.partial_order._proof_1), max_def := _, min := min_default (λ (a b : antisymmetrization α has_le.le), quotient.lift_on₂'.decidable a b (λ (a₁ : α), has_le.le a₁) antisymmetrization.partial_order._proof_1), min_def := _}

source

@[simp]

theorem to_antisymmetrization_le_to_antisymmetrization_iff {α : Type u_1} [preorder α] {a b : α} :

to_antisymmetrization has_le.le a ≤ to_antisymmetrization has_le.le b ↔ a ≤ b

source

@[simp]

theorem to_antisymmetrization_lt_to_antisymmetrization_iff {α : Type u_1} [preorder α] {a b : α} :

to_antisymmetrization has_le.le a < to_antisymmetrization has_le.le b ↔ a < b

source

@[simp]

theorem of_antisymmetrization_le_of_antisymmetrization_iff {α : Type u_1} [preorder α] {a b : antisymmetrization α has_le.le} :

of_antisymmetrization has_le.le a ≤ of_antisymmetrization has_le.le b ↔ a ≤ b

source

@[simp]

theorem of_antisymmetrization_lt_of_antisymmetrization_iff {α : Type u_1} [preorder α] {a b : antisymmetrization α has_le.le} :

of_antisymmetrization has_le.le a < of_antisymmetrization has_le.le b ↔ a < b

source

theorem to_antisymmetrization_mono {α : Type u_1} [preorder α] :

monotone (to_antisymmetrization has_le.le)

source

def order_hom.to_antisymmetrization {α : Type u_1} [preorder α] :

α →o antisymmetrization α has_le.le

to_antisymmetrization as an order homomorphism.

Equations

order_hom.to_antisymmetrization = {to_fun := to_antisymmetrization has_le.le has_le.le.is_preorder, monotone' := _}

source

@[simp]

theorem order_hom.to_antisymmetrization_coe {α : Type u_1} [preorder α] (ᾰ : α) :

⇑order_hom.to_antisymmetrization ᾰ = to_antisymmetrization has_le.le ᾰ

source

@[protected]

def order_hom.antisymmetrization {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) :

antisymmetrization α has_le.le →o antisymmetrization β has_le.le

Turns an order homomorphism from α to β into one from antisymmetrization α to antisymmetrization β. antisymmetrization is actually a functor. See Preorder_to_PartialOrder.

Equations

f.antisymmetrization = {to_fun := quotient.map' ⇑f _, monotone' := _}

source

@[simp]

theorem order_hom.coe_antisymmetrization {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) :

⇑(f.antisymmetrization) = quotient.map' ⇑f _

source

@[simp]

theorem order_hom.antisymmetrization_apply {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : antisymmetrization α has_le.le) :

⇑(f.antisymmetrization) a = quotient.map' ⇑f _ a

source

@[simp]

theorem order_hom.antisymmetrization_apply_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α →o β) (a : α) :

⇑(f.antisymmetrization) (to_antisymmetrization has_le.le a) = to_antisymmetrization has_le.le (⇑f a)

source

noncomputable def order_embedding.of_antisymmetrization (α : Type u_1) [preorder α] :

antisymmetrization α has_le.le ↪o α

of_antisymmetrization as an order embedding.

Equations

order_embedding.of_antisymmetrization α = {to_embedding := {to_fun := of_antisymmetrization has_le.le has_le.le.is_preorder, inj' := _}, map_rel_iff' := _}

source

@[simp]

theorem order_embedding.of_antisymmetrization_apply (α : Type u_1) [preorder α] (ᾰ : antisymmetrization α has_le.le) :

⇑(order_embedding.of_antisymmetrization α) ᾰ = of_antisymmetrization has_le.le ᾰ

source

def order_iso.dual_antisymmetrization (α : Type u_1) [preorder α] :

(antisymmetrization α has_le.le)ᵒᵈ ≃o antisymmetrization αᵒᵈ has_le.le

antisymmetrization and order_dual commute.

Equations

order_iso.dual_antisymmetrization α = {to_equiv := {to_fun := quotient.map' id _, inv_fun := quotient.map' id _, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem order_iso.dual_antisymmetrization_apply (α : Type u_1) [preorder α] (a : α) :

⇑(order_iso.dual_antisymmetrization α) (⇑order_dual.to_dual (to_antisymmetrization has_le.le a)) = to_antisymmetrization has_le.le (⇑order_dual.to_dual a)

source

@[simp]

theorem order_iso.dual_antisymmetrization_symm_apply (α : Type u_1) [preorder α] (a : α) :

⇑((order_iso.dual_antisymmetrization α).symm) (to_antisymmetrization has_le.le (⇑order_dual.to_dual a)) = ⇑order_dual.to_dual (to_antisymmetrization has_le.le a)