Documentation

Complexity.Logics.FirstOrder.Problems.Coloring

Colorability of graph structures #

A structure for Mathlib's language of graphs FirstOrder.Language.graph is a directed graph, possibly with loops. It is n-colorable (graph.Colorable) when its vertices can be colored with n colors so that the two ends of every edge have different colors; a loop makes it uncolorable, and on simple graphs this is SimpleGraph.Colorable. The classes graph.ThreeColorable of three-colorable finite graph structures (3COL, loops allowed) and graph.SimpleThreeColorable of three-colorable finite simple graphs (classical 3COL) are closed under isomorphism and invariant under disjoint copies. Their existential second-order definability is in Complexity.Logics.SecondOrder.Coloring, and the machine-level problem, on graphs encoded as lists of vertices and edges, is Cslib.Complexity.ThreeColoring.

Main definitions #

Main results #

References #

source
def Cslib.Logic.FO.graph.Colorable (n : ℕ) (M : Type u_1) [FirstOrder.Language.graph.Structure M] :
Prop

A graph structure is n-colorable when its vertices can be colored with n colors so that the two ends of every edge have different colors.

Instances For
    source
    def Cslib.Logic.FO.graph.ThreeColorable :
    Set (CategoryTheory.Bundled FirstOrder.Language.graph.Structure)

    3COL: the class of three-colorable graph structures, loops allowed.

    Instances For
      source
      def Cslib.Logic.FO.graph.SimpleThreeColorable :
      Set (CategoryTheory.Bundled FirstOrder.Language.graph.Structure)

      Classical 3COL: the class of three-colorable simple graphs.

      Instances For
        source
        theorem Cslib.Logic.FO.graph.Colorable.of_equiv {M : Type u_2} {N : Type u_3} [FirstOrder.Language.graph.Structure M] [FirstOrder.Language.graph.Structure N] {n : ℕ} (e : FirstOrder.Language.graph.Equiv M N) (h : Colorable n M) :
        Colorable n N

        Colorability is invariant under isomorphism.

        source
        theorem Cslib.Logic.FO.graph.isoClosed_ThreeColorable :
        IsoClosed ThreeColorable

        3COL is closed under isomorphism.

        source
        theorem Cslib.Logic.FO.graph.isoClosed_SimpleThreeColorable :
        IsoClosed SimpleThreeColorable

        Classical 3COL is closed under isomorphism.

        source
        theorem Cslib.Logic.FO.graph.colorable_of_isEmpty {M : Type u_2} [FirstOrder.Language.graph.Structure M] {n : ℕ} [IsEmpty M] :
        Colorable n M

        The empty graph is colorable.

        source
        theorem Cslib.Logic.FO.graph.colorable_copies_iff {J : Type u_1} {M : Type u_2} [FirstOrder.Language.graph.Structure M] {n : ℕ} [Nonempty J] :
        Colorable n (Copies J M) ↔ Colorable n M

        A positive number of disjoint copies of a graph is n-colorable exactly when the graph is.

        source
        theorem Cslib.Logic.FO.graph.simpleGraph_copies_iff {J : Type u_1} {M : Type u_2} [FirstOrder.Language.graph.Structure M] [Nonempty J] :
        Copies J M ⊨ FirstOrder.Language.Theory.simpleGraph ↔ M ⊨ FirstOrder.Language.Theory.simpleGraph

        A positive number of disjoint copies of a graph is a simple graph exactly when the graph is.

        source
        theorem Cslib.Logic.FO.graph.copyInvariant_ThreeColorable :
        CopyInvariant ThreeColorable

        3COL is invariant under copies.

        source
        theorem Cslib.Logic.FO.graph.copyInvariant_SimpleThreeColorable :
        CopyInvariant SimpleThreeColorable

        Classical 3COL is invariant under copies.