The clique tree of maximal cliques

The bag decomposition attached to a perfect elimination order (CliqueTree/PEO.lean) does not ask the bags to be maximal cliques, so it usually contains redundant bags. This file removes them: for a finite chordal graph we build a clique tree whose bags are exactly the maximal cliques of the graph, each occurring once (bag is injective).

The construction is by elimination of simplicial vertices. Writing S' = S \ {v} for a simplicial vertex v of G[S] and C = N(v) ∩ S':

• if C is already a maximal clique of G[S'], the bag C is replaced by C ∪ {v};
• otherwise a new leaf bag C ∪ {v} is attached to a maximal clique of G[S'] containing C.

Both steps preserve the running-intersection property, the maximality of every bag and the fact that every maximal clique occurs as a bag.

Main definitions

• SimpleGraph.IsMaximalCliqueOn — maximal cliques of the subgraph induced on a finite vertex set
• SimpleGraph.MaxCliqueForest — the data produced by the induction

Main results

• SimpleGraph.IsChordal.exists_maximalCliqueTree — a finite chordal graph has a clique tree whose bags are precisely its maximal cliques, without repetitions
• SimpleGraph.IsPEO.exists_eq_peoBag_of_isMaximalCliqueOn — every maximal clique is one of the PEO bags, namely the bag of its earliest vertex (so removing redundant bags loses nothing)

def SimpleGraph.IsMaximalCliqueOn {V : Type u_1} (G : SimpleGraph V) (S K : Finset V) : Prop

K is a maximal clique of the subgraph of G induced on S.

Equations

• G.IsMaximalCliqueOn S K = (K ⊆ S ∧ G.IsClique ↑K ∧ ∀ K' ⊆ S, G.IsClique ↑K' → K ⊆ K' → K' = K)

theorem SimpleGraph.IsMaximalCliqueOn.subset {V : Type u_1} {G : SimpleGraph V} {S K : Finset V} (h : G.IsMaximalCliqueOn S K) : K ⊆ S

theorem SimpleGraph.IsMaximalCliqueOn.isClique {V : Type u_1} {G : SimpleGraph V} {S K : Finset V} (h : G.IsMaximalCliqueOn S K) : G.IsClique ↑K

theorem SimpleGraph.IsMaximalCliqueOn.eq_of_subset {V : Type u_1} {G : SimpleGraph V} {S K K' : Finset V} (h : G.IsMaximalCliqueOn S K) (hK' : K' ⊆ S) (hclique : G.IsClique ↑K') (hsub : K ⊆ K') : K' = K

theorem SimpleGraph.exists_isMaximalCliqueOn {V : Type u_1} {G : SimpleGraph V} {S K : Finset V} (hKS : K ⊆ S) (hK : G.IsClique ↑K) : ∃ (M : Finset V), K ⊆ M ∧ G.IsMaximalCliqueOn S M

Every clique inside S extends to a maximal clique inside S.

Simplicial elimination: how the maximal cliques change

theorem SimpleGraph.isClique_insert_of_simplicial {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S C : Finset V} {v : V} (hsimp : ∀ a ∈ S, ∀ b ∈ S, G.Adj v a → G.Adj v b → a ≠ b → G.Adj a b) (hC : ∀ (u : V), u ∈ C ↔ u ∈ S.erase v ∧ G.Adj v u) : G.IsClique ↑(insert v C)

The closed neighbourhood of a simplicial vertex is a clique.

theorem SimpleGraph.isClique_of_simplicial {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S C : Finset V} {v : V} (hsimp : ∀ a ∈ S, ∀ b ∈ S, G.Adj v a → G.Adj v b → a ≠ b → G.Adj a b) (hC : ∀ (u : V), u ∈ C ↔ u ∈ S.erase v ∧ G.Adj v u) : G.IsClique ↑C

The open neighbourhood of a simplicial vertex is a clique.

theorem SimpleGraph.isMaximalCliqueOn_insert {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S C : Finset V} {v : V} (hv : v ∈ S) (hsimp : ∀ a ∈ S, ∀ b ∈ S, G.Adj v a → G.Adj v b → a ≠ b → G.Adj a b) (hC : ∀ (u : V), u ∈ C ↔ u ∈ S.erase v ∧ G.Adj v u) : G.IsMaximalCliqueOn S (insert v C)

The closed neighbourhood of a simplicial vertex is a maximal clique.

theorem SimpleGraph.eq_insert_of_isMaximalCliqueOn_of_mem {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S C : Finset V} {v : V} {K : Finset V} (hv : v ∈ S) (hsimp : ∀ a ∈ S, ∀ b ∈ S, G.Adj v a → G.Adj v b → a ≠ b → G.Adj a b) (hC : ∀ (u : V), u ∈ C ↔ u ∈ S.erase v ∧ G.Adj v u) (hK : G.IsMaximalCliqueOn S K) (hvK : v ∈ K) : K = insert v C

A maximal clique containing the eliminated vertex is its closed neighbourhood.

theorem SimpleGraph.isMaximalCliqueOn_erase_of_notMem {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S : Finset V} {v : V} {K : Finset V} (hK : G.IsMaximalCliqueOn S K) (hvK : v ∉ K) : G.IsMaximalCliqueOn (S.erase v) K

A maximal clique avoiding the eliminated vertex stays maximal after the elimination.

theorem SimpleGraph.isMaximalCliqueOn_of_erase {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S C : Finset V} {v : V} {K : Finset V} (hsimp : ∀ a ∈ S, ∀ b ∈ S, G.Adj v a → G.Adj v b → a ≠ b → G.Adj a b) (hC : ∀ (u : V), u ∈ C ↔ u ∈ S.erase v ∧ G.Adj v u) (hK : G.IsMaximalCliqueOn (S.erase v) K) (hne : K ≠ C) : G.IsMaximalCliqueOn S K

Conversely, a maximal clique of the smaller graph other than the neighbourhood C is still a maximal clique of the bigger one.

The maximal-clique forest

structure SimpleGraph.MaxCliqueForest {V : Type u_1} (G : SimpleGraph V) (S : Finset V) : Type u_1

The data assembled by the simplicial-elimination induction: a rooted forest of bags indexed by naturals below size, whose bags are exactly the maximal cliques of G[S].

• size : ℕ

  Number of nodes.

• bag : ℕ → Finset V

  The bag of a node.

• parent : ℕ → Option ℕ

  The parent of a node.

• top : V → ℕ

  The highest node whose bag contains a given vertex.

• size_pos : 0 < self.size

  There is at least one node.

• parent_lt {i j : ℕ} : i < self.size → self.parent i = some j → j < i

  Parents have smaller indices.

• bag_maximal (i : ℕ) : i < self.size → G.IsMaximalCliqueOn S (self.bag i)

  Every bag is a maximal clique of G[S].

• exists_bag (K : Finset V) : G.IsMaximalCliqueOn S K → ∃ i < self.size, self.bag i = K

  Every maximal clique of G[S] is a bag.

• bag_inj (i : ℕ) : i < self.size → ∀ j < self.size, self.bag i = self.bag j → i = j

  No bag is repeated.

• top_lt (v : V) : self.top v < self.size

  Tops are nodes.

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

  Every vertex of S lies in its top bag.

• climb (i : ℕ) : i < self.size → ∀ v ∈ self.bag i, i ≠ self.top v → ∃ (j : ℕ), self.parent i = some j ∧ v ∈ self.bag j

  Local running-intersection property.

theorem SimpleGraph.nonempty_maxCliqueForest_empty {V : Type u_1} {G : SimpleGraph V} : Nonempty (G.MaxCliqueForest ∅)

The empty vertex set carries a one-node forest.

theorem SimpleGraph.nonempty_maxCliqueForest_step_of_maximal {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S : Finset V} {v : V} (hv : v ∈ S) (hsimp : ∀ a ∈ S, ∀ b ∈ S, G.Adj v a → G.Adj v b → a ≠ b → G.Adj a b) (F : G.MaxCliqueForest (S.erase v)) {C : Finset V} (hC : ∀ (u : V), u ∈ C ↔ u ∈ S.erase v ∧ G.Adj v u) (hCmax : G.IsMaximalCliqueOn (S.erase v) C) : Nonempty (G.MaxCliqueForest S)

Elimination step when the neighbourhood of the simplicial vertex is already a maximal clique: the corresponding bag is enlarged by the eliminated vertex.

theorem SimpleGraph.nonempty_maxCliqueForest_step_of_not_maximal {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] {S : Finset V} {v : V} (hv : v ∈ S) (hsimp : ∀ a ∈ S, ∀ b ∈ S, G.Adj v a → G.Adj v b → a ≠ b → G.Adj a b) (F : G.MaxCliqueForest (S.erase v)) {C : Finset V} (hC : ∀ (u : V), u ∈ C ↔ u ∈ S.erase v ∧ G.Adj v u) (hCmax : ¬G.IsMaximalCliqueOn (S.erase v) C) : Nonempty (G.MaxCliqueForest S)

Elimination step when the neighbourhood of the simplicial vertex is not maximal: a new leaf bag is attached to a maximal clique containing it.

theorem SimpleGraph.exists_maxCliqueForest {V : Type u_1} {G : SimpleGraph V} (hG : G.IsChordal) (n : ℕ) (S : Finset V) : S.card = n → Nonempty (G.MaxCliqueForest S)

Simplicial elimination. A finite chordal graph has a maximal-clique forest on every vertex subset.

theorem SimpleGraph.IsChordal.exists_maximalCliqueTree {V : Type u_1} {G : SimpleGraph V} [Fintype V] (hG : G.IsChordal) : ∃ (n : ℕ) (T : G.CliqueTree (Fin n)), (∀ (i : Fin n), G.IsMaximalCliqueOn Finset.univ (T.bag i)) ∧ (∀ (K : Finset V), G.IsMaximalCliqueOn Finset.univ K → ∃ (i : Fin n), T.bag i = K) ∧ Function.Injective T.bag

The clique tree of maximal cliques. A finite chordal graph carries a clique tree whose bags are exactly its maximal cliques, each occurring exactly once.

theorem SimpleGraph.IsPEO.exists_eq_peoBag_of_isMaximalCliqueOn {V : Type u_1} {G : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {ord : V → ℕ} (h : G.IsPEO ord) {K : Finset V} (hK : G.IsMaximalCliqueOn Finset.univ K) (hne : K.Nonempty) : ∃ v ∈ K, K = G.peoBag ord v

No maximal clique is lost by removing redundant bags. Along a perfect elimination order, every maximal clique is the bag of its earliest vertex.