edge coloring

Stream: graph theory

[Matthew Ballard]

@Utku Okur and Alec Helm worked on some results for edge colorings of graphs for a recent graduate class here. The repo is uofsc-spring-2023-math-768-001/project1. The current state of the repo might make your eyes bleed though.

Since @Yaël Dillies asked about this on another thread, I thought I should at least record here.

[Kevin Buzzard]

Is the repo public? Right now the hashtag isn't resolving to anything (for me)

[Matthew Ballard]

Thanks. Fixed.

[Matthew Ballard]

The goal was to do the two bounds in terms of maximal degree. We got

theorem maxDegree_le_edgeChromaticNumber [Fintype V] [DecidableRel G.Adj] [Fintype (edgeSet G)] :
    maxDegree G ≤ edgeChromaticNumber G

But not the harder direction. I am not sure if Utku or Alec are planning on working on this.

[Utku Okur]

Would it be considered a constructive proof of Vizing's Theorem, if we use the assumptions:

variable {V : Type} {G : SimpleGraph V} [Fintype V] [CompleteLinearOrder V]

In other words, I assume that there is a linear order on the (finitely many) vertices of the graph and show that its edge chromatic number is bounded above by its maximum degree plus one? I thought that this would avoid "Classical.choose".

[Mitchell Lee]

It should be sufficient to have [Fintype G.edgeSet]. (Roughly, this hypothesis means that there is an explicit bijection between the edge set of $G$ and the set $\{1, \ldots, n\}$, for some $n$.) Then, you may use induction (docs#Finset.induction_on) on G.edgeFinset (docs#SimpleGraph.edgeFinset). The hypotheses of [Fintype V] and [CompleteLinearOrder V] should not be necessary.

[Mitchell Lee]

You will likely need [DecidableEq V] as well, actually.

[Mitchell Lee]

Here is a reference for all the finiteness assumptions that one can make on simple graphs: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/Finite.html