Complete Multipartite Graphs

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

Main declarations

• SimpleGraph.IsCompleteMultipartite: predicate for a graph to be complete-multi-partite.

• 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 be a witness to non-complete-multi-partite-ness 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 colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree 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

Equations

• G.IsCompleteMultipartite = Transitive fun (x1 x2 : α) => ¬G.Adj x1 x2

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

Equations

• h.setoid = { r := fun (x1 x2 : α) => ¬G.Adj x1 x2, iseqv := ⋯ }

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)

Equations

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

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

Equations

• h.pathGraph3ComplEmbedding = { toFun := fun (x : Fin 3) => match x with | 0 => w₁ | 1 => v | 2 => w₂, inj' := ⋯, map_rel_iff' := ⋯ }

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.

Equations

• SimpleGraph.pathGraph3ComplEmbeddingOf h = ⋯.pathGraph3ComplEmbedding

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.

Equations

• SimpleGraph.completeEquipartiteGraph r t = SimpleGraph.comap Prod.fst ⊤

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.

Equations

• SimpleGraph.completeEquipartiteGraph.completeMultipartiteGraph = { toEquiv := (Equiv.sigmaEquivProd (Fin r) (Fin t)).symm, map_rel_iff' := ⋯ }

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.

Equations

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

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).