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.

• SimpleGraph.CompleteEquipartiteSubgraph G r t is a complete equipartite subgraph, that is, r subsets of vertices each of size t such that the vertices in distinct subsets are adjacent.

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

@[implicit_reducible]

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

structure SimpleGraph.CompleteEquipartiteSubgraph {V : Type u_1} (G : SimpleGraph V) (r t : ℕ) : Type u_1

A complete equipartite subgraph in r > 0 parts each of size t ≠ 0 in G is r subsets of vertices each of size t such that vertices in distinct subsets are adjacent.

If r > 0 but t = 0, then parts = {{}}. If r = 0, then parts = {}. These are the two distinct "empty" complete equipartite subgraphs, that is, the complete equipartite subgraphs having no vertices.

• parts : Finset (Finset V)

  The parts in a complete equipartite subgraph.

• card_parts : self.parts.card = r ∨ t = 0

  There are r parts or t = 0.

• card_mem_parts {p : Finset V} : p ∈ self.parts → p.card = t

  There are t vertices in each part.

• isCompleteBetween : (↑self.parts).Pairwise fun (x1 x2 : Finset V) => G.IsCompleteBetween ↑x1 ↑x2

  The vertices in distinct parts are adjacent.

theorem SimpleGraph.CompleteEquipartiteSubgraph.ext {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} {x y : G.CompleteEquipartiteSubgraph r t} (parts : x.parts = y.parts) : x = y

theorem SimpleGraph.CompleteEquipartiteSubgraph.ext_iff {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} {x y : G.CompleteEquipartiteSubgraph r t} : x = y ↔ x.parts = y.parts

theorem SimpleGraph.CompleteEquipartiteSubgraph.nonempty_of_eq_zero_or_eq_zero {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (h : r = 0 ∨ t = 0) : Nonempty (G.CompleteEquipartiteSubgraph r t)

At least one of the "empty" complete equipartite subgraphs is contained in a simple graph.

theorem SimpleGraph.CompleteEquipartiteSubgraph.disjoint {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t) : (↑K.parts).Pairwise Disjoint

The parts in a complete equipartite subgraph are pairwise disjoint.

def SimpleGraph.CompleteEquipartiteSubgraph.verts {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t) : Finset V

The finset of vertices in a complete equipartite subgraph.

theorem SimpleGraph.CompleteEquipartiteSubgraph.verts_eq_biUnion {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t) : K.verts = K.parts.biUnion id

The finset of vertices in a complete equipartite subgraph as a biUnion.

theorem SimpleGraph.CompleteEquipartiteSubgraph.card_verts {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t) : K.verts.card = r * t

There are r * t vertices in a complete equipartite subgraph with r parts of size t.

noncomputable def SimpleGraph.CompleteEquipartiteSubgraph.toCopy {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (K : G.CompleteEquipartiteSubgraph r t) : (completeEquipartiteGraph r t).Copy G

A complete equipartite subgraph gives rise to a copy of a complete equipartite graph.

def SimpleGraph.CompleteEquipartiteSubgraph.ofCopy {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} (f : (completeEquipartiteGraph r t).Copy G) : G.CompleteEquipartiteSubgraph r t

A copy of a complete equipartite graph identifies a complete equipartite subgraph.

theorem SimpleGraph.completeEquipartiteGraph_isContained_iff {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} : (completeEquipartiteGraph r t).IsContained G ↔ Nonempty (G.CompleteEquipartiteSubgraph r t)

Simple graphs contain a copy of a completeEquipartiteGraph r t iff the type G.CompleteEquipartiteSubgraph r t is nonempty.

theorem SimpleGraph.completeEquipartiteGraph_succ_isContained_iff {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} : (completeEquipartiteGraph (r + 1) t).IsContained G ↔ ∃ (K : G.CompleteEquipartiteSubgraph r t) (s : Finset V), s.card = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s

Simple graphs contain a copy of a completeEquipartiteGraph (r + 1) t iff there exists s : Finset V of size #s = t and K : G.CompleteEquipartiteSubgraph r t such that the vertices in s are adjacent to the vertices in K.