Every connected graph has a spanning tree

Stream: graph theory

[Thomas Waring]

Hi all, I proven that every connected graph has a spanning tree (without any finiteness assumption) — see here. I used the opposite idea to the proof that already exists in the finite case, the key lemma is that a maximal acyclic subgraph of a connected graph is connected. An outline is:

import Mathlib.Combinatorics.SimpleGraph.Acyclic

namespace SimpleGraph

variable {V : Type _} {G : SimpleGraph V}

-- this is used to show that, given a non-connected acyclic subgraph `H`, we can find an edge in
-- `G` which connected two connected components of `H`, so that `H ⊔ fromEdgeSet {s(x,y)}` is
-- acyclic (see below `add_edge_acyclic`).
theorem Connected.subset_connected_complement (h : G.Connected) (s : Set V) (hs : s.Nonempty) :
    s = Set.univ ∨ ∃ (u v : V), u ∈ s ∧ v ∉ s ∧ G.Adj u v := sorry

/-- Given a walk in `sSup Hs`, where `Hs` is directed, find `H ∈ Hs` which already contains the
walk. -/
theorem Walk.shrink_of_directed_sSup (Hs : Set <| SimpleGraph V) (H₀ : Hs)
    (h_dir : DirectedOn (· ≤ ·) Hs) {u v : V} (p : (sSup Hs).Walk u v) :
    ∃ H ∈ Hs, ∃ (p' : H.Walk u v),
      p'.edges = p.edges ∧ p'.support = p.support := sorry

/-- The directed (in particular increasing) union of acyclic graphs is acylic. -/
theorem sSup_acyclic_of_directed_of_acyclic (Hs : Set <| SimpleGraph V) (H₀ : Hs)
    (h_acyc : ∀ H ∈ Hs, H.IsAcyclic) (h_dir : DirectedOn (· ≤ ·) Hs) : IsAcyclic (sSup Hs) := by sorry

/-- Adding an edge between two unreachable vertices to an acyclic graph produces
an acyclic graph. -/
theorem add_edge_acyclic [DecidableEq V] {G : SimpleGraph V} (hG : IsAcyclic G) (x y : V)
    (hxy : ¬ Reachable G x y) : IsAcyclic <| G ⊔ fromEdgeSet {s(x,y)} := by sorry

/-- A maximal acyclic subgraph of an acyclic graph is acylic. -/
theorem Connected.connected_of_maximal_acyclic [Inhabited V] (T : SimpleGraph V) (hG : G.Connected)
    (h : Maximal (fun H => H ≤ G ∧ H.IsAcyclic) T) : T.Connected := by sorry

/-- A connected graph has a spanning tree. -/
theorem Connected.has_spanning_tree [Inhabited V] (hG : G.Connected) : ∃ T ≤ G, T.IsTree := by sorry

end SimpleGraph

(I did it this way because it wasn't clear to me how to prove the assumption of Zorn's lemma — that a descending intersection of connected graphs is connected — for the other way.) There's a lot of preparatory lemmas here, so I'm not sure it's appropriate for mathlib, but if it is I'd love any feedback that might help make it PR-ready!

[Aaron Liu]

Can you do the extends version, like what we have with "every vector space has a basis" in docs#LinearIndepOn.extend

[Aaron Liu]

any acyclic subgraph supported on a set s can be extended to an acyclic subgraph maximal among those supported on a set t if s ⊆ t

[Aaron Liu]

actually probably we want s and t to be subgraphs

[Thomas Waring]

the statement “every acyclic subgraph can be extended to a spanning tree” would be straightforward, that’s just swapping to use the version docs#zorn_le_nonempty₀

[Thomas Waring]

& i could certainly refactor it to be something like every acyclic H ≤ G can be extended to a maximal acyclic H’ ≤ G, if that’s what you mean? (& then derive H’ connected later, in the case that G is connected)

[Aaron Liu]

oh yes that's a more consise way to say that

[Thomas Waring]

done :) the full file is here but the new statements look like this:

import Mathlib.Combinatorics.SimpleGraph.Acyclic

namespace SimpleGraph

variable {V : Type _} {G : SimpleGraph V}

theorem exists_maximal_acyclic_extension {H : SimpleGraph V} (hHG : H ≤ G) (hH : H.IsAcyclic) :
    ∃ H' : SimpleGraph V, H ≤ H' ∧ Maximal (fun H => H ≤ G ∧ H.IsAcyclic) H' := sorry

theorem Connected.has_spanning_tree (hG : G.Connected) {H : SimpleGraph V} (hHG : H ≤ G)
  (hH : H.IsAcyclic) : ∃ T ≤ G, H ≤ T ∧ T.IsTree := sorry

end SimpleGraph

[John Talbot]

This looks great!

One small suggestion: you can useWalk.exists_boundary_dart to help with your first lemma above.

theorem Connected.subset_connected_complement (h : G.Connected) (s : Set V) (hs : s.Nonempty) :
    s = Set.univ ∨ ∃ (u v : V), u ∈ s ∧ v ∉ s ∧ G.Adj u v := by
  simp_rw [Classical.or_iff_not_imp_left, Set.ne_univ_iff_exists_notMem]
  intro ⟨v, hv⟩
  obtain ⟨u, hu⟩ := hs
  obtain ⟨p⟩ := h u v
  obtain ⟨d, _, h1, h2⟩ := p.exists_boundary_dart _ hu hv
  exact ⟨_, _, h1, h2, d.adj⟩

[Thomas Waring]

Ahh I thought there must be a better way thank you so much (in fact with that the whole lemma can be inlined for the case I use it)

[Thomas Waring]

One more optimisation: the same argument (intuitively) works for a spanning forest, but I couldn't figure out how to formulate that. I settled on "acyclic subgraph with the same reachability relation", as the most elegant way of stating it, so now the main results are:

import Mathlib.Combinatorics.SimpleGraph.Acyclic

namespace SimpleGraph

variable {V : Type _} {G : SimpleGraph V}

theorem exists_maximal_acyclic_extension {H : SimpleGraph V} (hHG : H ≤ G) (hH : H.IsAcyclic) :
    ∃ H' : SimpleGraph V, H ≤ H' ∧ Maximal (fun H => H ≤ G ∧ H.IsAcyclic) H' := sorry

theorem reachable_eq_of_maximal_acyclic (F : SimpleGraph V)
    (h : Maximal (fun H => H ≤ G ∧ H.IsAcyclic) F) : F.Reachable = G.Reachable := sorry

/-- Every graph has a spanning forest. -/
theorem exists_extension_acyclic_reachable_eq {H : SimpleGraph V} (hHG : H ≤ G)
    (hH : H.IsAcyclic) : ∃ F ≤ G, H ≤ F ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable := sorry

theorem Connected.connected_of_maximal_acyclic (T : SimpleGraph V) (hG : G.Connected)
    (h : Maximal (fun H => H ≤ G ∧ H.IsAcyclic) T) : T.Connected := sorry

theorem Connected.exists_extension_isTree_le (hG : G.Connected) {H : SimpleGraph V} (hHG : H ≤ G)
  (hH : H.IsAcyclic) : ∃ T ≤ G, H ≤ T ∧ T.IsTree := sorry

end SimpleGraph

The full file is still at the same link or (now I learnt this trick) here:

every graph has a spanning forest

import Mathlib.Combinatorics.SimpleGraph.Acyclic

namespace SimpleGraph

variable {V : Type _} {G : SimpleGraph V}

theorem Walk.shrink_of_directed_sSup (Hs : Set <| SimpleGraph V) (H₀ : Hs)

(h_dir : DirectedOn (· ≤ ·) Hs) {u v : V} (p : (sSup Hs).Walk u v) :

∃ H ∈ Hs, ∃ (p' : H.Walk u v),

p'.edges = p.edges ∧ p'.support = p.support := by

induction p with

| nil => refine ⟨H₀, by grind, Walk.nil, by simp⟩

| @cons u v w h_adj p ih =>

obtain ⟨H₁, hH₁, p', hp'⟩ := ih

rw [sSup_adj] at h_adj

replace ⟨H₂, hH₂, h_adj⟩ : ∃ H₂ ∈ Hs, H₂.Adj u v := h_adj

obtain ⟨H, hH, h⟩ := h_dir H₁ hH₁ H₂ hH₂

let p'' : H.Walk v w := Walk.map (Hom.ofLE h.1) p'

have : p''.edges = p'.edges ∧ p''.support = p'.support := by simp [p'']

have : H.Adj u v := by grind [SimpleGraph.le_iff_adj]

exact ⟨H, hH, Walk.cons this p'', by grind [support_cons, edges_cons]⟩

theorem sSup_acyclic_of_directed_of_acyclic (Hs : Set <| SimpleGraph V) (H₀ : Hs)

(h_acyc : ∀ H ∈ Hs, H.IsAcyclic) (h_dir : DirectedOn (· ≤ ·) Hs) : IsAcyclic (sSup Hs) := by

intro u p hp

obtain ⟨H, hH, p', hp'⟩ := p.shrink_of_directed_sSup Hs H₀ h_dir

suffices p'.IsCycle by exact (h_acyc H) hH p' this

rw [Walk.isCycle_def, Walk.isTrail_def] at hp ⊢

refine ⟨by grind, ?_, by grind⟩

rw [ne_eq, ←Walk.nil_iff_eq_nil, Walk.nil_iff_support_eq] at hp ⊢

grind

theorem exists_maximal_acyclic_extension {H : SimpleGraph V} (hHG : H ≤ G) (hH : H.IsAcyclic) :

∃ H' : SimpleGraph V, H ≤ H' ∧ Maximal (fun H => H ≤ G ∧ H.IsAcyclic) H' := by

let s : Set (SimpleGraph V) := {H : SimpleGraph V | H ≤ G ∧ H.IsAcyclic}

apply zorn_le_nonempty₀ s

· intro c hcs hc y hy

refine ⟨sSup c, ⟨?_, ?_⟩, CompleteLattice.le_sSup c⟩

· simp only [sSup_le_iff]

grind

· exact sSup_acyclic_of_directed_of_acyclic c ⟨y, hy⟩ (by grind) hc.directedOn

· grind

theorem add_edge_acyclic [DecidableEq V] {G : SimpleGraph V} (hG : IsAcyclic G) (x y : V)

(hxy : ¬ Reachable G x y) : IsAcyclic <| G ⊔ fromEdgeSet {s(x,y)} := by

have x_neq_y : x ≠ y := fun c => (c ▸ hxy) (Reachable.refl y)

have h_add_remove : G = (G ⊔ fromEdgeSet {s(x,y)}) \ fromEdgeSet {s(x,y)} := by

simp only [sup_sdiff_right_self]

apply edgeSet_inj.mp; ext e;

simp only [edgeSet_sdiff, edgeSet_fromEdgeSet, edgeSet_sdiff_sdiff_isDiag, Set.mem_diff,

Set.mem_singleton_iff, iff_self_and]

intro he c

rw [c, mem_edgeSet] at he

exact hxy <| Adj.reachable he

have h_bridge : (G ⊔ fromEdgeSet {s(x,y)}).IsBridge s(x,y) := by

simpa [isBridge_iff, x_neq_y, ←h_add_remove]

intro u c hc

apply isBridge_iff_adj_and_forall_cycle_notMem.mp at h_bridge

let c' : G.Walk u u := Walk.transfer c G (by

intro e he

have eneq : e ≠ s(x,y) := fun h => h_bridge.2 c hc (h ▸ he)

simpa [eneq] using Walk.edges_subset_edgeSet c he

)

exact hG c' (Walk.IsCycle.transfer (qc := hc) ..)

theorem reachable_eq_of_maximal_acyclic (F : SimpleGraph V)

(h : Maximal (fun H => H ≤ G ∧ H.IsAcyclic) F) : F.Reachable = G.Reachable := by

simp only [Maximal, and_imp] at h

obtain ⟨hF, h⟩ := h

apply funext; intro u; apply funext; intro v

refine propext ⟨fun hr => hr.mono hF.1, ?_⟩

contrapose! h

obtain ⟨p⟩ := h.1

let s : Set V := F.connectedComponentMk u

have hus : u ∈ s := ConnectedComponent.connectedComponentMk_mem

have hvs : v ∉ s := h.2 ∘ (F.connectedComponentMk u).reachable_of_mem_supp hus

obtain ⟨⟨⟨u', v'⟩, huv⟩, _, hu, hv⟩ := p.exists_boundary_dart s hus hvs

let F' := (F ⊔ fromEdgeSet {s(u', v')})

suffices F'.IsAcyclic by

rw [le_iff_adj] at hF

refine ⟨F', ?_, this, le_sup_left, ?_⟩

· have : G.Adj v' u' := G.symm huv

simp only [sup_le_iff, le_iff_adj, fromEdgeSet_adj, Set.mem_singleton_iff, Sym2.eq,

Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk, ne_eq, and_imp, F']

grind

· rw [le_iff_adj]

push_neg

refine ⟨u', v', ?_, ?_⟩

· simp only [sup_adj, fromEdgeSet_adj, Set.mem_singleton_iff, ne_eq, true_and, F']

grind

· intro hc

have : _ := ConnectedComponent.mem_supp_congr_adj (F.connectedComponentMk u) hc

grind

have : DecidableEq V := Classical.decEq V

apply add_edge_acyclic (hG := hF.2)

intro hc

rw [←ConnectedComponent.eq] at hc

suffices F.connectedComponentMk u' = s by

exact (hc ▸ this ▸ hv) ConnectedComponent.connectedComponentMk_mem

simp_rw [s, SetLike.coe, ConnectedComponent.supp_inj, ←ConnectedComponent.mem_supp_iff]

grind

/-- Every graph has a spanning forest. -/

theorem exists_extension_acyclic_reachable_eq {H : SimpleGraph V} (hHG : H ≤ G)

(hH : H.IsAcyclic) : ∃ F ≤ G, H ≤ F ∧ F.IsAcyclic ∧ F.Reachable = G.Reachable := by

obtain ⟨F, hHF, hF⟩ := exists_maximal_acyclic_extension hHG hH

exact ⟨F, hF.1.1, hHF, hF.1.2, reachable_eq_of_maximal_acyclic F hF⟩

theorem Connected.connected_of_maximal_acyclic (T : SimpleGraph V) (hG : G.Connected)

(h : Maximal (fun H => H ≤ G ∧ H.IsAcyclic) T) : T.Connected := by

have : Nonempty V := hG.nonempty

refine ⟨fun u v => ?_⟩

rw [reachable_eq_of_maximal_acyclic T h]

exact hG u v

theorem Connected.exists_extension_isTree_le (hG : G.Connected) {H : SimpleGraph V} (hHG : H ≤ G)

(hH : H.IsAcyclic) : ∃ T ≤ G, H ≤ T ∧ T.IsTree := by

obtain ⟨T, hHT, hT⟩ := exists_maximal_acyclic_extension hHG hH

exact ⟨T, hT.1.1, hHT, hG.connected_of_maximal_acyclic T hT, hT.1.2⟩

end SimpleGraph

[Snir Broshi]

Incredible! For the past few weeks I have been trying to prove the same thing with Zorn's lemma, which seems to take a lot of work:

Code with sorries

import Mathlib
variable {V : Type*} {G : SimpleGraph V}
namespace SimpleGraph

-- from #30757
theorem isTree_coe_singletonSubgraph (G : SimpleGraph V) (v : V) : G.singletonSubgraph v |>.coe.IsTree := sorry
theorem isTree_coe_subgraphOfAdj {u v : V} (h : G.Adj u v) : G.subgraphOfAdj h |>.coe.IsTree := sorry

theorem isAcyclic_coe_sup {G₁ G₂ : G.Subgraph} (h₁ : G₁.coe.IsAcyclic) (h₂ : G₂.coe.IsAcyclic)
    (h : (G₁.verts ∩ G₂.verts).Subsingleton) : (G₁ ⊔ G₂).coe.IsAcyclic :=
  sorry -- TODO (I am very close to a full proof of this)

theorem isTree_coe_sup {G₁ G₂ : G.Subgraph} (h₁ : G₁.coe.IsTree) (h₂ : G₂.coe.IsTree) {v : V}
    (h : G₁.verts ∩ G₂.verts = {v}) : (G₁ ⊔ G₂).coe.IsTree :=
  ⟨Subgraph.connected_sup ⟨h₁.isConnected.preconnected⟩ ⟨h₂.isConnected.preconnected⟩
    <| by simp [h], isAcyclic_coe_sup h₁.IsAcyclic h₂.IsAcyclic <| by simp [h]⟩

-- removing finiteness assumption using Zorn's lemma
theorem Connected.exists_isTree_le' (h : G.Connected) : ∃ T ≤ G, T.IsTree := by
  have ⟨T, hmax⟩ := zorn_le₀ {H : Subgraph G | H.coe.IsTree} fun s hsubset hchain ↦ by
    by_cases hempty : s ⊆ {⊥}
    · have ⟨v⟩ := h.nonempty
      exact ⟨_, G.isTree_coe_singletonSubgraph v, fun _ h ↦ hempty h ▸ OrderBot.bot_le _⟩
    have : Nonempty (sSup s).verts := Set.nonempty_iff_ne_empty'.mpr <|
      Subgraph.eq_bot_iff_verts_eq_empty _ |>.not.mp <| sSup_eq_bot.not.mpr hempty
    refine ⟨sSup s, ⟨⟨fun u v ↦ ?_⟩, fun v p ↦ ?_⟩, CompleteLattice.le_sSup _⟩
    · have ⟨Hu, hHu, hu⟩ := Set.mem_iUnion₂.mp u.prop
      have ⟨Hv, hHv, hv⟩ := Set.mem_iUnion₂.mp v.prop
      have hH := (hchain.total hHu hHv).elim
        (fun h ↦ right_eq_sup.mpr h ▸ hHv) (fun h ↦ left_eq_sup.mpr h ▸ hHu)
      exact Reachable.map (Subgraph.inclusion <| CompleteLattice.le_sSup _ _ hH) <|
        (hsubset hH).isConnected.preconnected
          ⟨u.val, (le_sup_left : Hu.verts ⊆ _) hu⟩
          ⟨v.val, (le_sup_right : Hv.verts ⊆ _) hv⟩
    · sorry -- TODO (induction on `p` but without requiring equal endpoints)
  refine ⟨T.spanningCoe, T.spanningCoe_le,
    (Iso.isTree_iff <| Subgraph.spanningCoeEquivCoeOfSpanning _ ?_).mpr hmax.prop⟩
  by_contra hspan
  have ⟨u, hu⟩ := hmax.prop.isConnected.nonempty
  have ⟨v, hv⟩ := Set.nonempty_compl.mpr <| Subgraph.isSpanning_iff.not.mp hspan
  have ⟨p⟩ := h.preconnected u v
  have ⟨d, hd, hd₁, hd₂⟩ := p.exists_boundary_dart T.verts hu hv
  exact hd₂ <| (le_sup_right.trans <| hmax.le_of_ge (isTree_coe_sup (v := d.fst) hmax.prop
    (isTree_coe_subgraphOfAdj d.adj) <| by grind [subgraphOfAdj]) le_sup_left).right rfl |>.snd_mem

theorem isBridge_iff_reachable_deleteEdges_ne_reachable {e : Sym2 V} :
    G.IsBridge e ↔ (G.deleteEdges {e}).Reachable ≠ G.Reachable := by
  sorry -- TODO

/-- Every connected graph has a full spanning forest. -/
lemma exists_isAcyclic_le [Finite V] : ∃ F ≤ G, F.IsAcyclic ∧ F.Reachable = G.Reachable := by
  -- TODO: can we remove finiteness assumption like `exists_isTree_le`?
  have ⟨F, hFG, hmin⟩ :=
    {H : SimpleGraph V | H.Reachable = G.Reachable}.toFinite.exists_le_minimal rfl
  refine ⟨F, hFG, isAcyclic_iff_forall_adj_isBridge.mpr fun _ _ _ ↦ ?_, hmin.left⟩
  exact by_contra fun hnb ↦ hmin.not_prop_of_lt (by simpa [deleteEdges, ← edgeSet_ssubset_edgeSet])
    <| Classical.not_not.mp (isBridge_iff_reachable_deleteEdges_ne_reachable.not.mp hnb)
      |>.trans hmin.left

(and like you I figured this is a special case of finding an acyclic subgraph with F.Reachable = G.Reachable)

[Thomas Waring]

Hi thanks for taking a look! I think the main difference (& possibly why I found it easier to prove my results) is that I would with G.IsSubgraph aka ≤ whereas you used the type G.Subgraph — my way avoids a lot of coercions which possibly makes life easier, and it seems to me like the API is a bit better developed

[Thomas Waring]

I'll leave a review on you PRs now — I think my first one #32041 (which does all the zorny stuff) is fairly optimised and doesn't really overlap with your results, let me know if you agree? definitely I think we should carry through results from both of our other ones