Reincorporating a simplicial vertex into a split partition #
In a graph without an induced pair of disjoint edges, a split partition of the graph minus a simplicial vertex extends to a split partition of the graph. The extension may exchange one clique vertex with one independent vertex. No finiteness hypothesis is needed for this local step.
theorem
SimpleGraph.isSplit_of_isClique_of_isIndepSet_compl
{V : Type u_1}
{G : SimpleGraph V}
{C : Set V}
(hc : G.IsClique C)
(hi : G.IsIndepSet Cᶜ)
:
G.IsSplit
A clique whose complement is independent certifies split membership.
theorem
SimpleGraph.isSplit_of_simplicial_extension
{V : Type u_1}
{G : SimpleGraph V}
{C : Set V}
{v : V}
(hc : G.IsClique C)
(hv : v ∉ C)
(hi : G.IsIndepSet (Cᶜ \ {v}))
(hs : G.IsSimplicial v)
(hf : ¬(⊤ ⊕g ⊤).IsIndContained G)
:
G.IsSplit
A split partition away from a simplicial vertex can be extended when 2K₂ is excluded.
theorem
SimpleGraph.isSplit_of_simplicial_delete
{V : Type u_1}
{G : SimpleGraph V}
{v : V}
(hs : G.IsSimplicial v)
(hf : ¬(⊤ ⊕g ⊤).IsIndContained G)
(hd : (induce {x : V | x ≠ v} G).IsSplit)
:
G.IsSplit
The local extension step applied to a split certificate on the deleted graph.
theorem
SimpleGraph.IsChordal.isSplit_of_not_twoK2_isIndContained
{V : Type u_1}
{G : SimpleGraph V}
[Finite V]
(hc : G.IsChordal)
(hf : ¬(⊤ ⊕g ⊤).IsIndContained G)
:
G.IsSplit
A finite chordal graph with no induced pair of disjoint edges is split.
theorem
SimpleGraph.isSplit_iff_isChordal_and_not_twoK2_isIndContained
{V : Type u_1}
{G : SimpleGraph V}
[Finite V]
:
Finite split graphs are exactly chordal graphs without an induced pair of disjoint edges.
theorem
SimpleGraph.IsChordal.of_isIndContained
{V : Type u_1}
{G : SimpleGraph V}
{W : Type u_2}
{H : SimpleGraph W}
(h : G.IsChordal)
(hf : H.IsIndContained G)
:
Chordality pulls back along a native induced-containment certificate.