Color-critical graphs

DefinitionCritical edge sets#✓fully proved

Let \(G\) be a graph and \(S\) a set of unordered pairs of its vertices. Then \(S\) is critical for \(G\) if deleting the edges of \(G\) that lie in \(S\) strictly lowers the chromatic number, as an element of \(\mathbb{N} \cup \{\infty\}\).

def IsCriticalEdges (edges : Set (Sym2 V)) : Prop :=
  (G.deleteEdges edges).chromaticNumber < G.chromaticNumber

Used by 1

Used byCritical edge

DefinitionCritical edge#✓fully proved

For a graph \(G\) and an unordered pair \(e\) of vertices, \(e\) is a critical edge of \(G\) if removing \(e\) from the edge set of \(G\) strictly lowers the chromatic number of \(G\), taken in \(\mathbb{N} \cup \{\infty\}\).

Only edges of \(G\) can be critical.

def IsCriticalEdge (e : Sym2 V) : Prop := G.IsCriticalEdges ({e} : Set (Sym2 V))

Uses 1

Statement usesCritical edge sets

DefinitionCritical vertex sets of a subgraph#✓fully proved

Let \(G'\) be a subgraph of a graph \(G\). A set \(S\) of vertices is critical for \(G'\) if deleting the vertices in \(S\) from \(G'\) strictly lowers the chromatic number of \(G'\), viewed as a graph on its own vertex set, with chromatic numbers taken in \(\mathbb{N} \cup \{\infty\}\).

def Subgraph.IsCriticalVerts (verts : Set V) (G' : G.Subgraph) : Prop :=
  (G'.deleteVerts verts).coe.chromaticNumber < G'.coe.chromaticNumber

Used by 1

Used byCritical vertices of a subgraph

DefinitionCritical vertices of a subgraph#✓fully proved

Let \(G'\) be a subgraph of a graph \(G\). A vertex \(v\) is critical for \(G'\) if \(\{v\}\) is a critical vertex set of \(G'\), that is, deleting \(v\) from \(G'\) strictly lowers the chromatic number of \(G'\), viewed as a graph on its own vertex set, with chromatic numbers taken in \(\mathbb{N} \cup \{\infty\}\).

def Subgraph.IsCriticalVertex (v : V) (G' : G.Subgraph) : Prop := G'.IsCriticalVerts {v}

Uses 1 · Used by 1

Statement usesCritical vertex sets of a subgraph

Used byVertex-critical graphs

DefinitionVertex-critical graphs#✓fully proved

Let \(k\) be a natural number. A graph \(G\) is \(k\)-critical (or vertex-critical) if its chromatic number equals \(k\) and every vertex \(v\) of \(G\) is critical, that is, deleting \(v\) from \(G\) strictly lowers the chromatic number.

def IsCritical (k : ℕ) : Prop := G.chromaticNumber = k ∧ ∀ v, (⊤ : G.Subgraph).IsCriticalVertex v

Uses 1

Statement usesCritical vertices of a subgraph

DefinitionCocolorable graphs#✓fully proved

A graph \(G\) is cocolorable with \(n\) colors if there is a map from its vertices to the colors \(\{0, \dots, n-1\}\) such that each color class induces either an independent set or a complete graph in \(G\).

def Cocolorable (G : SimpleGraph V) (n : ℕ) : Prop := ∃ coloring : V → Fin n,
  ∀ i, G.induce {v | coloring v = i} = ⊥ ∨ G.induce {v | coloring v = i} = ⊤

Used by 5

Used byCochromatic number · Cochromatic number as a minimum · Cochromatic number of a finite graph · Colorable graphs are cocolorable · Finite graphs are cocolorable

TheoremColorable graphs are cocolorable#✓fully proved

For every natural number \(n\), if a graph \(G\) has a proper coloring with \(n\) colors, then \(G\) is cocolorable with \(n\) colors.

Each color class of a proper coloring induces an independent set.

theorem Colorable.cocolorable {n : ℕ} (hc : G.Colorable n) : G.Cocolorable n

Uses 1 · Used by 1

Statement usesCocolorable graphs

Used byFinite graphs are cocolorable

TheoremFinite graphs are cocolorable#✓fully proved

Every graph \(G\) on a finite vertex set \(V\) is cocolorable with \(|V|\) colors.

Giving every vertex its own color is a proper coloring.

theorem cocolorable_of_fintype [Fintype V] (G : SimpleGraph V) :
    G.Cocolorable (Fintype.card V)

Uses 2 · Used by 1

Statement usesCocolorable graphs

Proof usesColorable graphs are cocolorable

Used byCochromatic number of a finite graph

DefinitionCochromatic number#✓fully proved

The cochromatic number of a graph \(G\), an element of \(\mathbb{N} \cup \{\infty\}\), is the least natural number \(n\) such that \(G\) is cocolorable with \(n\) colors, that is, the least number of colors in a coloring of the vertices of \(G\) in which each color class induces either an independent set or a complete graph. It is \(\infty\) exactly when \(G\) is not cocolorable with any finite number of colors.

noncomputable def cochromaticNumber (G : SimpleGraph V) : ℕ∞ := ⨅ n ∈ Set.ofPred G.Cocolorable,
  (n : ℕ∞)

Uses 1 · Used by 4

Statement usesCocolorable graphs

Used byCochromatic number as a minimum · Cochromatic number of a finite graph · Erdős Problem 760: subgraphs of large cochromatic number · Probability of a large chromatic–cochromatic gap

TheoremCochromatic number as a minimum#✓fully proved

If a graph \(G\) is cocolorable with \(n\) colors for some natural number \(n\), then the cochromatic number of \(G\) equals the least natural number \(m\) such that \(G\) is cocolorable with \(m\) colors.

theorem Cocolorable.cochromaticNumber_eq_sInf {n : ℕ} (h : G.Cocolorable n) :
    G.cochromaticNumber = sInf {n' : ℕ | G.Cocolorable n'}

Uses 2 · Used by 1

Statement usesCocolorable graphs · Cochromatic number

Used byCochromatic number of a finite graph

TheoremCochromatic number of a finite graph#✓fully proved

For every graph \(G\) on a finite vertex set, the cochromatic number of \(G\), converted from \(\mathbb{N} \cup \{\infty\}\) to \(\mathbb{N}\) by sending \(\infty\) to \(0\), equals the least natural number \(m\) such that \(G\) is cocolorable with \(m\) colors.

theorem cochromaticNumber_toNat_eq_sInf [Fintype V] (G : SimpleGraph V) :
    G.cochromaticNumber.toNat = sInf {n : ℕ | G.Cocolorable n}

Uses 4

Statement usesCocolorable graphs · Cochromatic number

Proof usesCochromatic number as a minimum · Finite graphs are cocolorable

DefinitionChromatic cardinal of a graph#✓fully proved

The chromatic cardinal is the minimal number of colors need to color it. In contrast to chromaticNumber, which assigns ⊤ : ℕ∞ to all non-finitely colorable graphs, this definition returns a Cardinal and can therefore distinguish between different infinite chromatic numbers.

noncomputable def chromaticCardinal.{u} {V : Type u} (G : SimpleGraph V) : Cardinal :=
  sInf {κ : Cardinal | ∃ (C : Type u) (_ : Cardinal.mk C = κ), Nonempty (G.Coloring C)}

DefinitionLargest union of independent sets#✓fully proved

For a graph \(G\) on a finite vertex set and a natural number \(k\), this is the maximum number of vertices in a union of \(k\) (possibly empty, possibly overlapping) independent sets of \(G\).

noncomputable def indepNumK (G : SimpleGraph V) [Fintype V] (k : ℕ) : ℕ :=
  sSup {n | ∃ f : Fin k → Set V, (∀ i, G.IsIndepSet (f i)) ∧ (⋃ i, f i).ncard = n}

Used by 1

Used byCDS-colorable graphs

DefinitionCDS-colorable graphs#✓fully proved

A graph \(G\) on a finite vertex set is CDS-colorable if it has a proper coloring \(C\) with colors in \(\mathbb{N}\) such that for every \(k \in \mathbb{N}\), the number of vertices whose color under \(C\) is less than \(k\) equals the maximum size of a union of \(k\) independent sets of \(G\).

def CDSColorable [Fintype α] (G : SimpleGraph α) : Prop :=
    ∃ (C : G.Coloring Nat), ∀ k : Nat,
   ∑ i < k, (C.colorClass i).ncard = indepNumK G k

Uses 1

Statement usesLargest union of independent sets

DefinitionRainbow homomorphisms#✓fully proved

Let \(f\) be a graph homomorphism from \(H\) to \(G\) and let \(c\) be a labeling of the edges of \(G\) by elements of a type \(K\). Then \(f\) is rainbow for \(c\) if distinct edges of \(H\) are mapped to edges of \(G\) with distinct labels, that is, the labeling \(e \mapsto c(f(e))\) of the edges of \(H\) is injective.

def IsRainbow {α V K : Type*} {H : SimpleGraph α} {G : SimpleGraph V} (f : H →g G)
    (c : G.EdgeLabeling K) : Prop :=
  Function.Injective (c.pullback f)

Used by 1

Used byAnti-Ramsey number

DefinitionAnti-Ramsey number#✓fully proved

For a graph \(H\) on a finite vertex type and a natural number \(n\), the anti-Ramsey number \(\mathrm{AR}(n, H)\) is the largest \(k\) for which there is a coloring of the edges of the complete graph \(K_n\) on \(\{0, \dots, n-1\}\) with colors \(\{0, \dots, k-1\}\), every color used, that contains no rainbow copy of \(H\). Here a copy of \(H\) is an injective homomorphism from \(H\) to \(K_n\), and it is rainbow when distinct edges of \(H\) are sent to edges of distinct colors. If no such \(k\) exists, \(\mathrm{AR}(n, H) = 0\).

noncomputable def antiRamseyNum {α : Type*} [Fintype α] (H : SimpleGraph α) (n : ℕ) : ℕ :=
  sSup {k | ∃ c : TopEdgeLabeling (Fin n) (Fin k), Function.Surjective c ∧
    ∀ f : H.Copy ⊤, ¬IsRainbow f.toHom c}

Uses 1

Statement usesRainbow homomorphisms

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.