edge_set for Digraphs

Stream: new members

[Christopher Schmidt]

Hello everyone, I am working on directed Graphs and I am trying to analogously (to simple_graph) introduce a bunch of stuff.
Right now I am trying to get and analogue to :

def edge_set : simple_graph V ↪o set (sym2 V) :=
order_embedding.of_map_le_iff (λ G, sym2.from_rel G.symm) $
  λ G G', ⟨λ h a b, @h ⟦(a, b)⟧, λ h e, sym2.ind @h e⟩

Here an mwe :

universe u

@[ext]
structure directed_simple_graph (V : Type u) := (adj : V → V → Prop)

namespace directed_simple_graph

variables {V : Type u}
variables (G : directed_simple_graph V)

def edge_set : directed_simple_graph V ↪ set (V × V) :=  \lambda G, sorry

I am a little lost on how to implement the idea that set(V \times V) is supposed to include all v1 v2 : V that fulfill G.adj

Any help is appreciated.

[Kyle Miller]

@Christopher Schmidt Here's an order embedding:

universe u

@[ext]
structure directed_simple_graph (V : Type u) := (adj : V → V → Prop)

namespace directed_simple_graph

variables {V : Type u}
variables (G : directed_simple_graph V)

-- Give `directed_simple_graph V` the induced partial order from the one already
-- defined on  `V → V → Prop`
instance : partial_order (directed_simple_graph V) := partial_order.lift adj ext

def edge_set : directed_simple_graph V ↪o set (V × V) :=
order_embedding.of_map_le_iff (λ (G : directed_simple_graph V), {p : V × V | G.adj p.1 p.2}) $
begin
  intros G G',
  rw [le_eq_subset, set_of_subset_set_of, prod.forall],
  refl,
end

end directed_simple_graph

[Kyle Miller]

Here's just an embedding:

def edge_set : directed_simple_graph V ↪ set (V × V) :=
{ to_fun := λ G, {p : V × V | G.adj p.1 p.2},
  inj' := begin
    intros G G' h,
    simp only [set.ext_iff] at h,
    ext u v,
    specialize h (u, v),
    exact h,
  end }

It takes a different proof since order_embedding.of_map_le_iff is able to prove the injectivity condition using a order-based principle.

[Kyle Miller]

Here's a plain function:

def edge_set : directed_simple_graph V → set (V × V) :=
λ G, {p : V × V | G.adj p.1 p.2}

Not too long ago docs#simple_graph.edge_set used to be a plain function

[Christopher Schmidt]

Thank you so much @Kyle Miller .
However, I have got a question. What is the difference between the embedding and the plain function when it comes to the use of G.edge_set ? Don't both just provide the same result ?

[Kyle Miller]

They all give the same functions, but the embeddings "bundle" additional proofs with the functions, which can make general lemmas about them become more easily available.

Otherwise, you can give extra lemmas about edge sets yourself. (The "unbundled" approach.)

I'm not sure exactly if there are applications of bundled edge sets in mathlib yet.

[Christopher Schmidt]

Ah I see. Thank you.