Complete Multipartite Graphs

A graph is complete multipartite iff non-adjacency is transitive.

Main declarations

• SimpleGraph.IsCompleteMultipartite: predicate for a graph to be complete multipartite.

• SimpleGraph.IsCompleteMultipartite.setoid: the Setoid given by non-adjacency.

• SimpleGraph.IsCompleteMultipartite.iso: the graph isomorphism from a graph that IsCompleteMultipartite to the corresponding completeMultipartiteGraph.

• SimpleGraph.IsPathGraph3Compl: predicate for three vertices to witness the non-complete-multipartiteness of a graph G. (The name refers to the fact that the three vertices form the complement of pathGraph 3.)

• See also: Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean. The lemma colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree states that a maximally r + 1-cliquefree graph is r-colorable iff it is complete multipartite.

• SimpleGraph.completeEquipartiteGraph: the complete equipartite graph in parts of equal size such that two vertices are adjacent if and only if they are in different parts.

Implementation Notes

The definition of completeEquipartiteGraph is similar to completeMultipartiteGraph except that Sigma.fst is replaced by Prod.fst in the definition. The difference is that the former vertices are a product type whereas the latter vertices are a dependent product type.

While completeEquipartiteGraph r t could have been defined as the specialisation completeMultipartiteGraph (const (Fin r) (Fin t)) (or turanGraph (r * t) r), it is convenient to instead have a non-dependent product type for the vertices.

See completeEquipartiteGraph.completeMultipartiteGraph, completeEquipartiteGraph.turanGraph for the isomorphisms between a completeEquipartiteGraph and a corresponding completeMultipartiteGraph, turanGraph.

def SimpleGraph.IsCompleteMultipartite {α : Type u} (G : SimpleGraph α) : Prop

G is IsCompleteMultipartite iff non-adjacency is transitive

theorem SimpleGraph.bot_isCompleteMultipartite {α : Type u} : ⊥.IsCompleteMultipartite

def SimpleGraph.IsCompleteMultipartite.setoid {α : Type u} {G : SimpleGraph α} (h : G.IsCompleteMultipartite) : Setoid α

The setoid given by non-adjacency

theorem SimpleGraph.completeMultipartiteGraph.isCompleteMultipartite {ι : Type u_1} (V : ι → Type u_2) : (completeMultipartiteGraph V).IsCompleteMultipartite

def SimpleGraph.IsCompleteMultipartite.iso {α : Type u} {G : SimpleGraph α} (h : G.IsCompleteMultipartite) : G ≃g completeMultipartiteGraph fun (c : Quotient h.setoid) => { x : α // h.setoid c.out x }

The graph isomorphism from a graph G that IsCompleteMultipartite to the corresponding completeMultipartiteGraph (see also isCompleteMultipartite_iff)

theorem SimpleGraph.isCompleteMultipartite_iff {α : Type u} {G : SimpleGraph α} : G.IsCompleteMultipartite ↔ ∃ (ι : Type u) (V : ι → Type u) (_ : ∀ (i : ι), Nonempty (V i)), Nonempty (G ≃g completeMultipartiteGraph V)

theorem SimpleGraph.IsCompleteMultipartite.colorable_of_cliqueFree {α : Type u} {G : SimpleGraph α} {n : ℕ} (h : G.IsCompleteMultipartite) (hc : G.CliqueFree n) : G.Colorable (n - 1)

structure SimpleGraph.IsPathGraph3Compl {α : Type u} (G : SimpleGraph α) (v w₁ w₂ : α) : Prop

The vertices v, w₁, w₂ form an IsPathGraph3Compl in G iff w₁w₂ is the only edge present between these three vertices. It is a witness to the non-complete-multipartite-ness of G (see not_isCompleteMultipartite_iff_exists_isPathGraph3Compl). This structure is an explicit way of saying that the induced graph on {v, w₁, w₂} is the complement of P3.

• adj : G.Adj w₁ w₂
• not_adj_fst : ¬G.Adj v w₁
• not_adj_snd : ¬G.Adj v w₂

theorem SimpleGraph.IsPathGraph3Compl.ne_fst {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h2 : G.IsPathGraph3Compl v w₁ w₂) : v ≠ w₁

theorem SimpleGraph.IsPathGraph3Compl.ne_snd {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h2 : G.IsPathGraph3Compl v w₁ w₂) : v ≠ w₂

theorem SimpleGraph.IsPathGraph3Compl.fst_ne_snd {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h2 : G.IsPathGraph3Compl v w₁ w₂) : w₁ ≠ w₂

theorem SimpleGraph.IsPathGraph3Compl.symm {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h : G.IsPathGraph3Compl v w₁ w₂) : G.IsPathGraph3Compl v w₂ w₁

theorem SimpleGraph.exists_isPathGraph3Compl_of_not_isCompleteMultipartite {α : Type u} {G : SimpleGraph α} (h : ¬G.IsCompleteMultipartite) : ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂

theorem SimpleGraph.not_isCompleteMultipartite_iff_exists_isPathGraph3Compl {α : Type u} {G : SimpleGraph α} : ¬G.IsCompleteMultipartite ↔ ∃ (v : α) (w₁ : α) (w₂ : α), G.IsPathGraph3Compl v w₁ w₂

def SimpleGraph.IsPathGraph3Compl.pathGraph3ComplEmbedding {α : Type u} {G : SimpleGraph α} {v w₁ w₂ : α} (h : G.IsPathGraph3Compl v w₁ w₂) : (pathGraph 3)ᶜ ↪g G

Any IsPathGraph3Compl in G gives rise to a graph embedding of the complement of the path graph

noncomputable def SimpleGraph.pathGraph3ComplEmbeddingOf {α : Type u} {G : SimpleGraph α} (h : ¬G.IsCompleteMultipartite) : (pathGraph 3)ᶜ ↪g G

Embedding of (pathGraph 3)ᶜ into G that is not complete-multipartite.

theorem SimpleGraph.not_isCompleteMultipartite_of_pathGraph3ComplEmbedding {α : Type u} {G : SimpleGraph α} (e : (pathGraph 3)ᶜ ↪g G) : ¬G.IsCompleteMultipartite

theorem SimpleGraph.IsCompleteMultipartite.comap {α : Type u} {G : SimpleGraph α} {β : Type u_1} {H : SimpleGraph β} (f : H ↪g G) : G.IsCompleteMultipartite → H.IsCompleteMultipartite

@[reducible, inline]

abbrev SimpleGraph.completeEquipartiteGraph (r t : ℕ) : SimpleGraph (Fin r × Fin t)

The complete equipartite graph in r parts each of equal size t such that two vertices are adjacent if and only if they are in different parts, often denoted $K_r(t)$.

This is isomorphic to a corresponding completeMultipartiteGraph and turanGraph. The difference is that the former vertices are a product type.

See completeEquipartiteGraph.completeMultipartiteGraph, completeEquipartiteGraph.turanGraph.

theorem SimpleGraph.completeEquipartiteGraph_adj {r t : ℕ} {v w : Fin r × Fin t} : (completeEquipartiteGraph r t).Adj v w ↔ v.1 ≠ w.1

def SimpleGraph.completeEquipartiteGraph.completeMultipartiteGraph {r t : ℕ} : completeEquipartiteGraph r t ≃g SimpleGraph.completeMultipartiteGraph (Function.const (Fin r) (Fin t))

A completeEquipartiteGraph is isomorphic to a corresponding completeMultipartiteGraph.

The difference is that the former vertices are a product type whereas the latter vertices are a dependent product type.

def SimpleGraph.completeEquipartiteGraph.turanGraph {r t : ℕ} : completeEquipartiteGraph r t ≃g SimpleGraph.turanGraph (r * t) r

A completeEquipartiteGraph is isomorphic to a corresponding turanGraph.

The difference is that the former vertices are a product type whereas the latter vertices are not.

theorem SimpleGraph.completeEquipartiteGraph_eq_bot_iff {r t : ℕ} : completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0

completeEquipartiteGraph r t contains no edges when r ≤ 1 or t = 0.

theorem SimpleGraph.completeEquipartiteGraph.isCompleteMultipartite {r t : ℕ} : (completeEquipartiteGraph r t).IsCompleteMultipartite

theorem SimpleGraph.neighborSet_completeEquipartiteGraph {r t : ℕ} (v : Fin r × Fin t) : (completeEquipartiteGraph r t).neighborSet v = {v.1}ᶜ ×ˢ Set.univ

theorem SimpleGraph.neighborFinset_completeEquipartiteGraph {r t : ℕ} (v : Fin r × Fin t) : (completeEquipartiteGraph r t).neighborFinset v = {v.1}ᶜ ×ˢ Finset.univ

theorem SimpleGraph.degree_completeEquipartiteGraph {r t : ℕ} (v : Fin r × Fin t) : (completeEquipartiteGraph r t).degree v = (r - 1) * t

theorem SimpleGraph.card_edgeFinset_completeEquipartiteGraph {r t : ℕ} : (completeEquipartiteGraph r t).edgeFinset.card = r.choose 2 * t ^ 2

theorem SimpleGraph.isContained_completeEquipartiteGraph_of_colorable {α : Type u} {G : SimpleGraph α} [Fintype α] {n : ℕ} (C : G.Coloring (Fin n)) (t : ℕ) (h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t) : G.IsContained (completeEquipartiteGraph n t)

Every n-colorable graph is contained in a completeEquipartiteGraph in n parts (as long as the parts are at least as large as the largest color class).