## Stream: graph theory

### Topic: Union of connected subgraphs

#### Rémi Bottinelli (Aug 22 2022 at 06:50):

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 (Aug 22 2022 at 06:52):

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 (Aug 22 2022 at 06:53):

docs#simple_graph.subgraph.induce

#### Rémi Bottinelli (Aug 22 2022 at 06:55):

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 (Aug 22 2022 at 08:49):

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,
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,
{ 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 (Aug 22 2022 at 19:28):

@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⟩,
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 (Aug 22 2022 at 19:32):

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 (Aug 22 2022 at 19:43):

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 (Aug 23 2022 at 06:18):

Thanks! Where should the copy part live?

#### Rémi Bottinelli (Aug 23 2022 at 07:23):

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 (Aug 23 2022 at 07:56):

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


(deleted)

#### Rémi Bottinelli (Aug 23 2022 at 08:14):

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 (Aug 23 2022 at 08:18):

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 (Aug 23 2022 at 10:10):

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

#### Rémi Bottinelli (Aug 23 2022 at 11:23):

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⟩ _ _ _,
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 (Aug 23 2022 at 12:39):

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?

Last updated: Dec 20 2023 at 11:08 UTC