Tree characterisation

Stream: Is there code for X?

[Oliver Nash]

Does anyone have a proof of the converse to docs#SimpleGraph.IsTree.card_edgeFinset anywhere? I briefly looked in a couple likely locations (including LeanCamCombi) but I didn't find it.

[Oliver Nash]

More precisely, I'm looking for a proof of the following sorry:

import Mathlib.Combinatorics.SimpleGraph.Acyclic
import Mathlib.SetTheory.Cardinal.Finite

variable {V : Type*} (G : SimpleGraph V)

lemma SimpleGraph.isTree_iff_connected_and_card [Finite V] :
    G.IsTree ↔ G.Connected ∧ Nat.card G.edgeSet + 1 = Nat.card V := by
  refine ⟨fun h ↦ ⟨h.isConnected, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  · have : Fintype V := Fintype.ofFinite V
    have : Fintype G.edgeSet := Fintype.ofFinite G.edgeSet
    simpa using h.card_edgeFinset
  · sorry

[Kyle Miller]

It would be neat if we had an even more general theorem. These are the parts:

• We already have the number of components: Nat.card G.ConnectedComponent
• We need the dimension of the cycle space. I think that's the dimension of the nullspace of G.incMatrix (ZMod 2)
• Then the general theorem is that (as integers) Nat.card V - Nat.card G.edgeSet = Nat.card G.ConnectedComponent - G.cycleDim (Euler characteristic for graphs)

Then we'd want G.IsAcyclic <-> G.cycleDim = 0 and G.Connected <-> Nat.card G.ConnectedComponent = 1. Putting these all together, SimpleGraph.isTree_iff_connected_and_card follows.

[Oliver Nash]

The above is a great plan, which I’d love to see implemented.

However a direct proof of the tree characterisation would still be a perfectly good contribution.

[Kyle Miller]

No objections there. It's unclear to me that it's that much easier to avoid the more general theorem!

Maybe it's not so bad; we'd need that G.Connected implies Nat.card G.edgeSet + 1 >= Nat.card V and that adding an edge to a tree makes it non-acyclic. This could be organized using a characterization that trees are the minimal connected graphs in the SimpleGraph V lattice.

[Bhavik Mehta]

I (independently) thought about similar things a while ago, and suggested it to a student, so after the coursework deadline has passed, stuff making this easier should appear in PRs!

[Peter Nelson]

I think the stuff Kyle is talking about should wait for multigraphs (in fact, it's all matroidal; G.cycleDim is the rank of the dual graphic matroid of the G over ZMod 2, and this makes sense for any binary matroid).
Going too far down this road just for simple graphs will mean having to start from scratch later.
For instance, this theory interacts beautifully with edge-contractions, and simple graphs won't be enough to state that properly.

My PhD student is working on multigraphs now! Hopefully we'll be able to PR a reasonable definition before too long.

[Peter Nelson]

import Mathlib.Combinatorics.SimpleGraph.Acyclic
import Mathlib.SetTheory.Cardinal.Finite
import Mathlib.Data.Set.Card
import Mathlib.Data.Fintype.Order

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

/-- Deleting a non-bridge edge from a connected graph preserves connectedness. -/
lemma SimpleGraph.Connected.connected_del_of_not_isBridge (hG : G.Connected) {x y : V}
    (h : ¬ G.IsBridge s(x, y)) : (G \ fromEdgeSet {s(x, y)}).Connected := by
  classical
  simp only [isBridge_iff, not_and, not_not] at h
  obtain hxy | hxy := em' <| G.Adj x y
  · rwa [Disjoint.sdiff_eq_left (by simpa)]
  refine (connected_iff_exists_forall_reachable _).2 ⟨x, fun w ↦ ?_⟩
  obtain ⟨W⟩ := (hG.preconnected w x)
  let P := W.toPath
  obtain heP | heP := em' <| s(x,y) ∈ P.1.edges
  · exact ⟨(P.1.toDeleteEdges {s(x,y)} (by aesop)).reverse⟩
  have hyP := P.1.snd_mem_support_of_mem_edges heP
  set P₁ := P.1.takeUntil y hyP with hP₁
  have hxP₁ := Walk.endpoint_not_mem_support_takeUntil P.2 hyP hxy.ne
  have heP₁ : s(x,y) ∉ P₁.edges := fun h ↦ hxP₁ <| P₁.fst_mem_support_of_mem_edges h
  refine (h hxy).trans (Reachable.symm ⟨P₁.toDeleteEdges {s(x,y)} (by aesop)⟩)

/-- A minimally connected graph is a tree. -/
lemma SimpleGraph.isTree_of_minimal_connected (h : Minimal SimpleGraph.Connected G) :
    SimpleGraph.IsTree G := by
  rw [isTree_iff, and_iff_right h.prop, isAcyclic_iff_forall_adj_isBridge]
  refine fun v w hvw ↦ by_contra fun hbr ↦ ?_
  refine h.not_prop_of_lt ?_ (h.prop.connected_del_of_not_isBridge hbr)
  rw [← edgeSet_ssubset_edgeSet]
  simpa

/-- Every connected graph on `n` vertices has at least `n-1` edges. -/
lemma SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one [Fintype V] (hG : G.Connected) :
    Nat.card V ≤ Nat.card G.edgeSet + 1 := by
  classical
  obtain ⟨T, hTG, hmin⟩ := {H : SimpleGraph V | H.Connected}.toFinite.exists_minimal_le hG
  have hT : T.IsTree := isTree_of_minimal_connected hmin
  rw [Nat.card_eq_fintype_card, ← hT.card_edgeFinset, Set.Nat.card_coe_set_eq,
    ← Set.ncard_coe_Finset, add_le_add_iff_right]
  exact Set.ncard_mono <| by simpa

lemma SimpleGraph.isTree_iff_connected_and_card [Fintype V] :
    G.IsTree ↔ G.Connected ∧ Nat.card G.edgeSet + 1 = Nat.card V := by
  classical
  refine ⟨fun h ↦ ⟨h.isConnected, by simpa using h.card_edgeFinset⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
  simp_rw [isAcyclic_iff_forall_adj_isBridge]
  refine fun x y h ↦ by_contra fun hbr ↦ ?_
  refine (h₁.connected_del_of_not_isBridge hbr).card_vert_le_card_edgeSet_add_one.not_lt ?_
  simp only [← h₂, edgeSet_sdiff, edgeSet_fromEdgeSet, edgeSet_sdiff_sdiff_isDiag,
    add_lt_add_iff_right, Set.Nat.card_coe_set_eq]
  exact Set.ncard_diff_singleton_lt_of_mem h

[Peter Nelson]

That was fun! I've never really dived into SimpleGraph, but it looks like there are still a few API lemmas lacking.

[Oliver Nash]

Thanks so much for doing this. Please ping me on the PR :)

[Peter Nelson]

#23399 - I have also included a few TODOs. In particular, I had to prove the bridge lemma 'backwards' because of the lack of a dropUntil version of Walk.endpoint_not_mem_support_takeUntil, which is just part of a general lack of API for dropUntil.

Also some of my lemmas are true in the converse, but I am consciously avoiding spending too much time with SimpleGraph, because it will swallow me up if I do. So I'll leave it there with that PR.

[Peter Nelson]

Regarding TODOs, I see the point about clutter. But at the same time I think there should be a way to record them. Is a TODO section in the module docstring better than individual lemma docstrings?

[Oliver Nash]

If you want to keep them (which is fine) then I think where you put them is best.

[Peter Nelson]

Ok, I've addressed your comments, and just removed the TODOs. I've also added some API to extract paths from proofs of connectedness/reachability without diving into Connected -> Preconnected -> Reachable defeq.

[Peter Nelson]

edit : never mind

[Kim Morrison]

(General note: TODOs and "Future work" sections in module docs are great. I would encourage -- although there's no clear policy on this -- people to write their name somewhere associated with TODOs, so years later there is someone to guilt-trip if they are still there. :-)