Subtree representations of chordal graphs

This module provides the chordal-to-subtree direction of Gavril's classical characterization. It does not assert the converse for arbitrary families. The empty connector joins components without changing vertex occurrences. This constructor uses one extra host node; it does not claim a minimal or maximal-clique-indexed host tree.

structure SimpleGraph.SubtreeRepresentation {V : Type u_1} (G : SimpleGraph V) : Type (max 1 u_1)

An exact representation by nonempty connected vertex sets of a finite tree.

• Node : Type

  Vertices of the host tree.

• nodeFintype : Fintype self.Node
• tree : SimpleGraph self.Node

  The host tree.

• isTree : self.tree.IsTree

  The host is connected and acyclic.

• subtree : V → Set self.Node

  The subtree assigned to each graph vertex.

• connected (v : V) : (induce (self.subtree v) self.tree).Connected

  Every assigned subtree is connected, hence nonempty.

• adjacency (u v : V) : u ≠ v → (G.Adj u v ↔ (self.subtree u ∩ self.subtree v).Nonempty)

  Distinct vertices are adjacent exactly when their subtrees intersect.

noncomputable def SimpleGraph.CliqueTree.toSubtreeRepresentation {V : Type u_1} {G : SimpleGraph V} {ι : Type} [Fintype ι] (T : G.CliqueTree ι) : G.SubtreeRepresentation

A clique forest supplies an exact subtree representation, even when disconnected.

Equations

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

theorem SimpleGraph.IsChordal.nonempty_subtreeRepresentation {V : Type} {G : SimpleGraph V} [Finite V] (hG : G.IsChordal) : Nonempty G.SubtreeRepresentation

Every finite chordal graph has a subtree representation on a finite host tree.