Clique trees and minimal separators

SimpleGraph.CliqueTree.branch_separator shows that the intersection bag i ∩ bag j of two bags joined by a tree edge separates the branch below i from the rest of the graph. This file proves that these intersections are exactly the minimal separators of the graph.

Main results

• SimpleGraph.CliqueTree.separates_bag_inter — the separation statement in the form used below
• SimpleGraph.CliqueTree.isMinimalSeparator_bag_inter — for a clique tree whose bags are the maximal cliques (pairwise distinct), the intersection along a tree edge is a minimal separator
• SimpleGraph.CliqueTree.exists_parent_eq_of_isMinimalSeparator — conversely, every minimal separator of two vertices joined by a walk is such an intersection

Both hypotheses are shown to be necessary: SimpleGraph.CliqueTree.not_exists_isMinimalSeparator_dupBagTree refutes the direct statement for a clique tree with repeated maximal bags, and SimpleGraph.CliqueTree.not_exists_parent_eq_isolatedTree refutes the converse for a disconnected graph.

theorem SimpleGraph.CliqueTree.separates_bag_inter {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} [DecidableEq V] {i j : ι} (hp : T.parent i = some j) {a b : V} (ha : a ∈ T.branch i) (hb : b ∉ T.branch i) (haS : a ∉ T.bag i ∩ T.bag j) (hbS : b ∉ T.bag i ∩ T.bag j) : G.Separates (↑(T.bag i ∩ T.bag j)) a b

Separation by a tree edge. If a lies in the branch below i and b does not, and neither lies in the separator bag i ∩ bag j of the tree edge i → j, then that separator separates a from b.

theorem SimpleGraph.CliqueTree.isMinimalSeparator_bag_inter {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Fintype V] [DecidableEq V] (T : G.CliqueTree ι) (hmax : ∀ (i : ι), G.IsMaximalCliqueOn Finset.univ (T.bag i)) (hinj : Function.Injective T.bag) {i j : ι} (hp : T.parent i = some j) : ∃ (a : V) (b : V), G.IsMinimalSeparator (↑(T.bag i ∩ T.bag j)) a b

The separator of a tree edge is a minimal separator, for a clique tree whose bags are the maximal cliques of G, each occurring once.

The converse: every minimal separator is the intersection of two adjacent bags

theorem SimpleGraph.CliqueTree.exists_parent_eq_of_isMinimalSeparator {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Finite V] [DecidableEq V] (T : G.CliqueTree ι) {S : Set V} {a b : V} (hS : G.IsMinimalSeparator S a b) (hreach : G.Reachable a b) : ∃ (i : ι) (j : ι), T.parent i = some j ∧ S = ↑(T.bag i ∩ T.bag j)

Every minimal separator of a clique tree is the intersection of two adjacent bags.

No maximality of the bags is needed here. The hypothesis that a and b are joined by a walk cannot be dropped: in a disconnected graph the empty set is a minimal separator of two vertices of different components, while the clique forest may have no tree edge at all.

The maximality and injectivity hypotheses are needed

The direct statement fails for a clique tree whose bags are maximal cliques but are allowed to repeat: below, a one-vertex graph is given a two-node clique tree with the same bag twice, so the separator of its unique tree edge is the whole vertex set and separates nothing.

def SimpleGraph.CliqueTree.dupBagTree : ⊥.CliqueTree Bool

A clique tree of the one-vertex graph with two nodes carrying the same (maximal) bag.

Equations

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

theorem SimpleGraph.CliqueTree.not_exists_isMinimalSeparator_dupBagTree : (∀ (i : Bool), ⊥.IsMaximalCliqueOn Finset.univ (dupBagTree.bag i)) ∧ dupBagTree.parent true = some false ∧ ¬∃ (a : Unit) (b : Unit), ⊥.IsMinimalSeparator (↑(dupBagTree.bag true ∩ dupBagTree.bag false)) a b

Injectivity of the bags cannot be dropped from isMinimalSeparator_bag_inter. All the bags of dupBagTree are maximal cliques, but the separator of its tree edge is the whole vertex set, hence separates no pair of vertices.

Connectivity is needed in the converse

In a disconnected graph the empty set is a minimal separator of two vertices of distinct components, while a clique forest need not have any tree edge at all.

def SimpleGraph.CliqueTree.isolatedTree : ⊥.CliqueTree Bool

Two isolated vertices, each in its own bag, with no tree edge.

Equations

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

theorem SimpleGraph.CliqueTree.not_exists_parent_eq_isolatedTree : (∀ (i : Bool), ⊥.IsMaximalCliqueOn Finset.univ (isolatedTree.bag i)) ∧ ⊥.IsMinimalSeparator ∅ true false ∧ ¬∃ (i : Bool) (j : Bool), isolatedTree.parent i = some j ∧ ∅ = ↑(isolatedTree.bag i ∩ isolatedTree.bag j)

The walk hypothesis cannot be dropped from exists_parent_eq_of_isMinimalSeparator. All the bags of isolatedTree are maximal cliques and ∅ is a minimal separator of its two vertices, but the forest has no tree edge.