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

Stream: graph theory

[Eric Wieser]

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]

i'd be super surprised if we did

[Eric Rodriguez]

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

[Eric Wieser]

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

[Bhavik Mehta]

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

[Eric Wieser]

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]

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

[Eric Rodriguez]

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]

Sure, but my approach would give you the bounded_lattice too

[Eric Rodriguez]

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]

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]

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]

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]

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

[Eric Wieser]

#8358