Twins and nontrivial decompositions of cographs

Twins have the same adjacency to every other vertex; they may be adjacent (true twins) or nonadjacent (false twins). Decomposition statements require two nonempty parts and do not constrain the root of an arbitrary unreduced cotree.

def SimpleGraph.AreTwins {V : Type u_1} (G : SimpleGraph V) (a b : V) : Prop

Distinct vertices with identical adjacency outside the pair.

Equations

• G.AreTwins a b = (a ≠ b ∧ ∀ (x : V), x ≠ a → x ≠ b → (G.Adj a x ↔ G.Adj b x))

theorem SimpleGraph.AreTwins.symm {V : Type u_1} {G : SimpleGraph V} {a b : V} (h : G.AreTwins a b) : G.AreTwins b a

The twin relation is symmetric.

theorem SimpleGraph.AreTwins.compl {V : Type u_1} {G : SimpleGraph V} {a b : V} (h : G.AreTwins a b) : Gᶜ.AreTwins a b

Complementation exchanges true and false twins while preserving the twin relation.

theorem SimpleGraph.AreTwins.mapIso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {a b : V} (h : G.AreTwins a b) (f : G ≃g H) : H.AreTwins (f a) (f b)

Relabel a pair of twins along a graph isomorphism.

theorem SimpleGraph.AreTwins.sum_left {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {a b : V} (h : G.AreTwins a b) (H : SimpleGraph W) : (G ⊕g H).AreTwins (Sum.inl a) (Sum.inl b)

A left-child twin pair remains twins in a disjoint union.

theorem SimpleGraph.AreTwins.sum_right {V : Type u_1} {W : Type u_2} {H : SimpleGraph W} {a b : W} (h : H.AreTwins a b) (G : SimpleGraph V) : (G ⊕g H).AreTwins (Sum.inr a) (Sum.inr b)

A right-child twin pair remains twins in a disjoint union.

theorem SimpleGraph.Cotree.exists_twins (t : Cotree) : Nontrivial t.Vertex → ∃ (a : t.Vertex) (b : t.Vertex), t.graph.AreTwins a b

Every cotree with at least two leaves has a twin pair.

theorem SimpleGraph.IsCograph.exists_twins {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V] (h : G.IsCograph) : ∃ (a : V) (b : V), G.AreTwins a b

Every nontrivial finite cograph has true or false twins.

theorem SimpleGraph.IsCograph.exists_join_cut {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V] (h : G.IsCograph) (hc : G.Preconnected) : ∃ (s : Set V), s.Nonempty ∧ sᶜ.Nonempty ∧ ∀ u ∈ s, ∀ v ∉ s, G.Adj u v

A connected nontrivial finite cograph admits a join cut with two nonempty parts.

noncomputable def SimpleGraph.isoJoinInduce {V : Type u_1} {G : SimpleGraph V} (s : Set V) (hcross : ∀ u ∈ s, ∀ v ∉ s, G.Adj u v) : (induce s G).graphJoin (induce sᶜ G) ≃g G

A cut with every cross edge gives an exact join decomposition.

Equations

• SimpleGraph.isoJoinInduce s hcross = ⋯.mp (⋯.mp (⋯.mp (SimpleGraph.isoSumInduce s ⋯).complement))

noncomputable def SimpleGraph.CotreeRepresentation.joinInduce {V : Type u_1} {G : SimpleGraph V} (s : Set V) (hcross : ∀ u ∈ s, ∀ v ∉ s, G.Adj u v) (L : (SimpleGraph.induce s G).CotreeRepresentation) (R : (SimpleGraph.induce sᶜ G).CotreeRepresentation) : G.CotreeRepresentation

Assemble the supplied cotrees across a complete join cut.

Equations

• SimpleGraph.CotreeRepresentation.joinInduce s hcross L R = (L.graphJoin R).mapIso (SimpleGraph.isoJoinInduce s hcross)

theorem SimpleGraph.IsCograph.exists_sum_decomposition {V : Type u_1} {G : SimpleGraph V} (h : G.IsCograph) (hn : ¬G.Preconnected) : ∃ (s : Set V), s.Nonempty ∧ sᶜ.Nonempty ∧ (SimpleGraph.induce s G).IsCograph ∧ (SimpleGraph.induce sᶜ G).IsCograph ∧ Nonempty (SimpleGraph.induce s G ⊕g SimpleGraph.induce sᶜ G ≃g G)

A disconnected cograph splits as a union of two nonempty cographs.

theorem SimpleGraph.IsCograph.exists_join_decomposition {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V] (h : G.IsCograph) (hc : G.Preconnected) : ∃ (s : Set V), s.Nonempty ∧ sᶜ.Nonempty ∧ (SimpleGraph.induce s G).IsCograph ∧ (SimpleGraph.induce sᶜ G).IsCograph ∧ Nonempty ((SimpleGraph.induce s G).graphJoin (SimpleGraph.induce sᶜ G) ≃g G)

A connected nontrivial finite cograph splits as a join of two nonempty cographs.

theorem SimpleGraph.IsCograph.exists_union_root {V : Type u_1} {G : SimpleGraph V} [Finite V] (h : G.IsCograph) (hn : ¬G.Preconnected) : ∃ (R : G.CotreeRepresentation) (l : Cotree) (r : Cotree), R.cotree = l.union r ∧ Nonempty l.Vertex ∧ Nonempty r.Vertex

A disconnected finite cograph admits a union-root cotree with nonempty children.

theorem SimpleGraph.IsCograph.exists_join_root {V : Type u_1} {G : SimpleGraph V} [Finite V] [Nontrivial V] (h : G.IsCograph) (hc : G.Preconnected) : ∃ (R : G.CotreeRepresentation) (l : Cotree) (r : Cotree), R.cotree = l.join r ∧ Nonempty l.Vertex ∧ Nonempty r.Vertex

A connected nontrivial finite cograph admits a join-root cotree with nonempty children.