Documentation

Mathlib.Combinatorics.SimpleGraph.Coloring

Graph Coloring #

This module defines colorings of simple graphs (also known as proper colorings in the literature). A graph coloring is the attribution of "colors" to all of its vertices such that adjacent vertices have different colors. A coloring can be represented as a homomorphism into a complete graph, whose vertices represent the colors.

Main definitions #

Todo: #

@[reducible, inline]
abbrev SimpleGraph.Coloring {V : Type u} (G : SimpleGraph V) (α : Type v) :
Type (max u v)

An α-coloring of a simple graph G is a homomorphism of G into the complete graph on α. This is also known as a proper coloring.

Equations
Instances For
    theorem SimpleGraph.Coloring.valid {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) {v : V} {w : V} (h : G.Adj v w) :
    C v C w
    @[match_pattern]
    def SimpleGraph.Coloring.mk {V : Type u} {G : SimpleGraph V} {α : Type u_1} (color : Vα) (valid : ∀ {v w : V}, G.Adj v wcolor v color w) :
    G.Coloring α

    Construct a term of SimpleGraph.Coloring using a function that assigns vertices to colors and a proof that it is as proper coloring.

    (Note: this is a definitionally the constructor for SimpleGraph.Hom, but with a syntactically better proper coloring hypothesis.)

    Equations
    Instances For
      def SimpleGraph.Coloring.colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) (c : α) :
      Set V

      The color class of a given color.

      Equations
      • C.colorClass c = {v : V | C v = c}
      Instances For
        def SimpleGraph.Coloring.colorClasses {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) :
        Set (Set V)

        The set containing all color classes.

        Equations
        Instances For
          theorem SimpleGraph.Coloring.mem_colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) (v : V) :
          v C.colorClass (C v)
          theorem SimpleGraph.Coloring.colorClasses_isPartition {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) :
          Setoid.IsPartition C.colorClasses
          theorem SimpleGraph.Coloring.mem_colorClasses {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) {v : V} :
          C.colorClass (C v) C.colorClasses
          theorem SimpleGraph.Coloring.colorClasses_finite {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) [Finite α] :
          C.colorClasses.Finite
          theorem SimpleGraph.Coloring.card_colorClasses_le {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) [Fintype α] [Fintype C.colorClasses] :
          Fintype.card C.colorClasses Fintype.card α
          theorem SimpleGraph.Coloring.not_adj_of_mem_colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) {c : α} {v : V} {w : V} (hv : v C.colorClass c) (hw : w C.colorClass c) :
          ¬G.Adj v w
          theorem SimpleGraph.Coloring.color_classes_independent {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) (c : α) :
          IsAntichain G.Adj (C.colorClass c)
          noncomputable instance SimpleGraph.instFintypeColoring {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype V] [Fintype α] :
          Fintype (G.Coloring α)
          Equations
          def SimpleGraph.Colorable {V : Type u} (G : SimpleGraph V) (n : ) :

          Whether a graph can be colored by at most n colors.

          Equations
          Instances For
            def SimpleGraph.coloringOfIsEmpty {V : Type u} (G : SimpleGraph V) {α : Type u_1} [IsEmpty V] :
            G.Coloring α

            The coloring of an empty graph.

            Equations
            Instances For
              theorem SimpleGraph.colorable_of_isEmpty {V : Type u} (G : SimpleGraph V) [IsEmpty V] (n : ) :
              G.Colorable n
              theorem SimpleGraph.isEmpty_of_colorable_zero {V : Type u} (G : SimpleGraph V) (h : G.Colorable 0) :
              def SimpleGraph.selfColoring {V : Type u} (G : SimpleGraph V) :
              G.Coloring V

              The "tautological" coloring of a graph, using the vertices of the graph as colors.

              Equations
              Instances For
                noncomputable def SimpleGraph.chromaticNumber {V : Type u} (G : SimpleGraph V) :

                The chromatic number of a graph is the minimal number of colors needed to color it. This is (infinity) iff G isn't colorable with finitely many colors.

                If G is colorable, then ENat.toNat G.chromaticNumber is the -valued chromatic number.

                Equations
                • G.chromaticNumber = nsetOf G.Colorable, n
                Instances For
                  theorem SimpleGraph.chromaticNumber_eq_biInf {V : Type u} {G : SimpleGraph V} :
                  G.chromaticNumber = nsetOf G.Colorable, n
                  theorem SimpleGraph.chromaticNumber_eq_iInf {V : Type u} {G : SimpleGraph V} :
                  G.chromaticNumber = ⨅ (n : {m : | G.Colorable m}), n
                  theorem SimpleGraph.Colorable.chromaticNumber_eq_sInf {V : Type u} {G : SimpleGraph V} {n : } (h : G.Colorable n) :
                  G.chromaticNumber = (sInf {n' : | G.Colorable n'})
                  def SimpleGraph.recolorOfEmbedding {V : Type u} (G : SimpleGraph V) {α : Type u_3} {β : Type u_4} (f : α β) :
                  G.Coloring α G.Coloring β

                  Given an embedding, there is an induced embedding of colorings.

                  Equations
                  Instances For
                    @[simp]
                    theorem SimpleGraph.coe_recolorOfEmbedding {V : Type u} (G : SimpleGraph V) {α : Type u_1} {β : Type u_2} (f : α β) :
                    (G.recolorOfEmbedding f) = (SimpleGraph.Embedding.completeGraph f).toHom.comp
                    def SimpleGraph.recolorOfEquiv {V : Type u} (G : SimpleGraph V) {α : Type u_3} {β : Type u_4} (f : α β) :
                    G.Coloring α G.Coloring β

                    Given an equivalence, there is an induced equivalence between colorings.

                    Equations
                    • G.recolorOfEquiv f = { toFun := (G.recolorOfEmbedding f.toEmbedding), invFun := (G.recolorOfEmbedding f.symm.toEmbedding), left_inv := , right_inv := }
                    Instances For
                      @[simp]
                      theorem SimpleGraph.coe_recolorOfEquiv {V : Type u} (G : SimpleGraph V) {α : Type u_1} {β : Type u_2} (f : α β) :
                      (G.recolorOfEquiv f) = (SimpleGraph.Embedding.completeGraph f.toEmbedding).toHom.comp
                      noncomputable def SimpleGraph.recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (hn : Fintype.card α Fintype.card β) :
                      G.Coloring α G.Coloring β

                      There is a noncomputable embedding of α-colorings to β-colorings if β has at least as large a cardinality as α.

                      Equations
                      • G.recolorOfCardLE hn = G.recolorOfEmbedding .some
                      Instances For
                        @[simp]
                        theorem SimpleGraph.coe_recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α Fintype.card β) :
                        (G.recolorOfCardLE hαβ) = (SimpleGraph.Embedding.completeGraph .some).toHom.comp
                        theorem SimpleGraph.Colorable.mono {V : Type u} {G : SimpleGraph V} {n : } {m : } (h : n m) (hc : G.Colorable n) :
                        G.Colorable m
                        theorem SimpleGraph.Coloring.colorable {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] (C : G.Coloring α) :
                        G.Colorable (Fintype.card α)
                        theorem SimpleGraph.colorable_of_fintype {V : Type u} (G : SimpleGraph V) [Fintype V] :
                        G.Colorable (Fintype.card V)
                        noncomputable def SimpleGraph.Colorable.toColoring {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] {n : } (hc : G.Colorable n) (hn : n Fintype.card α) :
                        G.Coloring α

                        Noncomputably get a coloring from colorability.

                        Equations
                        Instances For
                          theorem SimpleGraph.Colorable.of_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_3} {G' : SimpleGraph V'} (f : G ↪g G') {n : } (h : G'.Colorable n) :
                          G.Colorable n
                          theorem SimpleGraph.colorable_iff_exists_bdd_nat_coloring {V : Type u} {G : SimpleGraph V} (n : ) :
                          G.Colorable n ∃ (C : G.Coloring ), ∀ (v : V), C v < n
                          theorem SimpleGraph.colorable_set_nonempty_of_colorable {V : Type u} {G : SimpleGraph V} {n : } (hc : G.Colorable n) :
                          {n : | G.Colorable n}.Nonempty
                          theorem SimpleGraph.chromaticNumber_bddBelow {V : Type u} {G : SimpleGraph V} :
                          BddBelow {n : | G.Colorable n}
                          theorem SimpleGraph.Colorable.chromaticNumber_le {V : Type u} {G : SimpleGraph V} {n : } (hc : G.Colorable n) :
                          G.chromaticNumber n
                          theorem SimpleGraph.chromaticNumber_ne_top_iff_exists {V : Type u} {G : SimpleGraph V} :
                          G.chromaticNumber ∃ (n : ), G.Colorable n
                          theorem SimpleGraph.chromaticNumber_le_iff_colorable {V : Type u} {G : SimpleGraph V} {n : } :
                          G.chromaticNumber n G.Colorable n
                          @[deprecated SimpleGraph.Colorable.chromaticNumber_le]
                          theorem SimpleGraph.chromaticNumber_le_card {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] (C : G.Coloring α) :
                          G.chromaticNumber (Fintype.card α)
                          theorem SimpleGraph.colorable_chromaticNumber {V : Type u} {G : SimpleGraph V} {m : } (hc : G.Colorable m) :
                          G.Colorable G.chromaticNumber.toNat
                          theorem SimpleGraph.colorable_chromaticNumber_of_fintype {V : Type u} (G : SimpleGraph V) [Finite V] :
                          G.Colorable G.chromaticNumber.toNat
                          theorem SimpleGraph.chromaticNumber_eq_zero_of_isempty {V : Type u} (G : SimpleGraph V) [IsEmpty V] :
                          G.chromaticNumber = 0
                          theorem SimpleGraph.isEmpty_of_chromaticNumber_eq_zero {V : Type u} (G : SimpleGraph V) [Finite V] (h : G.chromaticNumber = 0) :
                          theorem SimpleGraph.chromaticNumber_pos {V : Type u} {G : SimpleGraph V} [Nonempty V] {n : } (hc : G.Colorable n) :
                          0 < G.chromaticNumber
                          theorem SimpleGraph.colorable_of_chromaticNumber_ne_top {V : Type u} {G : SimpleGraph V} (h : G.chromaticNumber ) :
                          G.Colorable G.chromaticNumber.toNat
                          theorem SimpleGraph.Colorable.mono_left {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') {n : } (hc : G'.Colorable n) :
                          G.Colorable n
                          theorem SimpleGraph.chromaticNumber_le_of_forall_imp {V : Type u} {G : SimpleGraph V} {V' : Type u_3} {G' : SimpleGraph V'} (h : ∀ (n : ), G'.Colorable nG.Colorable n) :
                          G.chromaticNumber G'.chromaticNumber
                          theorem SimpleGraph.chromaticNumber_mono {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph V) (h : G G') :
                          G.chromaticNumber G'.chromaticNumber
                          theorem SimpleGraph.chromaticNumber_mono_of_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_3} {G' : SimpleGraph V'} (f : G ↪g G') :
                          G.chromaticNumber G'.chromaticNumber
                          theorem SimpleGraph.card_le_chromaticNumber_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] :
                          (Fintype.card α) G.chromaticNumber ∀ (C : G.Coloring α), Function.Surjective C
                          theorem SimpleGraph.le_chromaticNumber_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {n : } :
                          n G.chromaticNumber ∀ (C : G.Coloring (Fin n)), Function.Surjective C
                          theorem SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] (hG : G.Colorable (Fintype.card α)) :
                          G.chromaticNumber = (Fintype.card α) ∀ (C : G.Coloring α), Function.Surjective C
                          theorem SimpleGraph.chromaticNumber_eq_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {n : } (hG : G.Colorable n) :
                          G.chromaticNumber = n ∀ (C : G.Coloring (Fin n)), Function.Surjective C
                          theorem SimpleGraph.chromaticNumber_bot {V : Type u} [Nonempty V] :
                          .chromaticNumber = 1
                          @[simp]
                          theorem SimpleGraph.chromaticNumber_top {V : Type u} [Fintype V] :
                          .chromaticNumber = (Fintype.card V)

                          The bicoloring of a complete bipartite graph using whether a vertex is on the left or on the right.

                          Equations
                          Instances For

                            Cliques #

                            theorem SimpleGraph.IsClique.card_le_of_coloring {V : Type u} {G : SimpleGraph V} {α : Type u_1} {s : Finset V} (h : G.IsClique s) [Fintype α] (C : G.Coloring α) :
                            s.card Fintype.card α
                            theorem SimpleGraph.IsClique.card_le_of_colorable {V : Type u} {G : SimpleGraph V} {s : Finset V} (h : G.IsClique s) {n : } (hc : G.Colorable n) :
                            s.card n
                            theorem SimpleGraph.IsClique.card_le_chromaticNumber {V : Type u} {G : SimpleGraph V} {s : Finset V} (h : G.IsClique s) :
                            s.card G.chromaticNumber
                            theorem SimpleGraph.Colorable.cliqueFree {V : Type u} {G : SimpleGraph V} {n : } {m : } (hc : G.Colorable n) (hm : n < m) :
                            G.CliqueFree m
                            theorem SimpleGraph.cliqueFree_of_chromaticNumber_lt {V : Type u} {G : SimpleGraph V} {n : } (hc : G.chromaticNumber < n) :
                            G.CliqueFree n