Lax Lean Archive

Colorings of graphs

Lax185574.Colorings · concepts/Lax185574/Colorings.lean · lax-185574

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A coloring of a graph G is an expansion G⁺ of G by finitely many unary predicates. With c predicates, G⁺ is a structure in the signature of graphs expanded by c unary symbols.

    Concept map
    2 concepts; 10 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax710763.Transductions
    2import Mathlib.ModelTheory.Graph
    3
    4/-!
    5---
    6title: Colorings of graphs
    7type: definition
    8---
    9A *coloring* of a graph G is an expansion G⁺ of G by finitely many unary
    10predicates. With c predicates, G⁺ is a structure in the signature of
    11graphs expanded by c unary symbols.
    12
    13# Formalization notes
    14
    15The colored language and the color sets are those of
    16`Lax710763.Transductions`, which the archive's monadic dependence is
    17stated over. The c color sets are arbitrary: they may overlap and need
    18not cover the vertex set. The expansion is the structure of the sum
    19language, which interprets adjacency by `G` and the i-th color by the
    20i-th color set.
    21
    22The main theorem, monadic dependence and the independence property use
    23the formulas of `Lax185574.FirstOrderLogic`, with a coloring given by
    24one set of vertices per color. The statements about types and
    25definability use the formulas of mathlib in the colored language here,
    26since mathlib provides the quantifier rank, parameters and the sets of
    27formulas that types are made of. In both, a coloring with c colors is
    28a family of c sets of vertices, which may overlap.
    29-/
    30
    31namespace Lax185574.Colorings
    32
    33open FirstOrder FirstOrder.Language Lax710763.Transductions
    34
    35universe z
    36
    37variable {V : Type z}
    38
    39/-- The expansion `G⁺` of the graph `G` by the color sets `colors`. -/
    40@[implicit_reducible]
    41def expansion (G : SimpleGraph V) {c : ℕ} (colors : Fin c → Set V) :
    42 (withColors Language.graph c).Structure V :=
    43 @Language.sumStructure _ _ V G.structure (colorStructure colors)
    44
    45end Lax185574.Colorings
    46
    Formalization notes

    The colored language and the color sets are those of Lax710763.TransductionsLax710763.Transductions, which the archive's monadic dependence is stated over. The c color sets are arbitrary: they may overlap and need not cover the vertex set. The expansion is the structure of the sum language, which interprets adjacency by GG and the i-th color by the i-th color set.

    The main theorem, monadic dependence and the independence property use the formulas of Lax185574.FirstOrderLogicLax185574.FirstOrderLogic, with a coloring given by one set of vertices per color. The statements about types and definability use the formulas of mathlib in the colored language here, since mathlib provides the quantifier rank, parameters and the sets of formulas that types are made of. In both, a coloring with c colors is a family of c sets of vertices, which may overlap.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…