feat(Combinatorics/SimpleGraph/Maps): characterize neighborSet and edgeSet across an embedding (#35628)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -88,9 +88,21 @@ theorem edgeSet_map (f : V ↪ W) (G : SimpleGraph V) :
     rw [Embedding.sym2Map_apply, Sym2.map_mk, Sym2.eq_iff] at he
     exact he.elim (fun ⟨h, h'⟩ ↦ ⟨_, _, hadj, h, h'⟩) (fun ⟨h', h⟩ ↦ ⟨_, _, hadj.symm, h, h'⟩)
 
+@[simp]
+theorem neighborSet_map (f : V ↪ W) (v : V) :
+    (G.map f).neighborSet (f v) = f '' G.neighborSet v := by
+  refine Set.ext fun u ↦ ⟨?_, ?_⟩
+  · exact fun ⟨hne, v', u', hadj, hv, hu⟩ ↦ ⟨u', f.injective hv ▸ hadj, hu⟩
+  · exact fun ⟨u', hadj, hu⟩ ↦ ⟨hu ▸ f.injective.ne hadj.ne, v, u', hadj, rfl, hu⟩
+
 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
 
+variable {G} in
+theorem map_adj_apply' {f : V → W} (hadj : G.Adj u v) (hne : f u ≠ f v) :
+    (G.map f).Adj (f u) (f v) :=
+  ⟨hne, u, v, hadj, 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⟩
@@ -329,9 +341,23 @@ theorem map_adj {v w : V} (h : G.Adj v w) : G'.Adj (f v) (f w) :=
 theorem map_mem_edgeSet {e : Sym2 V} (h : e ∈ G.edgeSet) : e.map f ∈ G'.edgeSet :=
   Sym2.ind (fun _ _ => f.map_rel') e h
 
+theorem subset_preimage_edgeSet : G.edgeSet ⊆ Sym2.map f ⁻¹' G'.edgeSet :=
+  fun _ ↦ f.map_mem_edgeSet
+
+theorem image_edgeSet_subset : Sym2.map f '' G.edgeSet ⊆ G'.edgeSet :=
+  Set.image_subset_iff.mpr f.subset_preimage_edgeSet
+
 theorem apply_mem_neighborSet {v w : V} (h : w ∈ G.neighborSet v) : f w ∈ G'.neighborSet (f v) :=
   map_adj f h
 
+variable (v) in
+theorem subset_preimage_neighborSet : G.neighborSet v ⊆ f ⁻¹' G'.neighborSet (f v) :=
+  fun _ ↦ f.apply_mem_neighborSet
+
+variable (v) in
+theorem image_neighborSet_subset : f '' G.neighborSet v ⊆ G'.neighborSet (f v) :=
+  Set.image_subset_iff.mpr <| f.subset_preimage_neighborSet v
+
 /-- The map between edge sets induced by a homomorphism.
 The underlying map on edges is given by `Sym2.map`. -/
 @[simps]
@@ -364,6 +390,11 @@ theorem mapEdgeSet.injective (hinj : Function.Injective f) : Function.Injective
   repeat rw [Subtype.mk_eq_mk]
   apply Sym2.map.injective hinj
 
+@[gcongr]
+theorem _root_.SimpleGraph.neighborSet_mono (hle : G₁ ≤ G₂) (v : V) :
+    G₁.neighborSet v ⊆ G₂.neighborSet v :=
+  subset_preimage_neighborSet v <| .ofLE hle
+
 /-- Every graph homomorphism from a complete graph is injective. -/
 theorem injective_of_top_hom (f : (⊤ : SimpleGraph V) →g G') : Function.Injective f := by
   intro v w h
@@ -419,9 +450,18 @@ abbrev toHom : G →g G' :=
 theorem map_mem_edgeSet_iff {e : Sym2 V} : e.map f ∈ G'.edgeSet ↔ e ∈ G.edgeSet :=
   Sym2.ind (fun _ _ => f.map_adj_iff) e
 
+@[simp]
+theorem preimage_edgeSet : Sym2.map f ⁻¹' G'.edgeSet = G.edgeSet :=
+  Set.ext fun _ ↦ map_mem_edgeSet_iff f
+
 theorem apply_mem_neighborSet_iff {v w : V} : f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v :=
   map_adj_iff f
 
+variable (v) in
+@[simp]
+theorem preimage_neighborSet : f ⁻¹' G'.neighborSet (f v) = G.neighborSet v :=
+  Set.ext fun _ ↦ apply_mem_neighborSet_iff f
+
 /-- A graph embedding induces an embedding of edge sets. -/
 @[simps]
 def mapEdgeSet : G.edgeSet ↪ G'.edgeSet where
@@ -574,6 +614,10 @@ theorem map_mem_edgeSet_iff {e : Sym2 V} : e.map f ∈ G'.edgeSet ↔ e ∈ G.ed
 theorem apply_mem_neighborSet_iff {v w : V} : f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v :=
   map_adj_iff f
 
+theorem image_neighborSet : f '' G.neighborSet v = G'.neighborSet (f v) := by
+  rw [← f.toEmbedding.preimage_neighborSet]
+  apply Equiv.image_preimage
+
 @[simp]
 theorem symm_toHom_comp_toHom : f.symm.toHom.comp f.toHom = Hom.id := by
   ext v
@@ -666,6 +710,18 @@ theorem coe_comp (f' : G' ≃g G'') (f : G ≃g G') : ⇑(f'.comp f) = f' ∘ f
 
 end Iso
 
+theorem neighborSet_comap (f : V → W) (v : V) :
+    (G'.comap f).neighborSet v = f ⁻¹' G'.neighborSet (f v) :=
+  rfl
+
+theorem neighborSet_induce (s : Set V) (v : s) :
+    (G.induce s).neighborSet v = (↑) ⁻¹' G.neighborSet v :=
+  G.neighborSet_comap _ v
+
+theorem neighborSet_map_equiv (e : V ≃ W) (w : W) :
+    (G.map e).neighborSet w = e.symm ⁻¹' G.neighborSet (e.symm w) :=
+  Iso.map e G |>.symm.toEmbedding.preimage_neighborSet w |>.symm
+
 /-- The graph induced on `Set.univ` is isomorphic to the original graph. -/
 @[simps!]
 def induceUnivIso (G : SimpleGraph V) : G.induce Set.univ ≃g G where