Forbidden induced subgraphs of split graphs #

This file proves the necessary direction of the classical Földes–Hammer characterization. Obstructions use Mathlib graph sums, cycle graphs, and IsIndContained. The converse characterization is not assumed here.

source

theorem SimpleGraph.SplitPartition.mem_clique_or_mem_clique_of_adj {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) {a b : V} (hab : G.Adj a b) :

a ∈ P.clique ∨ b ∈ P.clique

Every edge of a split graph has an endpoint in the clique part.

source

theorem SimpleGraph.SplitPartition.not_two_disjoint_edges {V : Type u_1} {G : SimpleGraph V} (P : G.SplitPartition) {a b c d : V} (hab : G.Adj a b) (hcd : G.Adj c d) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hnac : ¬G.Adj a c) (hnad : ¬G.Adj a d) (hnbc : ¬G.Adj b c) (hnbd : ¬G.Adj b d) :

False

Two disjoint edges cannot have all four cross pairs nonadjacent in a split graph.

source

theorem SimpleGraph.IsSplit.of_isIndContained {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (h : G.IsSplit) (hf : H.IsIndContained G) :

H.IsSplit

Split membership pulls back along native induced-containment certificates.

source

theorem SimpleGraph.twoK2_isIndContained_of_adj {V : Type u_1} {G : SimpleGraph V} {a b c d : V} (hab : G.Adj a b) (hcd : G.Adj c d) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hnac : ¬G.Adj a c) (hnad : ¬G.Adj a d) (hnbc : ¬G.Adj b c) (hnbd : ¬G.Adj b d) :

(⊤ ⊕g ⊤).IsIndContained G

A pair of disjoint edges with no cross edges supplies a native induced embedding.

source

theorem SimpleGraph.not_isSplit_twoK2 :

¬(⊤ ⊕g ⊤).IsSplit

The disjoint union of two edges is not split.

source

theorem SimpleGraph.not_isSplit_cycleGraph_four :

¬(cycleGraph 4).IsSplit

The four-cycle is not split: its complement contains the two opposite edges.

source

theorem SimpleGraph.not_isSplit_cycleGraph_five :