Chromatic symmetric function

DefinitionChromatic profile count#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), let \(k\) be a natural number and let \(m : \{0, \dots, k-1\} \to \mathbb{N}\). The chromatic profile count of \(G\) at \(k\) and \(m\) is the number of proper colorings \(c : V \to \{0, \dots, k-1\}\) of \(G\) such that for every color \(i\), exactly \(m(i)\) vertices \(v\) satisfy \(c(v) = i\).

These counts are the coefficients of the chromatic symmetric function.

noncomputable def chromaticProfileCount [Finite V] (G : SimpleGraph V) (k : ℕ)
    (multiplicity : Fin k → ℕ) : ℕ :=
  Nat.card { c : G.Coloring (Fin k) //
    ∀ color, Nat.card { v : V // c v = color } = multiplicity color }

Used by 4

Used byReflexivity of having the same chromatic symmetric function · Graphs with the same chromatic symmetric function · Symmetry of having the same chromatic symmetric function · Transitivity of having the same chromatic symmetric function

DefinitionGraphs with the same chromatic symmetric function#✓fully proved

Let \(G\) and \(H\) be simple graphs on finite vertex sets. We say that \(G\) and \(H\) have the same chromatic symmetric function when, for every natural number \(k\) and every \(m : \{0, \dots, k-1\} \to \mathbb{N}\), the chromatic profile count of \(G\) at \(k\) and \(m\) equals that of \(H\): both graphs have equally many proper colorings with colors \(\{0, \dots, k-1\}\) in which each color \(i\) is used on exactly \(m(i)\) vertices.

This is equality of chromatic symmetric functions, expressed through their coefficients.

def SameChromaticSymmetricFunction [Finite V] [Finite W]
    (G : SimpleGraph V) (H : SimpleGraph W) : Prop :=
  ∀ k multiplicity,
    chromaticProfileCount G k multiplicity = chromaticProfileCount H k multiplicity

Uses 1 · Used by 4

Statement usesChromatic profile count

Used byIsomorphic graphs have the same chromatic symmetric function · Reflexivity of having the same chromatic symmetric function · Symmetry of having the same chromatic symmetric function · Transitivity of having the same chromatic symmetric function

TheoremReflexivity of having the same chromatic symmetric function#✓fully proved

Every simple graph on a finite vertex set has the same chromatic symmetric function as itself.

theorem SameChromaticSymmetricFunction.refl [Finite V] (G : SimpleGraph V) :
    SameChromaticSymmetricFunction G G

Uses 2

Statement usesGraphs with the same chromatic symmetric function

Proof usesChromatic profile count

TheoremSymmetry of having the same chromatic symmetric function#✓fully proved

Let \(G\) and \(H\) be simple graphs on finite vertex sets. If \(G\) has the same chromatic symmetric function as \(H\), then \(H\) has the same chromatic symmetric function as \(G\).

theorem SameChromaticSymmetricFunction.symm
    [Finite V] [Finite W]
    (h : SameChromaticSymmetricFunction G H) : SameChromaticSymmetricFunction H G

Uses 2

Statement usesGraphs with the same chromatic symmetric function

Proof usesChromatic profile count

TheoremTransitivity of having the same chromatic symmetric function#✓fully proved

Let \(G\), \(H\) and \(K\) be simple graphs on finite vertex sets. If \(G\) has the same chromatic symmetric function as \(H\), and \(H\) has the same chromatic symmetric function as \(K\), then \(G\) has the same chromatic symmetric function as \(K\).

theorem SameChromaticSymmetricFunction.trans [Finite V] [Finite W]
    {U : Type*} [Finite U] {K : SimpleGraph U}
    (hGH : SameChromaticSymmetricFunction G H)
    (hHK : SameChromaticSymmetricFunction H K) : SameChromaticSymmetricFunction G K

Uses 2

Statement usesGraphs with the same chromatic symmetric function

Proof usesChromatic profile count

TheoremIsomorphic graphs have the same chromatic symmetric function#✓fully proved

If \(G\) and \(H\) are isomorphic simple graphs on finite vertex sets, then \(G\) and \(H\) have the same chromatic symmetric function.

The proof transports colorings and their color classes along the isomorphism.

theorem SameChromaticSymmetricFunction.of_iso [Finite V] [Finite W] (e : G ≃g H) :
    SameChromaticSymmetricFunction G H

Uses 1

Statement usesGraphs with the same chromatic symmetric function

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.