mathlib3 documentation

combinatorics.simple_graph.partition

Graph partitions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

simple_graph.partition is a structure to represent a partition of a simple graph
simple_graph.partition.parts_card_le is whether a given partition is an n-partition. (a partition with at most n parts).
simple_graph.partitionable n is whether a given graph is n-partite
simple_graph.partition.to_coloring creates colorings from partitions
simple_graph.coloring.to_partition creates partitions from colorings

Main statements #

simple_graph.partitionable_iff_colorable is that n-partitionability and n-colorability are equivalent.

structure simple_graph.partition {V : Type u} (G : simple_graph V) :

parts : set (set V)
is_partition : setoid.is_partition self.parts
independent : ∀ (s : set V), s ∈ self.parts → is_antichain G.adj s

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

parts: a set of subsets of the vertices V of G
is_partition: 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

Instances for simple_graph.partition

simple_graph.partition.has_sizeof_inst
simple_graph.partition.inhabited

def simple_graph.partition.parts_card_le {V : Type u} {G : simple_graph V} (P : G.partition) (n : ℕ) :

Prop

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

Equations

P.parts_card_le n = ∃ (h : P.parts.finite), h.to_finset.card ≤ n

def simple_graph.partitionable {V : Type u} (G : simple_graph 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

G.partitionable n = ∃ (P : G.partition), P.parts_card_le n

def simple_graph.partition.part_of_vertex {V : Type u} {G : simple_graph V} (P : G.partition) (v : V) :

The part in the partition that v belongs to

Equations

P.part_of_vertex v = classical.some _

theorem simple_graph.partition.part_of_vertex_mem {V : Type u} {G : simple_graph V} (P : G.partition) (v : V) :

P.part_of_vertex v ∈ P.parts

theorem simple_graph.partition.mem_part_of_vertex {V : Type u} {G : simple_graph V} (P : G.partition) (v : V) :

v ∈ P.part_of_vertex v

theorem simple_graph.partition.part_of_vertex_ne_of_adj {V : Type u} {G : simple_graph V} (P : G.partition) {v w : V} (h : G.adj v w) :

P.part_of_vertex v ≠ P.part_of_vertex w

def simple_graph.partition.to_coloring {V : Type u} {G : simple_graph V} (P : G.partition) :

G.coloring ↥(P.parts)

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

Equations

P.to_coloring = simple_graph.coloring.mk (λ (v : V), ⟨P.part_of_vertex v, _⟩) _

def simple_graph.partition.to_coloring' {V : Type u} {G : simple_graph V} (P : G.partition) :

G.coloring (set V)

Like simple_graph.partition.to_coloring but uses set V as the coloring type.

Equations

P.to_coloring' = simple_graph.coloring.mk P.part_of_vertex _

theorem simple_graph.partition.to_colorable {V : Type u} {G : simple_graph V} (P : G.partition) [fintype ↥(P.parts)] :

G.colorable (fintype.card ↥(P.parts))

def simple_graph.coloring.to_partition {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) :

Creates a partition from a coloring.

Equations

C.to_partition = {parts := C.color_classes, is_partition := _, independent := _}

@[simp]

theorem simple_graph.coloring.to_partition_parts {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) :

C.to_partition.parts = C.color_classes

@[simp]

theorem simple_graph.partition.inhabited_default {V : Type u} {G : simple_graph V} :

inhabited.default = G.self_coloring.to_partition

@[protected, instance]

def simple_graph.partition.inhabited {V : Type u} {G : simple_graph V} :

inhabited G.partition

The partition where every vertex is in its own part.

Equations

simple_graph.partition.inhabited = {default := G.self_coloring.to_partition}

theorem simple_graph.partitionable_iff_colorable {V : Type u} {G : simple_graph V} {n : ℕ} :

G.partitionable n ↔ G.colorable n