Zulip Chat Archive

Stream: maths

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


view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 27 2018 at 16:07):

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

view this post on Zulip Kenny Lau (Apr 27 2018 at 16:07):

and I used all three properties of a partial order

view this post on Zulip 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 }

view this post on Zulip Kenny Lau (Apr 27 2018 at 16:13):

and the converse :P

view this post on Zulip Kenny Lau (Apr 27 2018 at 16:14):

wait, that's the wrong converse

view this post on Zulip 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}

view this post on Zulip Reid Barton (Apr 27 2018 at 17:18):

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

view this post on Zulip 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