feat(Combinatorics/SimpleGraph/Coloring/EdgeColoring): create a basic edge-coloring API by SnirBroshi · Pull Request #33313 · leanprover-community/mathlib4

SnirBroshi · 2025-12-26T15:55:38Z

Future work (which I'm working on):

Relating degrees to edge-colorability (G.maxDegree ≤ G.chromaticIndex)
Vizing's theorem (G.chromaticIndex ≤ G.maxDegree + 1)
chromaticIndex ⊤ = (if Even #V then #V - 1 else #V)
[Infinite α] → chromaticIndex ⊤ = ⊤

depends on: [Merged by Bors] - feat(Combinatorics/SimpleGraph/LineGraph): lift copies/isomorphisms to line-graph #33292

github-actions · 2025-12-26T15:56:42Z

PR summary b31b601893

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeColoring` (new file)	1041

Declarations diff

+ EdgeColorable
+ EdgeColorable.anti
+ EdgeColorable.chromaticIndex_le
+ EdgeColorable.chromaticIndex_of_finite
+ EdgeColorable.chromaticIndex_pos
+ EdgeColorable.mono
+ EdgeColorable.of_bot
+ EdgeColorable.of_fintype
+ EdgeColorable.of_isContained
+ EdgeColorable.of_iso
+ EdgeColorable.of_lineGraph_hom
+ EdgeColorable.of_lineGraph_iso
+ EdgeColorableWith
+ EdgeColorableWith.anti
+ EdgeColorableWith.mono
+ EdgeColorableWith.of_bot
+ EdgeColorableWith.of_isContained
+ EdgeColorableWith.of_iso
+ EdgeColorableWith.of_lineGraph_hom
+ EdgeColorableWith.of_lineGraph_iso
+ EdgeColoring
+ EdgeColoring.apply_eq_iff_of_adj
+ EdgeColoring.colorClassSubgraph
+ EdgeColoring.edgeColorable
+ EdgeColoring.id
+ EdgeColoring.isMatching_colorClassSubgraph
+ EdgeColoring.ne_of_adj_lineGraph
+ EdgeColoring.ofBot
+ EdgeColoring.ofColorEmbedding
+ EdgeColoring.ofColorIso
+ EdgeColoring.ofCopy
+ EdgeColoring.ofIsSubgraph
+ EdgeColoring.ofIso
+ EdgeColoring.ofLineGraphHom
+ EdgeColoring.ofLineGraphIso
+ IsContained.chromaticIndex_le
+ Iso.chromaticIndex_eq
+ chromaticIndex
+ chromaticIndex_bot
+ chromaticIndex_eq_iff_edgeColorable_not_edgeColorable
+ chromaticIndex_eq_of_lineGraph_iso
+ chromaticIndex_le_iff_edgeColorable
+ chromaticIndex_le_of_lineGraph_hom
+ chromaticIndex_le_one_of_subsingleton
+ chromaticIndex_mono
+ chromaticIndex_ne_top_iff_exists
+ edgeColorableWith_iff_of_isEmpty
+ edgeColorable_chromaticIndex_iff
+ edgeColorable_zero_iff
+ eq_bot_of_chromaticIndex_eq_zero
+ instance : Coe (G.EdgeColoring α) (G.EdgeLabeling α)
+ two_le_chromaticIndex_of_adj

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib-dependent-issues · 2026-03-22T13:21:47Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Combinatorics/SimpleGraph/LineGraph): lift copies/isomorphisms to line-graph #33292~~
By Dependent Issues (🤖). Happy coding!

…oloring API

ooovi

Thanks for your PR! :)

Please put periods at the end of your docstrings.

Also consider moving the Coloring.lean file in the parent directory to the Coloring folder and renaming it to Basic.lean.

Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeColoring.lean

Mathlib/Combinatorics/SimpleGraph/Coloring/Edges.lean

SnirBroshi · 2026-04-01T13:20:26Z

Thanks for your PR! :)

Thank you for reviewing!

Please put periods at the end of your docstrings.

I really prefer them without periods, unless there's more than one sentence.
By my count ~15% of docstrings in Mathlib don't end with a period, and the style guide shows period-less docstrings as valid.
So I think this is currently author's choice, until the maintainers decide to change the style guide.

Also consider moving the Coloring.lean file in the parent directory to the Coloring folder and renaming it to Basic.lean.

Should I do in this PR or a separate one? Also, my plan was to have something like:

Coloring/Vertices.lean
Coloring/Edges.lean
Coloring/ListVertices.lean
Coloring/ListEdges.lean
Coloring/ChromaticPolynomial.lean

or (if that sounds weird)

Coloring/VertexColoring.lean
Coloring/EdgeColoring.lean
Coloring/VertexListColoring.lean
Coloring/EdgeListColoring.lean
Coloring/ChromaticPolynomial.lean

wdyt? I agree that vertex coloring is the simplest one, but making it Basic.lean seems wrong.

ooovi · 2026-04-01T17:20:06Z

I really prefer them without periods, unless there's more than one sentence. By my count ~15% of docstrings in Mathlib don't end with a period, and the style guide shows period-less docstrings as valid. So I think this is currently author's choice, until the maintainers decide to change the style guide.

I'm afraid the documentation style guide indeed recommends that "If a doc string is a complete sentence, then it should end in a period.". Then again, many of yours are not complete sentences :)

Should I do in this PR or a separate one?

It should be a separate PR just moving the file, and then another one that deprecates the module, since those are easy to approve. This PR can then depend on them.

wdyt? I agree that vertex coloring is the simplest one, but making it Basic.lean seems wrong.

I also feel its wrong. I even remember being disappointed to find that SimpleGraph.Coloring was not the flavour I was looking for. It might even make sense to rename SimpleGraph.Coloring to SimpleGraph.VertexColoring in a separate PR, since afaict the literature just calls a graph coloring whatever it is currently interested in.

How about SimpleGraph/Labeling/VertexColoring.lean, so Labeling.lean can also live there?

SnirBroshi · 2026-04-01T21:24:09Z

I think coloring is a major part of graph-theory so we should have a Coloring/ folder.
EdgeLabeling is only for Ramsey's theorem. Maybe it can just live in Coloring/? Ramsey's theorem is also about colors, they just don't have any restrictions like actual coloring.

…oloring/VertexColoring.lean` (#37525) This is in preparation of #33313 and other material to come, here's how I imagine the folder to look like: - `Coloring/VertexColoring.lean` (currently `Coloring.lean`) - `Coloring/EdgeColoring.lean` - `Coloring/VertexListColoring.lean` - `Coloring/EdgeListColoring.lean` - `Coloring/ChromaticPolynomial.lean` - `Coloring/EdgeLabeling.lean` (currently `./EdgeLabeling.lean`) - `Coloring/ConcreteColorings.lean` (currently `./ConcreteColorings.lean`)

mathlib-merge-conflicts · 2026-04-02T10:14:28Z

This pull request has conflicts, please merge master and resolve them.

ooovi · 2026-04-02T17:27:57Z

Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeColoring.lean

+  simpa using isEmpty_of_chromaticNumber_eq_zero h
+
+/-- Lift an embedding of colors to an embedding of edge colorings. -/
+def EdgeColoring.ofColorEmbedding (f : α ↪ β) : G.EdgeColoring α ↪ G.EdgeColoring β :=


Suggested change

def EdgeColoring.ofColorEmbedding (f : α ↪ β) : G.EdgeColoring α ↪ G.EdgeColoring β :=

def EdgeColoring.ofEmbedding (f : α ↪ β) : G.EdgeColoring α ↪ G.EdgeColoring β :=

ooovi · 2026-04-02T17:28:01Z

Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeColoring.lean

+  recolorOfEmbedding _ f
+
+/-- Lift an isomorphism of colors to an isomorphism of edge colorings. -/
+def EdgeColoring.ofColorIso (f : α ≃ β) : G.EdgeColoring α ≃ G.EdgeColoring β :=


Suggested change

def EdgeColoring.ofColorIso (f : α ≃ β) : G.EdgeColoring α ≃ G.EdgeColoring β :=

def EdgeColoring.congr (f : α ≃ β) : G.EdgeColoring α ≃ G.EdgeColoring β :=

maybe? or maybe edgeColoringEquivOfEquiv outside of the EdgeLabelling namespace? The current name is probably not suitable.

edgeColoringEquivOfEquiv and edgeColoringEquivOfIso would then be separated by a slight technicality in naming. Are you sure?
I agree on un-namespacing this one, since it would allow for dot-notation on graphs.

ooovi · 2026-04-02T17:28:03Z

Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeColoring.lean

+
+variable (α) in
+/-- Edge-colorings of graphs with isomorphic line-graphs are equivalent. -/
+def EdgeColoring.ofLineGraphIso (f : G.lineGraph ≃g G'.lineGraph) :


Suggested change

def EdgeColoring.ofLineGraphIso (f : G.lineGraph ≃g G'.lineGraph) :

def edgeColoringEquivOfLineGraphIso (f : G.lineGraph ≃g G'.lineGraph) :

ooovi · 2026-04-02T17:28:05Z

Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeColoring.lean

+
+variable (α) in
+/-- Edge-colorings of isomorphic graphs are equivalent. -/
+def EdgeColoring.ofIso (f : G ≃g G') : G.EdgeColoring α ≃ G'.EdgeColoring α :=


Suggested change

def EdgeColoring.ofIso (f : G ≃g G') : G.EdgeColoring α ≃ G'.EdgeColoring α :=

def edgeColoringEquivOfIso (f : G ≃g G') : G.EdgeColoring α ≃ G'.EdgeColoring α :=

What's wrong with namespacing? (ditto for EdgeColoring.ofLineGraphIso)

Actually how about Iso.edgeColoringEquiv for dot notation on Iso?

…oloring/VertexColoring.lean` (leanprover-community#37525) This is in preparation of leanprover-community#33313 and other material to come, here's how I imagine the folder to look like: - `Coloring/VertexColoring.lean` (currently `Coloring.lean`) - `Coloring/EdgeColoring.lean` - `Coloring/VertexListColoring.lean` - `Coloring/EdgeListColoring.lean` - `Coloring/ChromaticPolynomial.lean` - `Coloring/EdgeLabeling.lean` (currently `./EdgeLabeling.lean`) - `Coloring/ConcreteColorings.lean` (currently `./ConcreteColorings.lean`)

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 26, 2025

SnirBroshi added the t-combinatorics Combinatorics label Dec 26, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 26, 2025

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 22, 2026

mathlib-dependent-issues bot deleted a comment from mathlib4-dependent-issues-bot Mar 22, 2026

SnirBroshi force-pushed the feature/simple-graph/edge-coloring branch from 151cba8 to 115da59 Compare March 22, 2026 14:46

SnirBroshi changed the title ~~feat(Combinatorics/SimpleGraph/EdgeColoring): create a basic edge-coloring API~~ feat(Combinatorics/SimpleGraph/Coloring/Edges): create a basic edge-coloring API Mar 22, 2026

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 22, 2026

feat(Combinatorics/SimpleGraph/Coloring/Edges): create a basic edge-c…

e40eb80

…oloring API

SnirBroshi force-pushed the feature/simple-graph/edge-coloring branch from 115da59 to e40eb80 Compare March 22, 2026 14:47

SnirBroshi added 2 commits March 22, 2026 16:50

Happy new year

7f67a69

style and gcongr

f2ed25a

ooovi reviewed Apr 1, 2026

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeColoring.lean Show resolved Hide resolved

Mathlib/Combinatorics/SimpleGraph/Coloring/Edges.lean Outdated Show resolved Hide resolved

SnirBroshi added 3 commits April 1, 2026 16:21

Merge branch 'master' into feature/simple-graph/edge-coloring

6a4739b

rename chromaticIndex_pos -> EdgeColorable.chromaticIndex_pos

95b507d

add EdgeColoring.apply_eq_iff_of_adj

84ccab0

SnirBroshi added 4 commits April 2, 2026 02:02

rename Coloring/Edges.lean -> Coloring/EdgeColoring.lean

e16c03c

docstring periods

2f28b44

add a different spelling of map_adj

0ce49d2

mk_all

73d9282

SnirBroshi mentioned this pull request Apr 1, 2026

[Merged by Bors] - chore(Combinatorics/SimpleGraph/Coloring): move Coloring.lean to Coloring/VertexColoring.lean #37525

Closed

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2026

SnirBroshi changed the title ~~feat(Combinatorics/SimpleGraph/Coloring/Edges): create a basic edge-coloring API~~ feat(Combinatorics/SimpleGraph/Coloring/EdgeColoring): create a basic edge-coloring API Apr 2, 2026

Merge branch 'master' into feature/simple-graph/edge-coloring

a4c41b3

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2026

update import

693331b

ooovi reviewed Apr 2, 2026

View reviewed changes

	def EdgeColoring.ofColorEmbedding (f : α ↪ β) : G.EdgeColoring α ↪ G.EdgeColoring β :=
	def EdgeColoring.ofEmbedding (f : α ↪ β) : G.EdgeColoring α ↪ G.EdgeColoring β :=

	def EdgeColoring.ofColorIso (f : α ≃ β) : G.EdgeColoring α ≃ G.EdgeColoring β :=
	def EdgeColoring.congr (f : α ≃ β) : G.EdgeColoring α ≃ G.EdgeColoring β :=

	def EdgeColoring.ofLineGraphIso (f : G.lineGraph ≃g G'.lineGraph) :
	def edgeColoringEquivOfLineGraphIso (f : G.lineGraph ≃g G'.lineGraph) :

	def EdgeColoring.ofIso (f : G ≃g G') : G.EdgeColoring α ≃ G'.EdgeColoring α :=
	def edgeColoringEquivOfIso (f : G ≃g G') : G.EdgeColoring α ≃ G'.EdgeColoring α :=

Conversation

SnirBroshi commented Dec 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary b31b601893

Import changes for modified files

Declarations diff

Uh oh!

mathlib-dependent-issues bot commented Mar 22, 2026

Uh oh!

ooovi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

SnirBroshi commented Apr 1, 2026

Uh oh!

ooovi commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SnirBroshi commented Apr 1, 2026

Uh oh!

mathlib-merge-conflicts bot commented Apr 2, 2026

Uh oh!

ooovi Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

ooovi Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

ooovi Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

ooovi Apr 2, 2026

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Apr 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

SnirBroshi commented Dec 26, 2025 •

edited

Loading

github-actions bot commented Dec 26, 2025 •

edited

Loading

ooovi commented Apr 1, 2026 •

edited

Loading

SnirBroshi Apr 2, 2026 •

edited

Loading