Chordality is equivalent to having a clique tree

CliqueTree/PEO.lean builds a clique tree out of a perfect elimination order of a chordal graph. This file proves the converse implications, turning both constructions into characterisations of chordality:

• a graph carrying a clique tree is chordal (SimpleGraph.IsChordal.of_nonempty_cliqueTree);
• a graph carrying a perfect elimination order is chordal (SimpleGraph.IsPEO.isChordal).

The proof of the first statement is direct, with no induction on the graph. Given a cycle of length at least 4, pick the vertex z of the cycle whose top node is deepest, i.e. of largest rank. The two neighbours of z along the cycle share a bag with z, so by maximality of the rank they both lie in the bag of top z; that bag is a clique, so they are adjacent, and being at distance two along a cycle of length at least 4 their edge is not an edge of the cycle.

Main results

• SimpleGraph.IsChordal.of_nonempty_cliqueTree
• SimpleGraph.isChordal_iff_nonempty_cliqueTree
• SimpleGraph.IsPEO.isChordal
• SimpleGraph.isChordal_iff_exists_isPEO

theorem SimpleGraph.IsChordal.of_nonempty_cliqueTree {V : Type u_1} {G : SimpleGraph V} {ι : Type u_2} (T : G.CliqueTree ι) : G.IsChordal

A graph carrying a clique tree is chordal.

theorem SimpleGraph.isChordal_iff_nonempty_cliqueTree {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.IsChordal ↔ Nonempty (G.CliqueTree V)

Chordality is exactly the existence of a clique tree.

theorem SimpleGraph.IsPEO.isChordal {V : Type u_1} {G : SimpleGraph V} [Finite V] {ord : V → ℕ} (h : G.IsPEO ord) : G.IsChordal

A graph carrying a perfect elimination order is chordal.

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

Chordality is exactly the existence of a perfect elimination order.