feat(Combinatorics/SimpleGraph/Maps): G →g G.map f

[SnirBroshi]

The existing SimpleGraph.Embedding.map takes an embedding and lifts it to a graph embedding G ↪g G.map f.
#36130 generalized SimpleGraph.map from embeddings to functions, so now we can get a graph homomorphism G →g G.map f without requiring that f is injective, although we still have to require that it is injective on adjacent vertices (aka a valid coloring).
This adds Coloring.homMap, and Hom.map which is identical but avoids coloring terminology/spelling.

---

I'd love for suggestions to improve the docstring of Coloring.homMap, I'm not sure about it :)

Are the two versions a good idea, or should we just have the coloring one? (we have {Hom,Embedding,Iso}.comap but only {Embedding,Iso}.map)

[github-actions]

PR summary e5c3d94642

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Coloring.homMap
+ map

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.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[eric-wieser]

I'd suggest this would be better as an abbrev

[SnirBroshi]

Could you explain why? I thought abbrev is only for defining types that you want instances for (Zulip).
The simps tag provides the API. Do you instead mean @[reducible]?