## Stream: maths

### Topic: every partial order can be order-embedded into a powerset

#### Kenny Lau (Apr 27 2018 at 16:07):

section

variables {α : Type u} [partial_order α] (x y : α)

def partial_order.embed : set α :=
{ z | z ≤ x }

theorem partial_order.embed.injective : function.injective (@partial_order.embed α _) :=
λ x y hxy,
have H1 : x ∈ partial_order.embed y, from hxy ▸ le_refl _,
have H2 : y ∈ partial_order.embed x, from hxy.symm ▸ le_refl _,
le_antisymm H1 H2

theorem partial_order.embed.ord (H : x ≤ y) : partial_order.embed x ⊆ partial_order.embed y :=
λ z hz, le_trans hz H

end


#### Kenny Lau (Apr 27 2018 at 16:07):

is there a more compact version of the title using category language?

#### Kenny Lau (Apr 27 2018 at 16:07):

and I used all three properties of a partial order

#### Kenny Lau (Apr 27 2018 at 16:13):

def converse (r : α → α → Prop) (H : r ≼o ((⊆) : set β → set β → Prop)) : partial_order α :=
{ le := inv_image (⊆) H,
le_refl := λ _, set.subset.refl _,
le_trans := λ _ _ _, set.subset.trans,
le_antisymm := λ _ _ H1 H2, H.1.2 \$ set.subset.antisymm H1 H2 }


#### Kenny Lau (Apr 27 2018 at 16:13):

and the converse :P

#### Kenny Lau (Apr 27 2018 at 16:14):

wait, that's the wrong converse

#### Reid Barton (Apr 27 2018 at 17:17):

It's the enriched Yoneda lemma where the enriching category is the poset of truth values {false -> true}

#### Reid Barton (Apr 27 2018 at 17:18):

{ z | z ≤ x } is the characteristic feature of Yoneda things.

#### Reid Barton (Apr 27 2018 at 17:25):

I guess there's slightly more going on here because you said "embedded into a powerset" = all functions from \a to V = {false -> true}, while the Yoneda embedding lands in order-reversing maps \a to V, i.e., lower sets of \a.

Last updated: May 14 2021 at 20:13 UTC