# Zulip Chat Archive

## 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],
apply ne_of_adj,
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):

Last updated: Aug 03 2023 at 10:10 UTC