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,
    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,
  right_inv := λ E, begin
    ext e, he⟩,
    induction e using quotient.induction_on,
    cases e,
    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 :=
  ext z,
  refine quotient.ind (λ x, _) z,

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,
  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