Perfect elimination orders and the clique-bag decomposition

A perfect elimination order (PEO) of a graph is a linear ordering of its vertices — here given by an injective ranking ord : V → ℕ — such that the neighbours of each vertex occurring later in the order form a clique. Dirac's theorem (available in Chordal.lean) yields a PEO for every finite chordal graph.

Out of a PEO we build the clique-bag decomposition: the bag of v is {v} ∪ N⁺(v), where N⁺(v) are the neighbours of v occurring later in the order. These bags are cliques, they cover all vertices and all edges, and maximality is never required: the bags form a genuine clique tree in the sense of SimpleGraph.CliqueTree, with parent of v the earliest later neighbour of v.

Main definitions

• SimpleGraph.IsPEO
• SimpleGraph.laterNbrs, SimpleGraph.peoBag, SimpleGraph.peoParent, SimpleGraph.peoRank
• SimpleGraph.IsPEO.cliqueTree — the clique tree carried by the bag decomposition

Main results

• SimpleGraph.IsChordal.exists_isPEO — a finite chordal graph admits a perfect elimination order
• SimpleGraph.IsPEO.peoBag_isClique, SimpleGraph.IsPEO.exists_peoBag_of_adj
• SimpleGraph.IsPEO.card_edgeFinset_eq_sum_card_laterNbrs — edge accounting: each edge is charged exactly once, to its earlier endpoint

structure SimpleGraph.IsPEO {V : Type u_1} (G : SimpleGraph V) (ord : V → ℕ) : Prop

A perfect elimination order of G, given by an injective ranking ord : V → ℕ: the neighbours of a vertex that come later in the order form a clique.

• injective : Function.Injective ord

  The ranking is injective, i.e. it is a linear order on the vertices.

• isClique_later (v : V) : G.IsClique {u : V | ord v < ord u ∧ G.Adj v u}

  The later neighbourhood of every vertex is a clique.

Existence of a perfect elimination order

theorem SimpleGraph.IsChordal.exists_simplicial_in_finset {V : Type u_1} {G : SimpleGraph V} (hG : G.IsChordal) (S : Finset V) (hSne : S.Nonempty) : ∃ z ∈ S, ∀ a ∈ S, ∀ b ∈ S, G.Adj z a → G.Adj z b → a ≠ b → G.Adj a b

Every nonempty finite vertex set in a chordal graph contains a vertex whose neighbours within that set form a clique.

theorem SimpleGraph.exists_rank_of_simplicial_elimination {V : Type u_1} {G : SimpleGraph V} (helim : ∀ (S : Finset V), S.Nonempty → ∃ z ∈ S, ∀ a ∈ S, ∀ b ∈ S, G.Adj z a → G.Adj z b → a ≠ b → G.Adj a b) (n : ℕ) (S : Finset V) : S.card = n → ∃ (f : V → ℕ), Set.InjOn f ↑S ∧ ∀ v ∈ S, G.IsClique {u : V | u ∈ S ∧ f v < f u ∧ G.Adj v u}

Relative simplicial elimination produces an injective ranking on every finite set.

theorem SimpleGraph.exists_isPEO_of_simplicial_in_finset {V : Type u_1} {G : SimpleGraph V} [Finite V] (hsimp : ∀ (S : Finset V), S.Nonempty → ∃ z ∈ S, ∀ a ∈ S, ∀ b ∈ S, G.Adj z a → G.Adj z b → a ≠ b → G.Adj a b) : ∃ (ord : V → ℕ), G.IsPEO ord

Relative simpliciality in every nonempty finite vertex set yields an elimination order.

theorem SimpleGraph.IsChordal.exists_isPEO {V : Type u_1} {G : SimpleGraph V} [Finite V] (hG : G.IsChordal) : ∃ (ord : V → ℕ), G.IsPEO ord

Every finite chordal graph has a perfect elimination order.

The clique-bag decomposition of a perfect elimination order

def SimpleGraph.laterNbrs {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (ord : V → ℕ) (v : V) : Finset V

The neighbours of v occurring later than v in the order ord.

Equations

• G.laterNbrs ord v = {u : V | ord v < ord u ∧ G.Adj v u}

def SimpleGraph.peoBag {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ord : V → ℕ) (v : V) : Finset V

The clique bag of v: the vertex together with its later neighbours.

Equations

• G.peoBag ord v = insert v (G.laterNbrs ord v)

noncomputable def SimpleGraph.peoParent {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (ord : V → ℕ) (v : V) : Option V

The parent of v: its earliest later neighbour, if any.

Equations

• G.peoParent ord v = if h : (G.laterNbrs ord v).Nonempty then some ⋯.choose else none

def SimpleGraph.peoRank {V : Type u_1} [Fintype V] (ord : V → ℕ) (v : V) : ℕ

The rank of v: the number of vertices occurring after v.

Equations

• SimpleGraph.peoRank ord v = {u : V | ord v < ord u}.card

@[simp]

theorem SimpleGraph.mem_laterNbrs {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {ord : V → ℕ} {v u : V} : u ∈ G.laterNbrs ord v ↔ ord v < ord u ∧ G.Adj v u

@[simp]

theorem SimpleGraph.mem_peoBag {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} {v u : V} : u ∈ G.peoBag ord v ↔ u = v ∨ ord v < ord u ∧ G.Adj v u

theorem SimpleGraph.self_mem_peoBag {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (v : V) : v ∈ G.peoBag ord v

theorem SimpleGraph.notMem_laterNbrs_self {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {ord : V → ℕ} (v : V) : v ∉ G.laterNbrs ord v

theorem SimpleGraph.card_peoBag {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (v : V) : (G.peoBag ord v).card = (G.laterNbrs ord v).card + 1

theorem SimpleGraph.peoRank_lt_of_ord_lt {V : Type u_1} [Fintype V] {ord : V → ℕ} {u v : V} (h : ord u < ord v) : peoRank ord v < peoRank ord u

theorem SimpleGraph.peoRank_injective {V : Type u_1} [Fintype V] {ord : V → ℕ} (h : Function.Injective ord) : Function.Injective (peoRank ord)

theorem SimpleGraph.peoParent_spec {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {ord : V → ℕ} {v p : V} (hp : G.peoParent ord v = some p) : p ∈ G.laterNbrs ord v ∧ ∀ u ∈ G.laterNbrs ord v, ord p ≤ ord u

theorem SimpleGraph.peoParent_eq_some {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {ord : V → ℕ} {v : V} (hne : (G.laterNbrs ord v).Nonempty) : ∃ (p : V), G.peoParent ord v = some p

theorem SimpleGraph.IsPEO.peoBag_isClique {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) (v : V) : G.IsClique ↑(G.peoBag ord v)

theorem SimpleGraph.IsPEO.exists_peoBag_of_adj {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) {u v : V} (hadj : G.Adj u v) : ∃ (w : V), u ∈ G.peoBag ord w ∧ v ∈ G.peoBag ord w

theorem SimpleGraph.IsPEO.mem_peoBag_peoParent {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) {v w : V} (hw : w ∈ G.peoBag ord v) (hne : w ≠ v) : ∃ (p : V), G.peoParent ord v = some p ∧ w ∈ G.peoBag ord p

noncomputable def SimpleGraph.IsPEO.cliqueTree {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) : G.CliqueTree V

The clique-bag decomposition of a perfect elimination order is a clique tree. No maximality of the bags is required.

Equations

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

@[simp]

theorem SimpleGraph.IsPEO.cliqueTree_bag {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) (v : V) : h.cliqueTree.bag v = G.peoBag ord v

@[simp]

theorem SimpleGraph.IsPEO.cliqueTree_top {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) (v : V) : h.cliqueTree.top v = v

Edge accounting

theorem SimpleGraph.IsPEO.card_edgeFinset_eq_sum_card_laterNbrs {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) : G.edgeFinset.card = ∑ v : V, (G.laterNbrs ord v).card

Unique edge assignment along a PEO. Every edge is charged to its earlier endpoint, and the total count of edges is the total number of later neighbours.

theorem SimpleGraph.IsPEO.card_edgeFinset_add_card_eq_sum_card_peoBag {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) : G.edgeFinset.card + Fintype.card V = ∑ v : V, (G.peoBag ord v).card

The bag form of the edge accounting: each bag contributes its size minus one.

theorem SimpleGraph.IsChordal.nonempty_cliqueTree {V : Type u_2} [Finite V] {G : SimpleGraph V} (hG : G.IsChordal) : Nonempty (G.CliqueTree V)

Every finite chordal graph has a clique tree, namely the clique-bag decomposition of any perfect elimination order.