feat(Combinatorics/SimpleGraph/Coloring): add lemmas about coloring and maps by IvanRenison · Pull Request #37598 · leanprover-community/mathlib4

IvanRenison · 2026-04-03T14:30:38Z

Idea from this Zulip thread: graph theory>Second Order Monadic Logic for Graph

github-actions · 2026-04-03T14:31:39Z

PR summary 6a7332dd00

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Coloring.ofHom
+ Hom.chromaticNumber_le
+ Iso.chromaticNumber_eq
+ Iso.colorable_iff
+ Iso.coloringEquiv
+ homCongr

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).

b-mehta

Thanks!

bors d+

Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean

mathlib-bors · 2026-04-03T14:35:33Z

✌️ IvanRenison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean

b-mehta · 2026-04-03T15:23:41Z

bors d-

Since Snir's suggestions are wise

mathlib-bors · 2026-04-03T15:23:44Z

🚫 All delegations have been removed from this PR. To re-add a delegation, reply with bors d+ (to delegate the PR author) or bors d=list,of,github,usernames to delegate multiple users.

Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean

IvanRenison · 2026-04-04T18:39:44Z

Mathlib/Combinatorics/SimpleGraph/Maps.lean

+/-- Equivalence of homomorphisms induced by isomorphisms of graphs. -/
+def homCongr (f' : G'' ≃g G''') : G →g G'' ≃ G' →g G''' := RelIso.relHomCongr f f'


I'm not sure if having this is a good idea, or if we should use the RelIso version directly. What do you think?

Probe lemmas about coloring, homomorphisms and isomorphisms

def1e44

github-actions bot added the t-combinatorics Combinatorics label Apr 3, 2026

b-mehta reviewed Apr 3, 2026

View reviewed changes

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

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 3, 2026