Union of connected subgraphs

Stream: graph theory

[Rémi Bottinelli]

Hey! Is there code dealing with non-empty intersection of connected subgraphs being connected, and related facts? E.g. the support of a walk is connected, and two "adjacent" connected subgraphs are connected?
If not, would that have its place somewhere?

lemma connected.union {V : Type*} {G : simple_graph V} {H K : G.subgraph}
  (Hconn : H.connected) (Kconn : K.connected) (HinterK : (H.inter K).verts.nonempty ) : (H.union K).connected :=
begin
  obtain ⟨v,⟨vH,vK⟩⟩ := HinterK,
  have vHK : v ∈ (H.union K).verts := by { left, exact vH,},
  haveI nempty : nonempty (H.union K).verts, by { use [v,vHK], },

  apply simple_graph.connected.mk,

  suffices : ∀ x : (H.union K).verts, (H.union K).coe.reachable x ⟨v,vHK⟩,
  { rintro x y, exact (this x).trans (this y).symm, },

  rintro ⟨x,xH|xK⟩,
  { obtain ⟨xv⟩ := Hconn ⟨x,xH⟩ ⟨v,vH⟩,
    use xv.map (subgraph.inclusion (sorry : H ≤ H.union K)), },
  { obtain ⟨xv⟩ := Kconn ⟨x,xK⟩ ⟨v,vK⟩,
    use xv.map (subgraph.inclusion (sorry : K ≤ H.union K)), },
end

lemma connected.adj_pair {V : Type*} {G : simple_graph V} {u v : V} (a : G.adj u v) : (G.induce {u,v}).connected :=
begin
  apply simple_graph.connected.mk,
  rintro ⟨x,(xe|xe)⟩ ⟨y,(ye|ye)⟩,
  all_goals {induction xe, induction ye, },
  any_goals {exact reachable.rfl},
  all_goals
  { apply nonempty.intro,
    refine walk.cons _ walk.nil,
    simp only [comap_adj, function.embedding.coe_subtype, subtype.coe_mk], },
  exact a,
  exact a.symm,
end

lemma connected.adj_union  {V : Type*} {G : simple_graph V} {H K : G.subgraph}
  (Hconn : H.connected) (Kconn : K.connected) (u v : V) (uH : u ∈ H.verts) (vK : v ∈ K.verts) (a : G.adj u v) : (H.union K).connected :=
begin
  have : H.union K = ((G.induce {u,v}).union H).union K,
end

[Rémi Bottinelli]

And a related question: There is delete_verts, but not keep_verts, so that I don't see a direct way to construct a subgraph induced by a set of vertices. What should I use?

[Yaël Dillies]

docs#simple_graph.subgraph.induce

[Rémi Bottinelli]

Yaël Dillies said:

docs#simple_graph.subgraph.induce

Ah, right: (⊤ : G.subgraph).induce works, though it looks a bit clumsy. Thanks!

[Rémi Bottinelli]

I've tried proving some relatively elementary facts about induced subgraphs, but it feels like I'm fighting the API:

import combinatorics.simple_graph.connectivity
import combinatorics.simple_graph.basic
import combinatorics.simple_graph.subgraph


open simple_graph

namespace simple_graph

lemma connected.singleton {V : Type*} {G : simple_graph V} (v : V) : ((⊤ : G.subgraph).induce ({v} : set V)).coe.connected :=
begin
  change ((⊤ : G.subgraph).induce {v}).coe.connected,
  rw connected_iff,
  split, rotate,
  { simp only [subgraph.induce_verts, set.nonempty_coe_sort, set.singleton_nonempty] },
  { rintro ⟨x,xe⟩ ⟨y,ye⟩,
   induction xe, induction ye, use walk.nil, },
end

lemma connected.edges_mono {V : Type*} {G : simple_graph V} {H K : G.subgraph} (Hconn : H.connected)
  (sub : H ≤ K) (Veq : H.verts = K.verts) : K.connected :=
begin
  change K.coe.connected,
  change H.coe.connected at Hconn,
  rw connected_iff,
  split, rotate,
  { rw ←Veq, rw connected_iff at Hconn, exact Hconn.2,},
  { rintro ⟨x,xK⟩ ⟨y,yK⟩,
    rw ←Veq at xK yK,
    obtain ⟨xy⟩ := Hconn ⟨x,xK⟩ ⟨y,yK⟩,
    use xy.map (subgraph.inclusion sub),}
end

lemma connected.union {V : Type*} {G : simple_graph V} {H K : G.subgraph}
  (Hconn : H.connected) (Kconn : K.connected) (HinterK : (H.inter K).verts.nonempty ) : (H.union K).coe.connected :=
begin
  obtain ⟨v,⟨vH,vK⟩⟩ := HinterK,
  have vHK : v ∈ (H.union K).verts := by { left, exact vH,},
  haveI nempty : nonempty (H.union K).verts, by { use [v,vHK], },

  change connected (H.union K).coe,
  apply simple_graph.connected.mk,

  suffices : ∀ x : (H.union K).verts, (H.union K).coe.reachable x ⟨v,vHK⟩,
  { rintro x y, exact (this x).trans (this y).symm, },

  rintro ⟨x,xH|xK⟩,
  { obtain ⟨xv⟩ := Hconn ⟨x,xH⟩ ⟨v,vH⟩,
    use xv.map (subgraph.inclusion (sorry : H ≤ H.union K)), },
  { obtain ⟨xv⟩ := Kconn ⟨x,xK⟩ ⟨v,vK⟩,
    use xv.map (subgraph.inclusion (sorry : K ≤ H.union K)), },
end

lemma connected.adj_pair {V : Type*} {G : simple_graph V} {u v : V} (a : G.adj u v) : ((⊤ : G.subgraph).induce {u,v}).coe.connected :=
begin
  change ((⊤ : G.subgraph).induce {u,v}).coe.connected,
  rw connected_iff,
  split, rotate,
  { exact set.has_insert.insert.nonempty u {v}, },
  { rintro ⟨x,(xe|xe)⟩ ⟨y,(ye|ye)⟩,
    all_goals {induction xe, induction ye, },
    any_goals {exact reachable.rfl},
    all_goals
    { apply nonempty.intro,
      refine walk.cons _ walk.nil,
      simp only [subgraph.coe_adj, subtype.coe_mk, subgraph.induce_adj, set.mem_insert_iff, eq_self_iff_true, true_or,
                 set.mem_singleton, or_true, subgraph.top_adj_iff, true_and], },
    exact a,
    exact a.symm, },
end

lemma connected.adj_union  {V : Type*} {G : simple_graph V} {H K : G.subgraph}
  (Hconn : H.connected) (Kconn : K.connected) (u v : V) (uH : u ∈ H.verts) (vK : v ∈ K.verts) (a : G.adj u v) :
  ((⊤ : G.subgraph).induce (H.verts ∪ K.verts)).coe.connected :=
begin
  have : (((⊤ : G.subgraph).induce {u,v}).union H).union K ≤ ((⊤ : G.subgraph).induce (H.verts ∪ K.verts)), by
  { sorry,},
  apply connected.edges_mono,
  { apply connected.union,
    apply connected.union,
    apply connected.adj_pair a,
    { exact Hconn, },
    { use u, split, simp,use uH, },
    { exact Kconn, },
    {use v, split, left, simp, use vK}, },
  { exact this },
  { simp,
    dsimp [subgraph.induce,subgraph.union],
    apply set.eq_of_subset_of_subset,
    { rw set.union_assoc,
      apply set.union_subset,
      { rintro x (xu|xv), {rw xu, left, exact uH}, {simp at xv, rw xv, right, exact vK}},
      { refl, }, },
    {rw set.union_assoc, apply set.subset_union_right,}
  }
end

lemma connected.walk_support {V : Type*} [decidable_eq V] {G : simple_graph V} {u v : V} (p : G.walk u v) :
  ((⊤ : G.subgraph).induce (p.support.to_finset : set V)).coe.connected :=
begin
  change ((⊤ : G.subgraph).induce (p.support.to_finset : set V)).coe.connected,
  induction p,
  { rw [walk.support_nil, list.to_finset_cons, list.to_finset_nil],  let h := @connected.singleton V G p, sorry },
  { rw connected_iff,
    obtain ⟨a,b⟩ := p_ih,
    sorry
  }
end

end simple_graph

[Kyle Miller]

@Rémi Bottinelli Here are some refinements to the lemmas up through connected.adj_union along with some supporting lemmas and constructions. There are still many opportunities for further refinement here since a number of proofs each contain a handful of useful lemmas.

import combinatorics.simple_graph.connectivity
import combinatorics.simple_graph.basic
import combinatorics.simple_graph.subgraph

open simple_graph
open simple_graph.walk

namespace simple_graph

/-- See Note [range copy pattern] -/
protected def copy {V : Type*} (G : simple_graph V) {V' : Type*} (h : V' = V) : simple_graph V' :=
{ adj := λ u v, G.adj (cast h u) (cast h v) }

@[simp] lemma copy_rfl {V : Type*} {G : simple_graph V} : G.copy rfl = G := by { ext, refl }

@[simp] lemma copy_copy {V V' V'' : Type*} {G : simple_graph V} (h : V' = V) (h' : V'' = V') :
  (G.copy h).copy h' = G.copy (h'.trans h) := by { subst h, subst h', refl }

/-- The graphs `G.copy h` and `G` are isomorphic using `cast h` on vertices. -/
@[simps]
def copy_iso {V : Type*} (G : simple_graph V) {V' : Type*} (h : V' = V) : G.copy h ≃g G :=
{ map_rel_iff' := by { subst h, intros u v, refl }, .. equiv.cast h }

@[simp]
lemma subgraph.adj_copy_coe {V : Type*} {G : simple_graph V} (H : G.subgraph) {s : set V}
  (h : s = H.verts) {u v : V} {hu hv} :
  (H.coe.copy (by rw h) : simple_graph s).adj ⟨u, hu⟩ ⟨v, hv⟩ = H.adj u v :=
by { subst h, refl }

lemma subgraph.connected_iff {V : Type*} {G : simple_graph V} (H : G.subgraph) :
  H.connected ↔ H.coe.preconnected ∧ H.verts.nonempty :=
begin
  change H.coe.connected ↔ _,
  rw [connected_iff, set.nonempty_coe_sort],
end

lemma subgraph.induce_singleton_connected {V : Type*} {G : simple_graph V} (v : V) :
  ((⊤ : G.subgraph).induce ({v} : set V)).connected :=
begin
  rw subgraph.connected_iff,
  split,
  { rintro ⟨x, xe, hx⟩ ⟨y, ye, hy⟩,
    use walk.nil, },
  { simp only [subgraph.induce_verts, set.singleton_nonempty] },
end

@[mono]
lemma connected.mono {V : Type*} {G G' : simple_graph V} (h : G ≤ G') :
  G.connected → G'.connected :=
begin
  simp_rw connected_iff,
  rintro ⟨hc, hn⟩,
  refine ⟨_, hn⟩,
  refine λ u v, (hc u v).elim (λ p, _),
  constructor,
  simpa using p.map (hom.map_spanning_subgraphs h),
end

lemma subgraph.connected.edges_mono {V : Type*} {G : simple_graph V} {H K : G.subgraph}
  (sub : H ≤ K) (Veq : H.verts = K.verts) : H.connected → K.connected :=
begin
  have : H.coe ≤ K.coe.copy (by rw Veq),
  { rintro ⟨u, hu⟩ ⟨v, hv⟩,
    simp only [subgraph.coe_adj, subtype.coe_mk, subgraph.adj_copy_coe],
    apply sub.2 },
  intro hc,
  have := hc.mono this,
  rw (copy_iso K.coe _).connected_iff at this,
  exact this,
end

lemma connected.union {V : Type*} {G : simple_graph V} {H K : G.subgraph}
  (Hconn : H.connected) (Kconn : K.connected) (HinterK : (H ⊓ K).verts.nonempty ) :
  (H ⊔ K).connected :=
begin
  obtain ⟨u, huH, huK⟩ := HinterK,
  have hu : u ∈ (H ⊔ K).verts := or.inl huH,
  rw subgraph.connected_iff,
  refine ⟨_, ⟨u, hu⟩⟩,
  have key : ∀ (v : (H ⊔ K).verts), (H ⊔ K).coe.reachable ⟨u, hu⟩ v,
  { rintro ⟨v, hv|hv⟩,
    { refine (Hconn ⟨u, huH⟩ ⟨v, hv⟩).elim (λ p, _),
      have q := p.map (subgraph.inclusion le_sup_left : H.coe →g (H ⊔ K).coe),
      constructor,
      simpa [subgraph.inclusion] using q, },
    { refine (Kconn ⟨u, huK⟩ ⟨v, hv⟩).elim (λ p, _),
      have q := p.map (subgraph.inclusion le_sup_right : K.coe →g (H ⊔ K).coe),
      constructor,
      simpa [subgraph.inclusion] using q, } },
  intros v w,
  exact reachable.trans (key _).symm (key _),
end

lemma subgraph.induce_pair_connected {V : Type*} {G : simple_graph V} {u v : V} (huv : G.adj u v) :
  ((⊤ : G.subgraph).induce {u, v}).connected :=
begin
  rw subgraph.connected_iff,
  split,
  { rintro ⟨x, hx⟩ ⟨y, hy⟩,
    simp only [subgraph.induce_verts, set.mem_insert_iff, set.mem_singleton_iff] at hx hy,
    obtain rfl|rfl := hx; obtain rfl|rfl := hy;
    refl <|> { refine ⟨walk.cons _ walk.nil⟩, simp [huv, huv.symm] } },
  { simp },
end

lemma connected.adj_union  {V : Type*} {G : simple_graph V} {H K : G.subgraph}
  (Hconn : H.connected) (Kconn : K.connected) (u v : V) (uH : u ∈ H.verts) (vK : v ∈ K.verts)
  (huv : G.adj u v) :
  ((⊤ : G.subgraph).induce {u, v} ⊔ H ⊔ K).connected :=
begin
  refine connected.union _ ‹_› _,
  { refine connected.union (subgraph.induce_pair_connected huv) ‹_› _,
    use u, -- TODO add simp lemmas for (inf/sup).verts
    split,
    { simp },
    { assumption } },
  { use v, -- TODO add simp lemmas for (inf/sup).verts
    split,
    { left, simp },
    { assumption } },
end

end simple_graph

[Kyle Miller]

I haven't been bold enough to commit the following coercions, which seem like they would be useful here: https://github.com/leanprover-community/mathlib/blob/walks_and_trees/src/combinatorics/simple_graph/subgraph.lean#L338-L348

They let you use h : G.adj u v as if it were a two-vertex subgraph. Now that we have induce, if we were to decide to introduce the coercion we'd define the coercion as (⊤ : G.subgraph).induce {u, v} (which doesn't strictly need h) and have some supporting lemmas that make use of h.

[Kyle Miller]

By the way, there's docs#simple_graph.induce

This might a reasonable formulation of mapping a walk into an induced graph:

def walk.to_induced  {V : Type*} [decidable_eq V] {G : simple_graph V} (S : set V) :
  Π {u v : S} (p : G.walk u v) (hp : ∀ w ∈ p.support, w ∈ S),
    (G.induce S).walk u v := sorry

However, we should have a function that pulls walks back along injective graph homomorpisms under the condition that the walk's support lies inside the image. Then walk.to_induced can be defined in terms of this. docs#simple_graph.walk.to_delete_edges probably should be redefined in terms of this function too.

[Rémi Bottinelli]

Thanks! Where should the copy part live?

[Rémi Bottinelli]

Mmh, continuing on your “However” remark, shouldn't it be further decomposed into:

• An injective morphism of graph induces an image subgraph and restricts to an isomorphism between domain and image.
• A walk can be “contained” in a subgraph, in which case there is a restriction of the walk to the subgraph.

And then we can combine those two?

[Rémi Bottinelli]

I'm thinking of something like this:

def walk.contained {V : Type*} [decidable_eq V] {G : simple_graph V} (H : G.subgraph)
  {u v : V} (p : G.walk u v) : Prop := (p.edges.to_finset : set $ sym2 V) ⊆ H.edge_set

lemma walk.contained_cons_iff  {V : Type*} [decidable_eq V] {G : simple_graph V} (H : G.subgraph)
  {u v w : V} (a : G.adj u v) (p : G.walk v w) :
  (walk.cons a p).contained H ↔ (H.adj u v ∧ p.contained H) := sorry

lemma walk.contained_verts {V : Type*} [decidable_eq V] {G : simple_graph V} (H : G.subgraph)
  {u v : V} (p : G.walk u v) : p.contained H → (p.support.to_finset : set V) ⊆ H.verts := sorry

lemma walk.contained_append_left  {V : Type*} [decidable_eq V] {G : simple_graph V} (H : G.subgraph)
  {u v w : V} (p : G.walk u v) (q : G.walk v w) : (p.append q).contained H → p.contained H := sorry

lemma walk.contained_append_right  {V : Type*} [decidable_eq V] {G : simple_graph V} (H : G.subgraph)
  {u v w : V} (p : G.walk u v) (q : G.walk v w) : (p.append q).contained H → p.contained H := sorry

def walk.contained.to_subgraph {V : Type*} [decidable_eq V] {G : simple_graph V} (H : G.subgraph)
  {u w : H.verts} (p : G.walk u w) (pcon : p.contained H) : H.coe.walk u w :=
begin
  rcases u with ⟨uu,hu⟩,
  rcases w with ⟨ww,hw⟩,
  dsimp at p,
  induction p with u u v w uav vpw ih,
  { exact walk.nil, },
  { rw walk.contained_cons_iff at pcon,
    have hv : v ∈ H.verts := H.edge_vert (pcon.1).symm,
    refine walk.cons' _ ⟨v,hv⟩ _ _ _,
    simp only [subgraph.coe_adj, subtype.coe_mk],
    exact pcon.1,
    exact ih hv hw pcon.2,},
end

def walk.contained.to_subgraph_map_eq {V : Type*} [decidable_eq V] {G : simple_graph V} (H : G.subgraph)
  {u w : H.verts} (p : G.walk u w) (pcon : p.contained H) :
  (walk.contained.to_subgraph H p pcon).map H.hom = p :=
begin
  rcases u with ⟨uu,hu⟩,
  rcases w with ⟨ww,hw⟩,
  dsimp at p,
  induction p with u u v w uav vpw ih,
  { dsimp [subgraph.hom,walk.contained.to_subgraph], refl, },
  { apply congr_arg2,
    simp only [eq_iff_true_of_subsingleton],
    apply ih,}
end

[Rémi Bottinelli]

(deleted)

[Rémi Bottinelli]

If this is an acceptable path, I think we don't actually need the “pull back along a morphism” part for the specific instance of an induced subgraph. I'm not sure which path is best.

[Rémi Bottinelli]

As for “An injective morphism of graph induces an image subgraph and restricts to an isomorphism between domain and image.”: does that already exist in some form somewhere? I couldn't find anything like that.

[Rémi Bottinelli]

Mmh, that's actually a wrong definition for walk.contained since nil will be contained no matter what…

[Rémi Bottinelli]

A corrected version:

def walk.contained [decidable_eq V] (H : G.subgraph) :
  Π {u v : V} (p : G.walk u v),  Prop
| _ _ (walk.nil' u) := u ∈ H.verts
| _ _ (walk.cons' u v w a p) := H.adj u v  ∧ walk.contained p

@[simp]
lemma walk.contained_cons_iff [decidable_eq V] (H : G.subgraph)
  {u v w : V} (a : G.adj u v) (p : G.walk v w) :
  (walk.cons a p).contained H ↔ (H.adj u v ∧ p.contained H) := by refl

@[simp]
lemma walk.contained_nil_iff [decidable_eq V] (H : G.subgraph)
  {u : V} : (walk.nil' u).contained H ↔ u ∈ H.verts := by refl

lemma walk.contained_verts [decidable_eq V] (H : G.subgraph)
  {u v : V} (p : G.walk u v) : p.contained H → ∀ (w : V), w ∈ p.support → w ∈ H.verts :=
begin
  rintro h,
  induction p,
  { simp, exact h, },
  { simp at h, specialize p_ih h.2,
    intros w wsup,
    rw [walk.support_cons,list.mem_cons_iff] at wsup,
    cases wsup,
    { rw wsup, exact H.edge_vert h.1, },
    { exact p_ih w wsup, },}
end

lemma walk.contained_induced_iff [decidable_eq V] (S : set V) {u v : V} (p : G.walk u v) :
  p.contained ((⊤ : G.subgraph).induce S) ↔ ∀ w ∈ p.support, w ∈ S :=
begin
  split,
  { exact walk.contained_verts _ p, },
  { rintro sub, dsimp only [walk.contained],
    induction p,
    {simp, apply sub, simp, },
    { simp, refine ⟨⟨_,_,p_h⟩,_⟩,
      {apply sub, simp,},
      {apply sub, simp,},
      {apply p_ih, rintro w ws, apply sub, simp, right, exact ws,},
    }},
end

lemma walk.contained_append_left [decidable_eq V] (H : G.subgraph)
  {u v w : V} (p : G.walk u v) (q : G.walk v w) : (p.append q).contained H → p.contained H := sorry

lemma walk.contained_append_right [decidable_eq V] (H : G.subgraph)
  {u v w : V} (p : G.walk u v) (q : G.walk v w) : (p.append q).contained H → p.contained H := sorry

def walk.contained.to_subgraph [decidable_eq V] (H : G.subgraph)
  {u w : H.verts} (p : G.walk u w) (pcon : p.contained H) : H.coe.walk u w :=
begin
  rcases u with ⟨uu,hu⟩,
  rcases w with ⟨ww,hw⟩,
  dsimp at p,
  induction p with u u v w uav vpw ih,
  { exact walk.nil, },
  { rw walk.contained_cons_iff at pcon,
    have hv : v ∈ H.verts := H.edge_vert (pcon.1).symm,
    refine walk.cons' _ ⟨v,hv⟩ _ _ _,
    simp only [subgraph.coe_adj, subtype.coe_mk],
    exact pcon.1,
    exact ih hv hw pcon.2,},
end

def walk.contained.to_subgraph_map_eq [decidable_eq V] (H : G.subgraph)
  {u w : H.verts} (p : G.walk u w) (pcon : p.contained H) :
  (walk.contained.to_subgraph H p pcon).map H.hom = p :=
begin
  rcases u with ⟨uu,hu⟩,
  rcases w with ⟨ww,hw⟩,
  dsimp at p,
  induction p with u u v w uav vpw ih,
  { dsimp [subgraph.hom,walk.contained.to_subgraph], refl, },
  { apply congr_arg2,
    simp only [eq_iff_true_of_subsingleton],
    apply ih,}
end


def walk.to_induced [decidable_eq V] (S : set V)
  {u v : S} (p : G.walk u v) (hp : ∀ w ∈ p.support, w ∈ S) : (G.induce S).walk u v :=
begin
  rw induce_eq_coe_induce_top,
  apply walk.contained.to_subgraph, rotate,
  exact p,
  rw walk.contained_induced_iff,
  exact hp,
end

[Rémi Bottinelli]

OK, I've put it all in a new branch. I think a PR is not in order yet, but hopefully we can get that in shape to get included?