feat(Combinatorics/SimpleGraphs): generalize SimpleGraph.map to any function (leanprover-community#36130)

The point is to be able to use map to define graph contractions. Added the injectivity assumption where needed.

Author: vbeffara

Mathlib/Combinatorics/SimpleGraph/Clique.lean

@@ -107,19 +107,19 @@ alias ⟨IsClique.subsingleton, _⟩ := isClique_bot_iff
 
 protected theorem IsClique.map (h : G.IsClique s) {f : α ↪ β} : (G.map f).IsClique (f '' s) := by
   rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab
-  exact ⟨a, b, h ha hb <| ne_of_apply_ne _ hab, rfl, rfl⟩
+  exact ⟨hab, a, b, h ha hb <| ne_of_apply_ne _ hab, rfl, rfl⟩
 
 theorem isClique_map_iff_of_nontrivial {f : α ↪ β} {t : Set β} (ht : t.Nontrivial) :
     (G.map f).IsClique t ↔ ∃ (s : Set α), G.IsClique s ∧ f '' s = t := by
   refine ⟨fun h ↦ ⟨f ⁻¹' t, ?_, ?_⟩, by rintro ⟨x, hs, rfl⟩; exact hs.map⟩
   · rintro x (hx : f x ∈ t) y (hy : f y ∈ t) hne
-    obtain ⟨u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
+    obtain ⟨-, u, v, huv, hux, hvy⟩ := h hx hy (by simpa)
     rw [EmbeddingLike.apply_eq_iff_eq] at hux hvy
     rwa [← hux, ← hvy]
   rw [Set.image_preimage_eq_iff]
   intro x hxt
   obtain ⟨y, hyt, hyne⟩ := ht.exists_ne x
-  obtain ⟨u, v, -, rfl, rfl⟩ := h hyt hxt hyne
+  obtain ⟨-, u, v, -, rfl, rfl⟩ := h hyt hxt hyne
   exact Set.mem_range_self _
 
 theorem isClique_map_iff {f : α ↪ β} {t : Set β} :
@@ -643,7 +643,7 @@ theorem cliqueSet_map (hn : n ≠ 1) (G : SimpleGraph α) (f : α ↪ β) :
       rw [map_eq_image, image_preimage, filter_true_of_mem]
       rintro a ha
       obtain ⟨b, hb, hba⟩ := exists_mem_ne (hn.lt_of_le' <| Finset.card_pos.2 ⟨a, ha⟩) a
-      obtain ⟨c, _, _, hc, _⟩ := hs ha hb hba.symm
+      obtain ⟨-, c, _, _, hc, _⟩ := hs ha hb hba.symm
       exact ⟨c, hc⟩
     refine ⟨s.preimage f f.injective.injOn, ⟨?_, by rw [← card_map f, hs']⟩, hs'⟩
     rw [coe_preimage]
@@ -653,11 +653,11 @@ theorem cliqueSet_map (hn : n ≠ 1) (G : SimpleGraph α) (f : α ↪ β) :
 
 @[simp]
 theorem cliqueSet_map_of_equiv (G : SimpleGraph α) (e : α ≃ β) (n : ℕ) :
-    (G.map e.toEmbedding).cliqueSet n = map e.toEmbedding '' G.cliqueSet n := by
+    (G.map e).cliqueSet n = map e.toEmbedding '' G.cliqueSet n := by
   obtain rfl | hn := eq_or_ne n 1
   · ext
     simp [e.exists_congr_left]
-  · exact cliqueSet_map hn _ _
+  · simpa using cliqueSet_map hn G e.toEmbedding
 
 end CliqueSet
 
@@ -774,8 +774,7 @@ theorem cliqueFinset_map (f : α ↪ β) (hn : n ≠ 1) :
     simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]
 
 @[simp]
-theorem cliqueFinset_map_of_equiv (e : α ≃ β) (n : ℕ) :
-    (G.map e.toEmbedding).cliqueFinset n =
+theorem cliqueFinset_map_of_equiv (e : α ≃ β) (n : ℕ) : (G.map e).cliqueFinset n =
       (G.cliqueFinset n).map ⟨map e.toEmbedding, Finset.map_injective _⟩ :=
   coe_injective <| by push_cast; exact cliqueSet_map_of_equiv _ _ _
 

Mathlib/Combinatorics/SimpleGraph/Coloring.lean

@@ -180,7 +180,7 @@ graph. -/
 theorem Colorable.map (f : V ↪ β) [NeZero n] (hc : G.Colorable n) : (G.map f).Colorable n := by
   obtain ⟨C⟩ := hc
   use extend f C (const β default)
-  intro a b ⟨_, _, hadj, ha, hb⟩
+  intro a b ⟨_, _, _, hadj, ha, hb⟩
   rw [← ha, f.injective.extend_apply, ← hb, f.injective.extend_apply]
   exact C.valid hadj
 

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -50,23 +50,28 @@ variable {V W X : Type*} (G : SimpleGraph V) (G' : SimpleGraph W) {u v : V}
 /-! ## Map and comap -/
 
 
-/-- Given an injective function, there is a covariant induced map on graphs by pushing forward
+/-- Given a function, there is a covariant induced map on graphs by pushing forward
 the adjacency relation.
 
-This is injective (see `SimpleGraph.map_injective`). -/
-protected def map (f : V ↪ W) (G : SimpleGraph V) : SimpleGraph W where
-  Adj := Relation.Map G.Adj f f
+This is injective when the function is (see `SimpleGraph.map_injective`). -/
+protected def map (f : V → W) (G : SimpleGraph V) : SimpleGraph W where
+  Adj := Ne ⊓ Relation.Map G.Adj f f
   symm a b := by
     rintro ⟨v, w, h, _⟩
     aesop (add norm unfold Relation.Map) (add forward safe Adj.symm)
-  loopless := ⟨fun a ↦ by aesop (add norm unfold Relation.Map)⟩
 
-instance instDecidableMapAdj {f : V ↪ W} {a b} [Decidable (Relation.Map G.Adj f f a b)] :
-    Decidable ((G.map f).Adj a b) := ‹Decidable (Relation.Map G.Adj f f a b)›
+instance instDecidableMapAdj [DecidableEq W] {f : V → W} {a b}
+    [Decidable (Relation.Map G.Adj f f a b)] : Decidable ((G.map f).Adj a b) := by
+  dsimp [SimpleGraph.map]; infer_instance
 
 @[simp]
 theorem map_adj (f : V ↪ W) (G : SimpleGraph V) (u v : W) :
-    (G.map f).Adj u v ↔ ∃ u' v' : V, G.Adj u' v' ∧ f u' = u ∧ f v' = v :=
+    (G.map f).Adj u v ↔ ∃ u' v' : V, G.Adj u' v' ∧ f u' = u ∧ f v' = v := by
+  dsimp [SimpleGraph.map, Relation.Map]
+  grind [SimpleGraph.Adj.ne]
+
+theorem map_adj' (f : V → W) (G : SimpleGraph V) (u v : W) :
+    (G.map f).Adj u v ↔ u ≠ v ∧ ∃ u' v' : V, G.Adj u' v' ∧ f u' = u ∧ f v' = v :=
   Iff.rfl
 
 theorem edgeSet_map (f : V ↪ W) (G : SimpleGraph V) :
@@ -86,15 +91,19 @@ theorem edgeSet_map (f : V ↪ W) (G : SimpleGraph V) :
 lemma map_adj_apply {G : SimpleGraph V} {f : V ↪ W} {a b : V} :
     (G.map f).Adj (f a) (f b) ↔ G.Adj a b := by simp
 
-theorem map_monotone (f : V ↪ W) : Monotone (SimpleGraph.map f) := by
-  rintro G G' h _ _ ⟨u, v, ha, rfl, rfl⟩
-  exact ⟨_, _, h ha, rfl, rfl⟩
+theorem map_monotone (f : V → W) : Monotone (SimpleGraph.map f) := by
+  rintro G G' h z1 z2 ⟨huv, u, v, ha, rfl, rfl⟩
+  exact ⟨huv, _, _, h ha, rfl, rfl⟩
 
-@[simp] lemma map_id : G.map (Function.Embedding.refl _) = G :=
-  SimpleGraph.ext <| Relation.map_id_id _
+@[simp] lemma map_id : G.map id = G := by
+  ext
+  dsimp [SimpleGraph.map, Relation.Map]
+  grind [SimpleGraph.Adj.ne]
 
-@[simp] lemma map_map (f : V ↪ W) (g : W ↪ X) : (G.map f).map g = G.map (f.trans g) :=
-  SimpleGraph.ext <| Relation.map_map _ _ _ _ _
+@[simp] lemma map_map (f : V → W) (g : W → X) : (G.map f).map g = G.map (g ∘ f) := by
+  ext
+  dsimp [SimpleGraph.map, Relation.Map]
+  grind [SimpleGraph.Adj.ne]
 
 theorem support_map (f : V ↪ W) (G : SimpleGraph V) :
     (G.map f).support = f '' G.support := by
@@ -154,8 +163,8 @@ theorem comap_surjective (f : V ↪ W) : Function.Surjective (SimpleGraph.comap
 
 theorem map_le_iff_le_comap (f : V ↪ W) (G : SimpleGraph V) (G' : SimpleGraph W) :
     G.map f ≤ G' ↔ G ≤ G'.comap f :=
-  ⟨fun h _ _ ha => h ⟨_, _, ha, rfl, rfl⟩, by
-    rintro h _ _ ⟨u, v, ha, rfl, rfl⟩
+  ⟨fun h _ _ ha => h ⟨f.injective.ne ha.ne, _, _, ha, rfl, rfl⟩, by
+    rintro h _ _ ⟨-, u, v, ha, rfl, rfl⟩
     exact h ha⟩
 
 set_option backward.isDefEq.respectTransparency false in
@@ -578,15 +587,15 @@ protected def comap (f : V ≃ W) (G : SimpleGraph W) : G.comap f.toEmbedding 
 lemma comap_apply (f : V ≃ W) (G : SimpleGraph W) (v : V) :
     SimpleGraph.Iso.comap f G v = f v := rfl
 
+-- Porting note: `@[simps]` does not work here anymore since `f` is not a constructor application.
+-- `@[simps toEmbedding]` could work, but Floris suggested writing `map_apply` for now.
 @[simp]
 lemma comap_symm_apply (f : V ≃ W) (G : SimpleGraph W) (w : W) :
     (SimpleGraph.Iso.comap f G).symm w = f.symm w := rfl
 
-/-- Given an injective function, there is an embedding from a graph into the mapped graph. -/
--- Porting note: `@[simps]` does not work here anymore since `f` is not a constructor application.
--- `@[simps toEmbedding]` could work, but Floris suggested writing `map_apply` for now.
+/-- Given a bijective function, there is an isomorphism from a graph into the mapped graph. -/
 protected def map (f : V ≃ W) (G : SimpleGraph V) : G ≃g G.map f.toEmbedding :=
-  { f with map_rel_iff' := by simp }
+  { f with map_rel_iff' := by aesop (add simp map_adj') }
 
 @[simp]
 lemma map_apply (f : V ≃ W) (G : SimpleGraph V) (v : V) :

Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

@@ -75,7 +75,7 @@ lemma EdgeDisjointTriangles.map (f : α ↪ β) (hG : G.EdgeDisjointTriangles) :
 
 lemma LocallyLinear.map (f : α ↪ β) (hG : G.LocallyLinear) : (G.map f).LocallyLinear := by
   refine ⟨hG.1.map _, ?_⟩
-  rintro _ _ ⟨a, b, h, rfl, rfl⟩
+  rintro _ _ ⟨-, a, b, h, rfl, rfl⟩
   obtain ⟨s, hs, ha, hb⟩ := hG.2 h
   exact ⟨s.map f, hs.map, mem_map_of_mem _ ha, mem_map_of_mem _ hb⟩