Converse of IsTree.card_edgeFinset

Stream: graph theory

[Elijah Beregovsky]

I want to prove the converse of IsTree.card_edgeFinset -- if the number of edges in a connected graph is one less than the number of its vertices then the graph is a tree. I want to do this by induction on the number of vertices
I'm very new to the language, so I'm struggling with even the basic stuff. Currently the proof is in the following state. Question: how do I remove a vertex from a Graph? Seems to be a very simple operation, but I couldn't find it in Operations, nor was it in Subgraph

import Mathlib.Combinatorics.SimpleGraph.Acyclic
import Mathlib.Combinatorics.SimpleGraph.Path
import Mathlib.Combinatorics.SimpleGraph.Subgraph
import Mathlib.Data.Fintype.Option
import Mathlib

universe u v

namespace SimpleGraph

open Walk

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

theorem isTree_of_singleton [Fintype V] [Fintype G.edgeSet] (hG : Fintype.card V = 1) : G.IsTree := by
  sorry

theorem exists_leaf_vertex_of_card_edgeFinset [Fintype V] [Fintype G.edgeSet]
    (h : G.edgeFinset.card + 1 = Fintype.card V) : ∃ (v : V), ∃! (w : V), G.Adj v w := by
  -- by contradiction using degree sum
  sorry

theorem isTree_of_card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.Connected)
    (h : G.edgeFinset.card + 1 = Fintype.card V) : G.IsTree := by
  set e := G.edgeFinset.card with he
  clear_value e
  induction' e with e ih generalizing V
  · rw[zero_add] at h
    symm at h
    apply isTree_of_singleton at h
    · exact h
    · assumption
  · rw[isTree_iff]
    have hl : ∃ (v : V), ∃! (w : V), G.Adj v w := by
      rw[he] at h
      apply exists_leaf_vertex_of_card_edgeFinset at h
      exact h
    constructor
    · assumption
    · cases hl with | intro v hl =>
      -- Remove leaf from graph
      -- by induction hypothesis resulting graph is a tree
      -- add leaf back, prove it creates no cycles
      -- done
      sorry

[Elijah Beregovsky]

If I'm overcomplicating things and there's a smarter/cleaner way to do this, please tell me!

[Yaël Dillies]

The way you should think about removing a point v : V from a graph is that it's the same as comapping your graph along the injection {w : V // w ≠ v} → V. Can you take it from there?

[Elijah Beregovsky]

Oh yeah! I think I understand now, thanks!

[Alena Gusakov]

Elijah Beregovsky said:

I want to prove the converse of IsTree.card_edgeFinset -- if the number of edges in a connected graph is one less than the number of its vertices then the graph is a tree. I want to do this by induction on the number of vertices
I'm very new to the language, so I'm struggling with even the basic stuff. Currently the proof is in the following state. Question: how do I remove a vertex from a Graph? Seems to be a very simple operation, but I couldn't find it in Operations, nor was it in Subgraph

import Mathlib.Combinatorics.SimpleGraph.Acyclic
import Mathlib.Combinatorics.SimpleGraph.Path
import Mathlib.Combinatorics.SimpleGraph.Subgraph
import Mathlib.Data.Fintype.Option
import Mathlib

universe u v

namespace SimpleGraph

open Walk

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

theorem isTree_of_singleton [Fintype V] [Fintype G.edgeSet] (hG : Fintype.card V = 1) : G.IsTree := by
  sorry

theorem exists_leaf_vertex_of_card_edgeFinset [Fintype V] [Fintype G.edgeSet]
    (h : G.edgeFinset.card + 1 = Fintype.card V) : ∃ (v : V), ∃! (w : V), G.Adj v w := by
  -- by contradiction using degree sum
  sorry

theorem isTree_of_card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.Connected)
    (h : G.edgeFinset.card + 1 = Fintype.card V) : G.IsTree := by
  set e := G.edgeFinset.card with he
  clear_value e
  induction' e with e ih generalizing V
  · rw[zero_add] at h
    symm at h
    apply isTree_of_singleton at h
    · exact h
    · assumption
  · rw[isTree_iff]
    have hl : ∃ (v : V), ∃! (w : V), G.Adj v w := by
      rw[he] at h
      apply exists_leaf_vertex_of_card_edgeFinset at h
      exact h
    constructor
    · assumption
    · cases hl with | intro v hl =>
      -- Remove leaf from graph
      -- by induction hypothesis resulting graph is a tree
      -- add leaf back, prove it creates no cycles
      -- done
      sorry

I will say, I'm currently working on a proof of the existence of a leaf for my own project, also using the degreeSum approach - is there a reason you stated it as "there exists a vertex with a unique neighbor" instead of "there exists a vertex whose degree is 1"?

[Elijah Beregovsky]

Alena Gusakov said:

is there a reason you stated it as "there exists a vertex with a unique neighbor" instead of "there exists a vertex whose degree is 1"?

Not really, for now that lemma is a placeholder, so I might restate it in the future if it turns out the other way is more convenient