Zulip Chat Archive

Stream: Is there code for X?

Topic: Injective on a set up to a relation


view this post on Zulip Kyle Miller (Jun 25 2020 at 18:38):

I couldn't find a definition like the following in mathlib:

universes u v
variables {α : Type u} {β : Type v}

@[reducible] def inj_on_by (f : α  β) (s : set α) (r : α  α  Prop) : Prop :=
x₁ x₂ : α⦄, x₁  s  x₂  s  f x₁ = f x₂  r x₁ x₂

(this is a variation on set.inj_on in data/set/function.lean). For the particular use I have in mind, α has a setoid instance, in case that matters.

So, (1) is there some other definition I should be using? or, barring that, (2) would this function be welcome in data/set/function.lean or elsewhere?

view this post on Zulip Patrick Massot (Jun 25 2020 at 18:40):

This looks very specialized.

view this post on Zulip Reid Barton (Jun 25 2020 at 18:41):

inj_on is already pretty obscure, I would say

view this post on Zulip Johan Commelin (Jun 25 2020 at 18:43):

@Kyle Miller I guess you want to use this in your graph theory stuff, right? Could you explain a bit more how/why?

view this post on Zulip Patrick Massot (Jun 25 2020 at 18:43):

#xy

view this post on Zulip Kyle Miller (Jun 25 2020 at 19:07):

@Johan Commelin One of the axioms for undirected graphs in the Chou formalization is exactly inj_on_by link.via links (≈), where links is a set of link elements, defined by

structure link (α : Type u) (β : Type v) :=
(src : α) (via : β) (dest : α)

def link.rev (x : link α β) : link α β := x.dest, x.via, x.src

with an equivalence relation given by

def same_edge : link α β  link α β  Prop := λ x y, x = y  x = y.rev

That is, if two links carry the same edge (have the same via), then they are equal up to orientation reversal.

It's not essential that this definition actually exists, and I'm fine with writing out the full definition of the axiom in the structure. This would be the only one of the three axioms involving any quantifiers.

In the context of all the axioms, we want link.via on the links set to have link.rev acting on its fibers.

Another way of thinking about this particular axiom is that link.via descends to a map on the quotient of link α β by same_edge, and we wish for this map to be injective. It seems like it would be more trouble than it's worth to use quotient types to specify this axiom.

view this post on Zulip Johan Commelin (Jun 25 2020 at 19:15):

I think it's easiest to just write it out

view this post on Zulip Johan Commelin (Jun 25 2020 at 19:16):

\forall x y, x.via = y.via → same_edge x y
is that what you want, or am I missing something?

view this post on Zulip Kyle Miller (Jun 25 2020 at 19:43):

Since there's a set of links, it would be

 {x y}, x  links  y  links  x.via = y.via  same_edge x y

but yeah, that's pretty much it.

I just thought I'd ask in case this was somehow less specialized than I imagined it to be, or if there was some convenient setoid thing I didn't know about.

Thanks for the advice everyone.

view this post on Zulip Johan Commelin (Jun 25 2020 at 19:45):

Yeah, just use what you wrote. It's fine.


Last updated: May 19 2021 at 02:10 UTC