Maximal cliques: the bridge to Mathlib, and how many there are

Two complements to CliqueTree/Maximal.lean.

• The relative notion SimpleGraph.IsMaximalCliqueOn G S K used in this library agrees, for S = Finset.univ, with the order-theoretic Maximal G.IsClique of Mathlib (SimpleGraph.isMaximalCliqueOn_univ_iff). The relative notion is kept because Mathlib does not cover cliques of induced subgraphs.
• A clique tree whose bags are the maximal cliques has at most Fintype.card V nodes, because every node is the top node of one of its own vertices. Hence a finite chordal graph has at most Fintype.card V maximal cliques.

Main results

• SimpleGraph.isMaximalCliqueOn_univ_iff
• SimpleGraph.MaxCliqueForest.size_le
• SimpleGraph.CliqueTree.card_le_card_of_isMaximalCliqueOn
• SimpleGraph.IsChordal.exists_maximalCliqueTree_card_le
• SimpleGraph.IsChordal.card_maximalCliques_le

The bridge to Maximal G.IsClique

theorem SimpleGraph.isMaximalCliqueOn_univ_iff {V : Type u_1} {G : SimpleGraph V} [Fintype V] {K : Finset V} : G.IsMaximalCliqueOn Finset.univ K ↔ Maximal G.IsClique ↑K

Bridge to Mathlib's notion. For S = Finset.univ the relative maximal cliques of this library are exactly the maximal cliques in the sense of Maximal G.IsClique.

Counting the maximal cliques

theorem SimpleGraph.MaxCliqueForest.exists_top_eq {V : Type u_1} {G : SimpleGraph V} {S : Finset V} (F : G.MaxCliqueForest S) {i : ℕ} (hi : i < F.size) (hne : (F.bag i).Nonempty) : ∃ v ∈ F.bag i, F.top v = i

Every node of a maximal-clique forest is the top node of one of its own vertices.

theorem SimpleGraph.MaxCliqueForest.bag_nonempty {V : Type u_1} {G : SimpleGraph V} {S : Finset V} (F : G.MaxCliqueForest S) {i : ℕ} (hi : i < F.size) (hS : S.Nonempty) : (F.bag i).Nonempty

If the vertex set is nonempty then so is every bag.

theorem SimpleGraph.MaxCliqueForest.size_le_card {V : Type u_1} {G : SimpleGraph V} {S : Finset V} (F : G.MaxCliqueForest S) (hS : S.Nonempty) : F.size ≤ S.card

A maximal-clique forest on a nonempty vertex set has at most one node per vertex.

theorem SimpleGraph.MaxCliqueForest.size_le {V : Type u_1} {G : SimpleGraph V} {S : Finset V} (F : G.MaxCliqueForest S) : F.size ≤ S.card + 1

A maximal-clique forest has at most S.card + 1 nodes, the extra node occurring only for the empty vertex set (whose unique maximal clique is ∅).

theorem SimpleGraph.CliqueTree.exists_top_eq {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Fintype V] [Nonempty V] (T : G.CliqueTree ι) (hmax : ∀ (i : ι), G.IsMaximalCliqueOn Finset.univ (T.bag i)) (hinj : Function.Injective T.bag) (i : ι) : ∃ (v : V), T.top v = i

In a clique tree whose bags are maximal cliques and pairwise distinct, every node is the top node of one of its own vertices.

theorem SimpleGraph.CliqueTree.card_le_card_of_isMaximalCliqueOn {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} [Fintype V] [Nonempty V] [Fintype ι] (T : G.CliqueTree ι) (hmax : ∀ (i : ι), G.IsMaximalCliqueOn Finset.univ (T.bag i)) (hinj : Function.Injective T.bag) : Fintype.card ι ≤ Fintype.card V

A clique tree of maximal cliques has at most one node per vertex.

theorem SimpleGraph.IsChordal.exists_maximalCliqueTree_card_le {V : Type u_1} {G : SimpleGraph V} [Fintype V] [Nonempty V] (hG : G.IsChordal) : ∃ (n : ℕ) (T : G.CliqueTree (Fin n)), n ≤ Fintype.card V ∧ (∀ (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, with the classical bound on the number of bags.

theorem SimpleGraph.IsChordal.card_maximalCliques_le {V : Type u_1} {G : SimpleGraph V} [Fintype V] [Nonempty V] [DecidablePred (G.IsMaximalCliqueOn Finset.univ)] (hG : G.IsChordal) : {K ∈ Finset.univ.powerset | G.IsMaximalCliqueOn Finset.univ K}.card ≤ Fintype.card V

A finite chordal graph has at most Fintype.card V maximal cliques.