## Stream: graph theory

### Topic: set {s : sym2 V // ¬s.is_diag}

#### Eric Wieser (Jul 16 2021 at 15:28):

Do we have something like this anywhere?

/-- Every set of non-diagonal edges is a simple graph -/
def iso_set_sym2 [decidable_eq V] : simple_graph V ≃ set {s : sym2 V // ¬s.is_diag} :=
{ to_fun := λ g, (coe : _ → sym2 V) ⁻¹' g.edge_set,
inv_fun := λ s,
{ adj := λ v w, ⟦(v, w)⟧ ∈ (coe : _ → sym2 V) '' s,
sym := λ v w h, by { rw sym2.eq_swap, exact h},
loopless := λ v h, by simpa using h },
left_inv := λ g, begin
ext v w,
dsimp,
rw [set.image_preimage_eq_inter_range, set.mem_inter_iff, subtype.range_coe_subtype,
set.mem_set_of_eq, sym2.is_diag_iff_proj_eq, mem_edge_set, and_iff_left_iff_imp],
end,
right_inv := λ E, begin
ext ⟨e, he⟩,
induction e using quotient.induction_on,
cases e,
dsimp,
simp_rw [set.mem_image, set.mem_preimage, subtype.exists, subtype.coe_mk,
exists_and_distrib_right, exists_eq_right, mem_edge_set],
rw exists_prop_of_true,
end }


#### Eric Rodriguez (Jul 16 2021 at 15:45):

i'd be super surprised if we did

#### Eric Rodriguez (Jul 16 2021 at 15:49):

searching for ≃ in combinatorics/simple_graph makes me pretty sure the answer is no

#### Eric Wieser (Jul 16 2021 at 15:58):

I was able to golf it a little using ne_of_adj and edge_set

#### Bhavik Mehta (Jul 16 2021 at 15:58):

I think we should have this, if it's not there already

#### Eric Wieser (Jul 16 2021 at 15:58):

The idea here is that you could use this to get the boolean algebra structure, although I'm not sure if it is definitionally nice

#### Bhavik Mehta (Jul 16 2021 at 16:02):

Right I think this is exactly the right idea, and we can use copy to get nice definitional properties if needed

#### Eric Rodriguez (Jul 16 2021 at 16:29):

Eric, no need for this:

instance : boolean_algebra (simple_graph V) :=
boolean_algebra.of_core ${ compl := compl, le_sup_inf := λ a b c v w ⟨hab, hac⟩, or.dcases_on hac or.inl$
or.dcases_on hab (λ h _, or.inl h) $λ hb hc, or.inr ⟨hb, hc⟩, inf_compl_le_bot := λ a v w h, false.elim$ h.2.2 h.1,
top_le_sup_compl := λ a v w ne, by {by_cases a.adj v w, exact or.inl h, exact or.inr ⟨ne, h⟩},
..simple_graph.bounded_lattice }


#### Eric Wieser (Jul 16 2021 at 16:53):

Sure, but my approach would give you the bounded_lattice too

#### Eric Rodriguez (Jul 16 2021 at 17:06):

i feel like with this approach it's more of a pain to get the right definitional properties than just writing it by hand (I'm currently rewriting without of_core to get a better sdiff), but it'd certainly be good to have a lift for various levels of lattices

#### Kyle Miller (Jul 16 2021 at 17:47):

Maybe it's worth adding in sym2.to_rel as an inverse to sym2.from_rel, defining an equivalence

{r : V → V → Prop // symmetric r ∧ irreflexive r} ≃ set {s : sym2 V // ¬s.is_diag}


in sym2, and then using this to define the equivalence. (Whether or not this is how the boolean_algebra is defined.)

namespace sym2

def to_rel (s : set (sym2 V)) (v w : V) : Prop := ⟦(v, w)⟧ ∈ s
@[simp] lemma to_rel_def (s : set (sym2 V)) (v w : V) : to_rel s v w ↔ ⟦(v, w)⟧ ∈ s := iff.rfl
lemma to_rel.symmetric (s : set (sym2 V)) : symmetric (to_rel s) :=
λ v w h, by rwa [to_rel, sym2.eq_swap]
@[simp] lemma to_rel_of_from_rel {α : Type*} {r : α → α → Prop} (h : symmetric r) :
to_rel (from_rel h) = r := rfl
@[simp] lemma from_rel_of_to_rel (s : set (sym2 V)) : from_rel (to_rel.symmetric s) = s :=
begin
ext z,
refine quotient.ind (λ x, _) z,
simp
end

end sym2

def rel_iso_sym2 : {r : V → V → Prop // symmetric r ∧ irreflexive r} ≃ set {s : sym2 V // ¬s.is_diag} :=
{ to_fun := λ x, coe ⁻¹' sym2.from_rel x.property.1,
inv_fun := λ s, ⟨sym2.to_rel (coe '' s), sym2.to_rel.symmetric _, λ v, by simp⟩,
left_inv := begin
rintro ⟨r, hs, hi⟩,
ext v w,
simp only [subtype.image_preimage_coe, set.mem_inter_eq, and_iff_left_iff_imp,
sym2.to_rel_def, sym2.from_rel_prop, subtype.coe_mk],
intro h,
--  change ¬sym2.is_diag ⟦(v, w)⟧,
apply (@sym2.from_rel_irreflexive _ _ hs).mp hi,
exact h,
end,
right_inv := begin
intro s,
ext x,
cases x with x hx,
simp [hx],
end }

def iso_set_rel : simple_graph V ≃ {r : V → V → Prop // symmetric r ∧ irreflexive r} :=
{ to_fun := λ G, ⟨G.adj, G.sym, G.loopless⟩,
inv_fun := λ x, ⟨x, x.property.1, x.property.2⟩,
left_inv := by tidy,
right_inv := by tidy }


#### Kyle Miller (Jul 16 2021 at 17:48):

By the way, something goes weird at the simp right before the commented out change. Something causes the expression to leave the set API, and I didn't track down what.

#### Kyle Miller (Jul 16 2021 at 17:50):

This is just factoring @Eric Wieser's definition into two parts -- I think it's generally useful to have an equivalence to a type made up of the "standard" inductive types. (I'm hoping that eventually there will be an attribute to automatically create these.)

There should probably also be

{r : V → V → Prop // symmetric r} ≃ set (sym2 V)


#### Eric Wieser (Jul 16 2021 at 19:18):

I think theres a sym2.lift hiding in your idea there, I'll try to PR it

#### Eric Wieser (Jul 18 2021 at 15:09):

#8358

Last updated: Aug 03 2023 at 10:10 UTC