Graph partitions

This module provides an interface for dealing with partitions on simple graphs. A partition of a graph G, with vertices V, is a set P of disjoint nonempty subsets of V such that:

• The union of the subsets in P is V.

• Each element of P is an independent set. (Each subset contains no pair of adjacent vertices.)

Graph partitions are graph colorings that do not name their colors. They are adjoint in the following sense. Given a graph coloring, there is an associated partition from the set of color classes, and given a partition, there is an associated graph coloring from using the partition's subsets as colors. Going from graph colorings to partitions and back makes a coloring "canonical": all colors are given a canonical name and unused colors are removed. Going from partitions to graph colorings and back is the identity.

Main definitions

• SimpleGraph.Partition is a structure to represent a partition of a simple graph

• SimpleGraph.Partition.PartsCardLe is whether a given partition is an n-partition. (a partition with at most n parts).

• SimpleGraph.Partitionable n is whether a given graph is n-partite

• SimpleGraph.Partition.toColoring creates colorings from partitions

• SimpleGraph.Coloring.toPartition creates partitions from colorings

Main statements

• SimpleGraph.partitionable_iff_colorable is that n-partitionability and n-colorability are equivalent.

structure SimpleGraph.Partition {V : Type u} (G : SimpleGraph V) : Type u

A Partition of a simple graph G is a structure constituted by

• parts: a set of subsets of the vertices V of G
• isPartition: a proof that parts is a proper partition of V
• independent: a proof that each element of parts doesn't have a pair of adjacent vertices

• parts : Set (Set V)

  parts: a set of subsets of the vertices V of G.

• isPartition : Setoid.IsPartition self.parts

  isPartition: a proof that parts is a proper partition of V.

• independent : ∀ s ∈ self.parts, IsAntichain G.Adj s

  independent: a proof that each element of parts doesn't have a pair of adjacent vertices.

def SimpleGraph.Partition.PartsCardLe {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) (n : ℕ) : Prop

Whether a partition P has at most n parts. A graph with a partition satisfying this predicate called n-partite. (See SimpleGraph.Partitionable.)

Equations

• SimpleGraph.Partition.PartsCardLe P n = ∃ (h : Set.Finite P.parts), (Set.Finite.toFinset h).card ≤ n

def SimpleGraph.Partitionable {V : Type u} (G : SimpleGraph V) (n : ℕ) : Prop

Whether a graph is n-partite, which is whether its vertex set can be partitioned in at most n independent sets.

Equations

• SimpleGraph.Partitionable G n = ∃ (P : SimpleGraph.Partition G), SimpleGraph.Partition.PartsCardLe P n

def SimpleGraph.Partition.partOfVertex {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) (v : V) : Set V

The part in the partition that v belongs to

Equations

• SimpleGraph.Partition.partOfVertex P v = Classical.choose ⋯

theorem SimpleGraph.Partition.partOfVertex_mem {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) (v : V) : SimpleGraph.Partition.partOfVertex P v ∈ P.parts

theorem SimpleGraph.Partition.mem_partOfVertex {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) (v : V) : v ∈ SimpleGraph.Partition.partOfVertex P v

theorem SimpleGraph.Partition.partOfVertex_ne_of_adj {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) {v : V} {w : V} (h : G.Adj v w) : SimpleGraph.Partition.partOfVertex P v ≠ SimpleGraph.Partition.partOfVertex P w

def SimpleGraph.Partition.toColoring {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) : SimpleGraph.Coloring G ↑P.parts

Create a coloring using the parts themselves as the colors. Each vertex is colored by the part it's contained in.

Equations

• SimpleGraph.Partition.toColoring P = SimpleGraph.Coloring.mk (fun (v : V) => { val := SimpleGraph.Partition.partOfVertex P v, property := ⋯ }) ⋯

def SimpleGraph.Partition.toColoring' {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) : SimpleGraph.Coloring G (Set V)

Like SimpleGraph.Partition.toColoring but uses Set V as the coloring type.

Equations

• SimpleGraph.Partition.toColoring' P = SimpleGraph.Coloring.mk (SimpleGraph.Partition.partOfVertex P) ⋯

theorem SimpleGraph.Partition.colorable {V : Type u} {G : SimpleGraph V} (P : SimpleGraph.Partition G) [Fintype ↑P.parts] : SimpleGraph.Colorable G (Fintype.card ↑P.parts)

@[simp]

theorem SimpleGraph.Coloring.toPartition_parts {V : Type u} {G : SimpleGraph V} {α : Type v} (C : SimpleGraph.Coloring G α) : (SimpleGraph.Coloring.toPartition C).parts = SimpleGraph.Coloring.colorClasses C

def SimpleGraph.Coloring.toPartition {V : Type u} {G : SimpleGraph V} {α : Type v} (C : SimpleGraph.Coloring G α) : SimpleGraph.Partition G

Creates a partition from a coloring.

Equations

• SimpleGraph.Coloring.toPartition C = { parts := SimpleGraph.Coloring.colorClasses C, isPartition := ⋯, independent := ⋯ }

@[simp]

theorem SimpleGraph.instInhabitedPartition_default {V : Type u} {G : SimpleGraph V} : default = SimpleGraph.Coloring.toPartition (SimpleGraph.selfColoring G)

instance SimpleGraph.instInhabitedPartition {V : Type u} {G : SimpleGraph V} : Inhabited (SimpleGraph.Partition G)

The partition where every vertex is in its own part.

Equations

• SimpleGraph.instInhabitedPartition = { default := SimpleGraph.Coloring.toPartition (SimpleGraph.selfColoring G) }

theorem SimpleGraph.partitionable_iff_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} : SimpleGraph.Partitionable G n ↔ SimpleGraph.Colorable G n