Split partitions

A split partition records a clique and an independent set covering the vertices. Either part may be empty. Membership in the class is a proposition; a partition is a separate certificate that can be restricted or transported.

structure SimpleGraph.SplitPartition {V : Type u_1} (G : SimpleGraph V) : Type u_1

A partition of the vertices into a clique and an independent set.

• clique : Set V

  The clique part.

• independent : Set V

  The independent part.

• isClique : G.IsClique self.clique

  The clique part induces a complete graph.

• isIndepSet : G.IsIndepSet self.independent

  The independent part contains no edges.

• disjoint : Disjoint self.clique self.independent

  No vertex belongs to both parts.

• cover : self.clique ∪ self.independent = Set.univ

  Every vertex belongs to one of the parts.

def SimpleGraph.IsSplit {V : Type u_1} (G : SimpleGraph V) : Prop

A graph is split if it admits a split partition.

Equations

• G.IsSplit = Nonempty G.SplitPartition

theorem SimpleGraph.SplitPartition.mem_clique_or_mem_independent {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) (v : V) : v ∈ P.clique ∨ v ∈ P.independent

Every vertex lies in one of the two parts.

def SimpleGraph.SplitPartition.compl {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) : Gᶜ.SplitPartition

Complementation exchanges the two parts.

Equations

• P.compl = { clique := P.independent, independent := P.clique, isClique := ⋯, isIndepSet := ⋯, disjoint := ⋯, cover := ⋯ }

def SimpleGraph.SplitPartition.comap {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (P : G.SplitPartition) (f : W ↪ V) : (SimpleGraph.comap (⇑f) G).SplitPartition

Pull a partition back along an injective vertex map.

Equations

• P.comap f = { clique := ⇑f ⁻¹' P.clique, independent := ⇑f ⁻¹' P.independent, isClique := ⋯, isIndepSet := ⋯, disjoint := ⋯, cover := ⋯ }

def SimpleGraph.SplitPartition.induce {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) (s : Set V) : (SimpleGraph.induce s G).SplitPartition

Restrict a split partition to an arbitrary induced subgraph.

Equations

• P.induce s = P.comap (Function.Embedding.subtype s)

theorem SimpleGraph.IsSplit.compl {V : Type u_1} {G : SimpleGraph V} (h : G.IsSplit) : Gᶜ.IsSplit

Split graphs are closed under complementation.

@[simp]

theorem SimpleGraph.isSplit_compl {V : Type u_1} {G : SimpleGraph V} : Gᶜ.IsSplit ↔ G.IsSplit

Split membership is invariant under complementation.

theorem SimpleGraph.IsSplit.comap {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (h : G.IsSplit) (f : W ↪ V) : (SimpleGraph.comap (⇑f) G).IsSplit

Split membership pulls back along an injective vertex map.

theorem SimpleGraph.IsSplit.induce {V : Type u_1} {G : SimpleGraph V} (h : G.IsSplit) (s : Set V) : (SimpleGraph.induce s G).IsSplit

Every induced subgraph of a split graph is split.

theorem SimpleGraph.Iso.isSplit_iff {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) : G.IsSplit ↔ H.IsSplit

Graph isomorphisms preserve split membership.

theorem SimpleGraph.isSplit_bot {V : Type u_1} : ⊥.IsSplit

Empty graphs are split, with every vertex in the independent part.

theorem SimpleGraph.isSplit_top {V : Type u_1} : ⊤.IsSplit

Complete graphs are split, with every vertex in the clique part.