Clique trees (rooted clique forests) of a finite graph

This file introduces a reusable, Mathlib-style structure for clique trees: tree decompositions whose bags are cliques of the ambient graph, presented in rooted form. A rooted presentation is carried by a partial parent function together with a strictly decreasing rank, which makes the whole ancestor calculus available by well-founded recursion and turns the running-intersection property into a single local climb condition.

The structure is deliberately independent of chordality: this file develops the general API, and the companion files construct clique trees of chordal graphs (from a perfect elimination order, and with maximal-clique bags).

Main definitions

• SimpleGraph.CliqueTree — a rooted clique forest for G: clique bags, a parent function with strictly decreasing rank, a distinguished top node top v for every vertex, edge covering, and the local climb condition.
• SimpleGraph.CliqueTree.IsAncestor — reflexive-transitive closure of parent.
• SimpleGraph.CliqueTree.IsLeaf — a node that is nobody's parent.
• SimpleGraph.CliqueTree.privateVerts — vertices occurring in exactly one bag.
• SimpleGraph.CliqueTree.branch — the set of vertices covered by the subtree below a node.
• SimpleGraph.CliqueTree.edgeBag — the canonical bag assigned to an edge.

Main results

• SimpleGraph.CliqueTree.mem_bag_of_isAncestor — intersection property: the nodes whose bag contains a fixed vertex form a connected (upward closed until top v) part of the forest.
• SimpleGraph.CliqueTree.branch_separator — branch separation: for a tree edge i → j, the intersection bag i ∩ bag j separates the branch below i from the rest of the graph.
• SimpleGraph.CliqueTree.isSimplicial_of_mem_privateVerts — a vertex lying in a single bag is simplicial.
• SimpleGraph.CliqueTree.exists_bag_ne_of_isLeaf — leaf elimination: after deleting a leaf, every edge not incident to a private vertex of that leaf is still covered.
• SimpleGraph.CliqueTree.existsUnique_edgeBag — unique edge assignment: every edge belongs to a unique deepest bag.
• SimpleGraph.CliqueTree.card_edgeFinset_eq_sum_fiber — accounting: the edges of G are partitioned by their assigned bags.

structure SimpleGraph.CliqueTree {V : Type u_1} (G : SimpleGraph V) (ι : Type u_2) : Type (max u_1 u_2)

A clique tree (rooted clique forest) of G indexed by ι.

bag i are cliques of G covering all vertices and all edges; parent organises the nodes into a rooted forest (made acyclic by the strictly decreasing rank); top v is the highest node whose bag contains v, and mem_bag_parent is the local form of the running-intersection property: a bag containing v which is not top v passes v on to its parent.

• bag : ι → Finset V

  The bag (clique) attached to a node.

• parent : ι → Option ι

  The parent of a node, none at a root.

• rank : ι → ℕ

  A rank witnessing acyclicity; it also distinguishes nodes.

• top : V → ι

  The top node of a vertex: the highest bag containing it.

• rank_injective : Function.Injective self.rank

  Distinct nodes have distinct ranks.

• rank_parent_lt {i j : ι} : self.parent i = some j → self.rank j < self.rank i

  The rank strictly decreases towards the root.

• bag_isClique (i : ι) : G.IsClique ↑(self.bag i)

  Every bag is a clique.

• mem_bag_top (v : V) : v ∈ self.bag (self.top v)

  Every vertex lies in its own top bag.

• exists_bag_of_adj {u v : V} : G.Adj u v → ∃ (i : ι), u ∈ self.bag i ∧ v ∈ self.bag i

  Every edge lies in some bag.

• mem_bag_parent {i : ι} {v : V} : v ∈ self.bag i → i ≠ self.top v → ∃ (j : ι), self.parent i = some j ∧ v ∈ self.bag j

  Local running-intersection property.

theorem SimpleGraph.CliqueTree.exists_mem_bag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) (v : V) : ∃ (i : ι), v ∈ T.bag i

Every vertex lies in some bag.

def SimpleGraph.CliqueTree.IsAncestor {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) (i j : ι) : Prop

T.IsAncestor i j means that j occurs on the chain of parents starting at i (inclusively).

Equations

• T.IsAncestor i j = Relation.ReflTransGen (fun (a b : ι) => T.parent a = some b) i j

theorem SimpleGraph.CliqueTree.isAncestor_refl {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} (i : ι) : T.IsAncestor i i

theorem SimpleGraph.CliqueTree.IsAncestor.trans {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i j k : ι} (h₁ : T.IsAncestor i j) (h₂ : T.IsAncestor j k) : T.IsAncestor i k

theorem SimpleGraph.CliqueTree.isAncestor_parent {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i j : ι} (h : T.parent i = some j) : T.IsAncestor i j

theorem SimpleGraph.CliqueTree.IsAncestor.rank_le {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i j : ι} (h : T.IsAncestor i j) : T.rank j ≤ T.rank i

theorem SimpleGraph.CliqueTree.IsAncestor.antisymm {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i j : ι} (h₁ : T.IsAncestor i j) (h₂ : T.IsAncestor j i) : i = j

The ancestor relation is antisymmetric.

theorem SimpleGraph.CliqueTree.IsAncestor.comparable {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i j k : ι} (h₁ : T.IsAncestor i j) (h₂ : T.IsAncestor i k) : T.IsAncestor j k ∨ T.IsAncestor k j

Ancestors of a fixed node are linearly ordered.

theorem SimpleGraph.CliqueTree.isAncestor_top_of_mem_bag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i : ι} {v : V} (h : v ∈ T.bag i) : T.IsAncestor i (T.top v)

Following parents from any bag containing v eventually reaches T.top v.

theorem SimpleGraph.CliqueTree.mem_bag_of_isAncestor {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i j : ι} {v : V} (hv : v ∈ T.bag i) (hij : T.IsAncestor i j) (hj : T.IsAncestor j (T.top v)) : v ∈ T.bag j

Intersection property. If v lies in the bag of i, then it lies in the bag of every node between i and T.top v.

def SimpleGraph.CliqueTree.IsLeaf {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) (i : ι) : Prop

A leaf of the clique forest: a node which is nobody's parent.

Equations

• T.IsLeaf i = ∀ (j : ι), T.parent j ≠ some i

theorem SimpleGraph.CliqueTree.eq_of_isAncestor_of_isLeaf {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i k : ι} (hleaf : T.IsLeaf i) (h : T.IsAncestor k i) : k = i

theorem SimpleGraph.CliqueTree.exists_isLeaf {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Finite ι] [Nonempty ι] (T : G.CliqueTree ι) : ∃ (i : ι), T.IsLeaf i

A finite nonempty clique forest has a leaf.

def SimpleGraph.CliqueTree.privateVerts {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) (i : ι) : Set V

The vertices occurring in exactly one bag, namely in the bag of i.

Equations

• T.privateVerts i = {v : V | v ∈ T.bag i ∧ ∀ (k : ι), v ∈ T.bag k → k = i}

theorem SimpleGraph.CliqueTree.mem_privateVerts_iff {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i : ι} {v : V} : v ∈ T.privateVerts i ↔ v ∈ T.bag i ∧ ∀ (k : ι), v ∈ T.bag k → k = i

theorem SimpleGraph.CliqueTree.isSimplicial_of_mem_privateVerts {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i : ι} {v : V} (hv : v ∈ T.privateVerts i) : G.IsSimplicial v

A vertex lying in a single bag is simplicial: all of its neighbours are in that bag, which is a clique.

theorem SimpleGraph.CliqueTree.exists_bag_ne_of_isLeaf {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i : ι} (hleaf : T.IsLeaf i) {x y : V} (hadj : G.Adj x y) (hx : x ∉ T.privateVerts i) (hy : y ∉ T.privateVerts i) : ∃ (k : ι), k ≠ i ∧ x ∈ T.bag k ∧ y ∈ T.bag k

Leaf elimination. Every edge whose endpoints are not private to a leaf i is covered by a bag different from i; hence deleting the leaf together with its private vertices leaves a covered graph.

def SimpleGraph.CliqueTree.branch {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) (i : ι) : Set V

The set of vertices covered by the subtree hanging below i.

Equations

• T.branch i = {v : V | ∃ (j : ι), T.IsAncestor j i ∧ v ∈ T.bag j}

theorem SimpleGraph.CliqueTree.mem_branch_self {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i : ι} {v : V} (h : v ∈ T.bag i) : v ∈ T.branch i

theorem SimpleGraph.CliqueTree.branch_separator {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {i j : ι} (hp : T.parent i = some j) {x y : V} (hadj : G.Adj x y) (hx : x ∈ T.branch i) (hy : y ∉ T.branch i) : x ∈ T.bag i ∧ x ∈ T.bag j

Branch separation. For a tree edge i → j, every G-edge leaving the branch below i does so through the separator bag i ∩ bag j.

theorem SimpleGraph.CliqueTree.not_adj_of_branch_separator {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} [DecidableEq V] {i j : ι} (hp : T.parent i = some j) {x y : V} (hx : x ∈ T.branch i) (hxs : x ∉ T.bag i ∩ T.bag j) (hy : y ∉ T.branch i) : ¬G.Adj x y

The separator of a tree edge disconnects: no G-edge joins the branch below i (minus the separator) to the outside of that branch.

Unique edge assignment and accounting

noncomputable def SimpleGraph.CliqueTree.edgeBag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) (e : Sym2 V) : ι

The canonical bag of an edge: the deeper of the two top bags of its endpoints.

Equations

• T.edgeBag e = Sym2.lift ⟨fun (x y : V) => if T.rank (T.top x) ≤ T.rank (T.top y) then T.top y else T.top x, ⋯⟩ e

theorem SimpleGraph.CliqueTree.edgeBag_mk {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} (x y : V) : T.edgeBag s(x, y) = if T.rank (T.top x) ≤ T.rank (T.top y) then T.top y else T.top x

theorem SimpleGraph.CliqueTree.existsUnique_edgeBag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {x y : V} (hadj : G.Adj x y) : ∃! i : ι, x ∈ T.bag i ∧ y ∈ T.bag i ∧ ∀ (k : ι), x ∈ T.bag k → y ∈ T.bag k → T.IsAncestor k i

Unique edge assignment. Every edge lies in a unique bag below all bags containing it.

theorem SimpleGraph.CliqueTree.mem_bag_edgeBag {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} {T : G.CliqueTree ι} {x y : V} (hadj : G.Adj x y) : x ∈ T.bag (T.edgeBag s(x, y)) ∧ y ∈ T.bag (T.edgeBag s(x, y))

The canonical bag of an edge contains both of its endpoints.

theorem SimpleGraph.CliqueTree.card_edgeFinset_eq_sum_fiber {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Fintype V] [DecidableRel G.Adj] [Fintype ι] [DecidableEq ι] (T : G.CliqueTree ι) : G.edgeFinset.card = ∑ i : ι, {e ∈ G.edgeFinset | T.edgeBag e = i}.card

Accounting. The edges of G are partitioned according to their assigned bags.

theorem SimpleGraph.CliqueTree.subset_bag_of_mem_fiber {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Fintype V] [DecidableRel G.Adj] [DecidableEq ι] (T : G.CliqueTree ι) {i : ι} {e : Sym2 V} (he : e ∈ {e' ∈ G.edgeFinset | T.edgeBag e' = i}) (v : V) : v ∈ e → v ∈ T.bag i

Every edge assigned to i has both endpoints in bag i.