Auxiliary lemmas for the Nash-Williams–Tutte theorems

General counting lemmas for forests and connected graphs, and the core exchange lemma: for any finite graph G there are k edge-disjoint forests F i ≤ G and a subgraph H ≤ G such that each F i ⊓ H has the same connected components as H, and every edge of G outside H is covered by some F i.

theorem NashWilliamsTutte.reachable_map_of_adj {V : Type u_1} {W : Type u_2} {A : SimpleGraph V} {B : SimpleGraph W} (g : V → W) (h : ∀ (a b : V), A.Adj a b → B.Reachable (g a) (g b)) {a b : V} (hab : A.Reachable a b) : B.Reachable (g a) (g b)

Reachability transfers along a map that sends adjacent vertices to reachable ones.

theorem NashWilliamsTutte.reachable_closed {V : Type u_1} {A : SimpleGraph V} (P : V → Prop) (h : ∀ (a b : V), A.Adj a b → P a → P b) {a b : V} (hab : A.Reachable a b) (ha : P a) : P b

A predicate closed under adjacency is closed under reachability.

theorem NashWilliamsTutte.disjoint_iff_adj {V : Type u_1} {A B : SimpleGraph V} : Disjoint A B ↔ ∀ (a b : V), A.Adj a b → ¬B.Adj a b

Disjointness of simple graphs in terms of adjacency.

theorem NashWilliamsTutte.sum_ncard_le_of_pairwise_disjoint {ι : Type u_2} {α : Type u_3} [Fintype ι] [Finite α] (A : ι → Set α) (B : Set α) (hAB : ∀ (i : ι), A i ⊆ B) (hd : Pairwise (Function.onFun Disjoint A)) : ∑ i : ι, (A i).ncard ≤ B.ncard

The sum of the sizes of pairwise disjoint subsets of a finite set is at most its size.

theorem NashWilliamsTutte.IsAcyclic.ncard_edgeSet_add_one_le {V : Type u_1} [Finite V] [Nonempty V] {F : SimpleGraph V} (hF : F.IsAcyclic) : F.edgeSet.ncard + 1 ≤ Nat.card V ∧ (Nat.card V ≤ F.edgeSet.ncard + 1 → F.IsTree)

A forest on a finite nonempty vertex type has at most |V| - 1 edges, and exactly |V| - 1 only if it is a tree.

theorem NashWilliamsTutte.card_le_ncard_edgeSet_add_card_image {V : Type u_1} [Fintype V] [DecidableEq V] [Nonempty V] (K : SimpleGraph V) (f : V → V) (hf : ∀ (v : V), K.Reachable v (f v)) : Nat.card V ≤ K.edgeSet.ncard + (Finset.image f Finset.univ).card

If every vertex v is reachable in K from f v, then K has at least |V| - #(image f) edges.

theorem NashWilliamsTutte.card_image_le_ncard_crossing_add_one {V : Type u_1} [Fintype V] [DecidableEq V] {T : SimpleGraph V} (hT : T.Connected) (f : V → V) : (Finset.image f Finset.univ).card ≤ (T.edgeSet ∩ (SimpleGraph.comap f ⊤).edgeSet).ncard + 1

A connected graph has at least m - 1 edges joining different fibres of f, where m is the number of nonempty fibres.

theorem NashWilliamsTutte.not_reachable_deleteEdges_of_mem_edges {V : Type u_1} {F : SimpleGraph V} (hF : F.IsAcyclic) {u v x y : V} (p : F.Walk u v) (hp : p.IsPath) (he : s(x, y) ∈ p.edges) : ¬(F.deleteEdges {s(x, y)}).Reachable u v

Deleting an edge of the unique path between u and v in a forest disconnects u from v.

def NashWilliamsTutte.ValidForests {V : Type u_1} (G : SimpleGraph V) {k : ℕ} (F : Fin k → SimpleGraph V) : Prop

k pairwise edge-disjoint forests in G.

Equations

• NashWilliamsTutte.ValidForests G F = ((∀ (i : Fin k), F i ≤ G ∧ (F i).IsAcyclic) ∧ Pairwise fun (i j : Fin k) => Disjoint (F i) (F j))

noncomputable def NashWilliamsTutte.totalEdges {V : Type u_1} {k : ℕ} (F : Fin k → SimpleGraph V) : ℕ

The total number of edges of a family of graphs.

Equations

• NashWilliamsTutte.totalEdges F = ∑ i : Fin k, (F i).edgeSet.ncard

def NashWilliamsTutte.Uncovered {V : Type u_1} (G : SimpleGraph V) {k : ℕ} (F : Fin k → SimpleGraph V) (u v : V) : Prop

uv is an edge of G not covered by the family F.

Equations

• NashWilliamsTutte.Uncovered G F u v = (G.Adj u v ∧ ∀ (j : Fin k), ¬(F j).Adj u v)

def NashWilliamsTutte.ExchangeStep {V : Type u_1} (G : SimpleGraph V) {k : ℕ} (F F' : Fin k → SimpleGraph V) : Prop

One exchange step: an uncovered edge uv replaces an edge xy of some F i, keeping it acyclic.

Equations

• One or more equations did not get rendered due to their size.

theorem NashWilliamsTutte.total_update {V : Type u_1} {k : ℕ} (F : Fin k → SimpleGraph V) (i : Fin k) (X : SimpleGraph V) : totalEdges (Function.update F i X) + (F i).edgeSet.ncard = totalEdges F + X.edgeSet.ncard

theorem NashWilliamsTutte.Uncovered.adj_iff {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {F : Fin k → SimpleGraph V} {u v : V} (h : Uncovered G F u v) {j : Fin k} {a b : V} (hab : s(a, b) = s(u, v)) : ¬(F j).Adj a b

theorem NashWilliamsTutte.adj_new {V : Type u_1} {F : SimpleGraph V} {x y u v a b : V} (h : (F.deleteEdges {s(x, y)} ⊔ SimpleGraph.edge u v).Adj a b) : F.Adj a b ∧ s(a, b) ≠ s(x, y) ∨ s(a, b) = s(u, v)

theorem NashWilliamsTutte.ValidForests.update {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {F : Fin k → SimpleGraph V} (hF : ValidForests G F) (i : Fin k) {X : SimpleGraph V} (hXG : X ≤ G) (hX : X.IsAcyclic) (hXadj : ∀ (a b : V), X.Adj a b → (F i).Adj a b ∨ ∀ (j : Fin k), ¬(F j).Adj a b) : ValidForests G (Function.update F i X)

Replacing F i by a graph X ≤ G whose edges are edges of F i or uncovered edges keeps the family valid, provided X is acyclic.

theorem NashWilliamsTutte.ExchangeStep.valid {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {F F' : Fin k → SimpleGraph V} (hF : ValidForests G F) (h : ExchangeStep G F F') : ValidForests G F'

theorem NashWilliamsTutte.ExchangeStep.total_eq {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Finite V] {F F' : Fin k → SimpleGraph V} (h : ExchangeStep G F F') : totalEdges F' = totalEdges F

theorem NashWilliamsTutte.reachable_of_uncovered {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Finite V] {F : Fin k → SimpleGraph V} (hF : ValidForests G F) (hmax : ∀ (F' : Fin k → SimpleGraph V), ValidForests G F' → totalEdges F' ≤ totalEdges F) {u v : V} (huv : Uncovered G F u v) (i : Fin k) : (F i).Reachable u v

In a family with the maximum total number of edges, the endpoints of an uncovered edge are joined in every forest.

theorem NashWilliamsTutte.ExchangeStep.uncovered {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {F : Fin k → SimpleGraph V} (hF : ValidForests G F) {i : Fin k} {u v x y : V} (huv : Uncovered G F u v) (hxy : (F i).Adj x y) : Uncovered G (Function.update F i ((F i).deleteEdges {s(x, y)} ⊔ SimpleGraph.edge u v)) x y

def NashWilliamsTutte.exchangeGraph {V : Type u_1} {k : ℕ} (G : SimpleGraph V) (F₀ : Fin k → SimpleGraph V) : SimpleGraph V

The graph of all edges of G that are uncovered in some family obtained from F₀ by a sequence of exchange steps.

Equations

• One or more equations did not get rendered due to their size.

theorem NashWilliamsTutte.exchangeGraph_adj {V : Type u_1} {G : SimpleGraph V} {k : ℕ} {F₀ : Fin k → SimpleGraph V} {a b : V} : (exchangeGraph G F₀).Adj a b ↔ ∃ (F : Fin k → SimpleGraph V), Relation.ReflTransGen (ExchangeStep G) F₀ F ∧ Uncovered G F a b

theorem NashWilliamsTutte.reach_valid {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Finite V] {F₀ : Fin k → SimpleGraph V} (hF₀ : ValidForests G F₀) {F : Fin k → SimpleGraph V} (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) : ValidForests G F ∧ totalEdges F = totalEdges F₀

theorem NashWilliamsTutte.reach_uncovered_reachable {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Finite V] {F₀ : Fin k → SimpleGraph V} (hF₀ : ValidForests G F₀) (hmax : ∀ (F : Fin k → SimpleGraph V), ValidForests G F → totalEdges F ≤ totalEdges F₀) {F : Fin k → SimpleGraph V} (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) {u v : V} (huv : Uncovered G F u v) (i : Fin k) : (F i ⊓ exchangeGraph G F₀).Reachable u v

theorem NashWilliamsTutte.step_reachable_iff {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Finite V] {F₀ : Fin k → SimpleGraph V} (hF₀ : ValidForests G F₀) (hmax : ∀ (F : Fin k → SimpleGraph V), ValidForests G F → totalEdges F ≤ totalEdges F₀) {F F' : Fin k → SimpleGraph V} (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) (hstep : ExchangeStep G F F') (j : Fin k) (a b : V) : (F j ⊓ exchangeGraph G F₀).Reachable a b ↔ (F' j ⊓ exchangeGraph G F₀).Reachable a b

theorem NashWilliamsTutte.reach_reachable_iff {V : Type u_1} {G : SimpleGraph V} {k : ℕ} [Finite V] {F₀ : Fin k → SimpleGraph V} (hF₀ : ValidForests G F₀) (hmax : ∀ (F : Fin k → SimpleGraph V), ValidForests G F → totalEdges F ≤ totalEdges F₀) {F : Fin k → SimpleGraph V} (hF : Relation.ReflTransGen (ExchangeStep G) F₀ F) (j : Fin k) (a b : V) : (F j ⊓ exchangeGraph G F₀).Reachable a b ↔ (F₀ j ⊓ exchangeGraph G F₀).Reachable a b

theorem NashWilliamsTutte.exists_forests_core {V : Type u_1} [Finite V] (G : SimpleGraph V) (k : ℕ) : ∃ (F : Fin k → SimpleGraph V) (H : SimpleGraph V), (∀ (i : Fin k), F i ≤ G ∧ (F i).IsAcyclic) ∧ (Pairwise fun (i j : Fin k) => Disjoint (F i) (F j)) ∧ H ≤ G ∧ (∀ (i : Fin k) (a b : V), H.Reachable a b → (F i ⊓ H).Reachable a b) ∧ ∀ (a b : V), G.Adj a b → ¬H.Adj a b → ∃ (i : Fin k), (F i).Adj a b

Core exchange lemma. For every finite graph G there are k pairwise edge-disjoint forests F i ≤ G and a subgraph H ≤ G such that each F i ⊓ H has the same connected components as H, and every edge of G outside H belongs to some F i.