Cotree semantics

A binary cotree constructs a finite graph from single vertices by disjoint union and join. An explicit empty constructor handles the empty graph. Binary cotrees need not be reduced or canonical; no uniqueness or recognition complexity is claimed.

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

Cographs are graphs with no induced four-vertex path.

Equations

• G.IsCograph = G.IsP4Free

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

Cograph membership is closed under complementation.

theorem SimpleGraph.IsCograph.comap {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} (h : G.IsCograph) (f : W → V) : (SimpleGraph.comap f G).IsCograph

Cograph membership pulls back along vertex maps.

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

Every induced subgraph of a cograph is a cograph.

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

Graph isomorphisms preserve cograph membership.

theorem SimpleGraph.isCograph_bot {V : Type u_1} : ⊥.IsCograph

Empty graphs are cographs.

theorem SimpleGraph.isCograph_top {V : Type u_1} : ⊤.IsCograph

Complete graphs are cographs.

theorem SimpleGraph.IsP4Free.sum {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (hG : G.IsP4Free) (hH : H.IsP4Free) : (G ⊕g H).IsP4Free

Disjoint union preserves exclusion of induced P₄.

def SimpleGraph.graphJoin {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (H : SimpleGraph W) : SimpleGraph (V ⊕ W)

The join is obtained by complementing the disjoint union of complements.

Equations

• G.graphJoin H = (Gᶜ ⊕g Hᶜ)ᶜ

theorem SimpleGraph.IsP4Free.graphJoin {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (hG : G.IsP4Free) (hH : H.IsP4Free) : (G.graphJoin H).IsP4Free

Join preserves exclusion of induced P₄.

inductive SimpleGraph.Cotree : Type

A finite binary union/join expression for a graph.

• empty : Cotree

  The empty graph.

• leaf : Cotree

  A single vertex.

• union (left right : Cotree) : Cotree

  Disjoint union of the graphs represented by two children.

• join (left right : Cotree) : Cotree

  Join of the graphs represented by two children.

def SimpleGraph.Cotree.Vertex : Cotree → Type

Leaves of a cotree, regarded as the vertices of its graph.

Equations

• SimpleGraph.Cotree.empty.Vertex = PEmpty.{1}
• SimpleGraph.Cotree.leaf.Vertex = Unit
• (l.union r).Vertex = (l.Vertex ⊕ r.Vertex)
• (l.join r).Vertex = (l.Vertex ⊕ r.Vertex)

@[instance_reducible]

noncomputable instance SimpleGraph.Cotree.vertexFintype (t : Cotree) : Fintype t.Vertex

A cotree has finitely many leaves.

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.Cotree.graph (t : Cotree) : SimpleGraph t.Vertex

Interpret union and join using Mathlib's graph operations.

Equations

• SimpleGraph.Cotree.empty.graph = ⊥
• SimpleGraph.Cotree.leaf.graph = ⊥
• (l.union r).graph = l.graph ⊕g r.graph
• (l.join r).graph = l.graph.graphJoin r.graph

theorem SimpleGraph.Cotree.graph_isP4Free (t : Cotree) : t.graph.IsP4Free

Every graph built by a cotree is P₄-free.

theorem SimpleGraph.Cotree.graph_isCograph (t : Cotree) : t.graph.IsCograph

A cotree always constructs a cograph.

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

A representation identifies the actual vertices with the leaves of a cotree.

• cotree : Cotree

  The finite union/join expression.

• iso : self.cotree.graph ≃g G

  The graph isomorphism carrying its leaves to the original vertices.

theorem SimpleGraph.CotreeRepresentation.isCograph {V : Type u_1} {G : SimpleGraph V} (R : G.CotreeRepresentation) : G.IsCograph

A cotree representation certifies cograph membership.

theorem SimpleGraph.isThreshold_iff_isSplit_and_isCograph {V : Type u_1} {G : SimpleGraph V} : G.IsThreshold ↔ G.IsSplit ∧ G.IsCograph

Threshold graphs are precisely split cographs.