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

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.

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean

@@ -179,6 +179,13 @@ theorem isEmpty_of_colorable_zero (h : G.Colorable 0) : IsEmpty V := by
 lemma colorable_zero_iff : G.Colorable 0 ↔ IsEmpty V :=
   ⟨isEmpty_of_colorable_zero, fun _ ↦ .of_isEmpty 0⟩
 
+/-- A coloring of a graph `G` is a homomorphism from it to the mapped graph.
+This is `Hom.map` spelled using colorings. The mapped graph `G.map f` can be thought of as taking
+the original graph `G` and considering every color class (independent set) as a single vertex. -/
+@[simps!]
+abbrev Coloring.homMap {α : Type*} (f : G.Coloring α) : G →g G.map f :=
+  .map f G f.map_adj
+
 /-- If `G` is `n`-colorable, then mapping the vertices of `G` produces an `n`-colorable simple
 graph. -/
 theorem Colorable.map (f : V ↪ β) [NeZero n] (hc : G.Colorable n) : (G.map f).Colorable n := by

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -401,6 +401,15 @@ theorem injective_of_top_hom (f : (⊤ : SimpleGraph V) →g G') : Function.Inje
   contrapose! h
   exact G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h))
 
+/-- A function `f` that is injective on adjacent vertices in a graph `G`
+(equivalently `f` is a valid `W`-coloring of `G`, or `G ≤ comap ⊤ f`)
+is a homomorphism from `G` to the mapped graph. -/
+@[simps]
+protected def map (f : V → W) (G : SimpleGraph V) (h : ∀ {u v}, G.Adj u v → f u ≠ f v) :
+    G →g G.map f where
+  toFun := f
+  map_rel' {u v} hadj := ⟨h hadj, u, v, hadj, rfl, rfl⟩
+
 /-- There is a homomorphism to a graph from a comapped graph.
 When the function is injective, this is an embedding (see `SimpleGraph.Embedding.comap`). -/
 @[simps]