Injective on a set up to a relation

Stream: Is there code for X?

[Kyle Miller]

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?

[Patrick Massot]

This looks very specialized.

[Reid Barton]

inj_on is already pretty obscure, I would say

[Johan Commelin]

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

[Patrick Massot]

#xy

[Kyle Miller]

@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.

[Johan Commelin]

I think it's easiest to just write it out

[Johan Commelin]

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

[Kyle Miller]

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.

[Johan Commelin]

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