Simplicial vertices and maximum-clique split partitions

A maximum clique part can be chosen, but partitions need not be unique or comparable. The two-vertex edgeless example has two incomparable maximum parts.

theorem SimpleGraph.SplitPartition.isSimplicial_of_mem_independent {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) {v : V} (hv : v ∈ P.independent) : G.IsSimplicial v

Every independent-part vertex of a split partition is simplicial.

theorem SimpleGraph.IsSplit.exists_maximum_clique_partition {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsSplit) : ∃ (C : Finset V), G.IsNClique G.cliqueNum C ∧ G.IsIndepSet (↑C)ᶜ

A finite split graph has a split partition whose clique part is a maximum clique.

theorem SimpleGraph.IsSplit.exists_partition_with_maximum_clique {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsSplit) : ∃ (P : G.SplitPartition) (C : Finset V), P.clique = ↑C ∧ G.IsNClique G.cliqueNum C

Package the maximum clique as the clique part of an actual split certificate.

def SimpleGraph.emptyPairPartition (v : Fin 2) : ⊥.SplitPartition

Either singleton can be the clique part of a two-vertex edgeless split graph.

Equations

• SimpleGraph.emptyPairPartition v = { clique := {v}, independent := {v}ᶜ, isClique := ⋯, isIndepSet := ⋯, disjoint := ⋯, cover := ⋯ }

theorem SimpleGraph.emptyPairPartition_incomparable : ¬(emptyPairPartition 0).clique ⊆ (emptyPairPartition 1).clique ∧ ¬(emptyPairPartition 1).clique ⊆ (emptyPairPartition 0).clique

Maximum clique parts of split partitions can be incomparable.

theorem SimpleGraph.emptyPairPartition_maximum (v : Fin 2) : ⊥.IsNClique ⊥.cliqueNum {v}

Each of the two incomparable singleton parts is a maximum clique.