Documentation

Mathlib.Combinatorics.SimpleGraph.Partition

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:

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 #

Main statements #

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

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
Instances For
    theorem SimpleGraph.Partition.isPartition {V : Type u} {G : SimpleGraph V} (self : G.Partition) :

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

    theorem SimpleGraph.Partition.independent {V : Type u} {G : SimpleGraph V} (self : G.Partition) (s : Set V) :
    s self.partsIsAntichain 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 : G.Partition) (n : ) :

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

    Equations
    • P.PartsCardLe n = ∃ (h : P.parts.Finite), h.toFinset.card n
    Instances For

      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.PartsCardLe n
      Instances For
        def SimpleGraph.Partition.partOfVertex {V : Type u} {G : SimpleGraph V} (P : G.Partition) (v : V) :
        Set V

        The part in the partition that v belongs to

        Equations
        Instances For
          theorem SimpleGraph.Partition.partOfVertex_mem {V : Type u} {G : SimpleGraph V} (P : G.Partition) (v : V) :
          P.partOfVertex v P.parts
          theorem SimpleGraph.Partition.mem_partOfVertex {V : Type u} {G : SimpleGraph V} (P : G.Partition) (v : V) :
          v P.partOfVertex v
          theorem SimpleGraph.Partition.partOfVertex_ne_of_adj {V : Type u} {G : SimpleGraph V} (P : G.Partition) {v : V} {w : V} (h : G.Adj v w) :
          P.partOfVertex v P.partOfVertex w
          def SimpleGraph.Partition.toColoring {V : Type u} {G : SimpleGraph 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
          Instances For
            def SimpleGraph.Partition.toColoring' {V : Type u} {G : SimpleGraph V} (P : G.Partition) :
            G.Coloring (Set V)

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

            Equations
            Instances For
              theorem SimpleGraph.Partition.colorable {V : Type u} {G : SimpleGraph V} (P : G.Partition) [Fintype P.parts] :
              G.Colorable (Fintype.card P.parts)
              @[simp]
              theorem SimpleGraph.Coloring.toPartition_parts {V : Type u} {G : SimpleGraph V} {α : Type v} (C : G.Coloring α) :
              C.toPartition.parts = C.colorClasses
              def SimpleGraph.Coloring.toPartition {V : Type u} {G : SimpleGraph V} {α : Type v} (C : G.Coloring α) :
              G.Partition

              Creates a partition from a coloring.

              Equations
              • C.toPartition = { parts := C.colorClasses, isPartition := , independent := }
              Instances For
                @[simp]
                theorem SimpleGraph.instInhabitedPartition_default {V : Type u} {G : SimpleGraph V} :
                default = G.selfColoring.toPartition
                instance SimpleGraph.instInhabitedPartition {V : Type u} {G : SimpleGraph V} :
                Inhabited G.Partition

                The partition where every vertex is in its own part.

                Equations
                • SimpleGraph.instInhabitedPartition = { default := G.selfColoring.toPartition }
                theorem SimpleGraph.partitionable_iff_colorable {V : Type u} {G : SimpleGraph V} {n : } :
                G.Partitionable n G.Colorable n