feat(Combinatorics/SimpleGraph/Hamiltonian): if mapping a Hamiltonian walk results in a path, the mapping function is injective (#36469)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -26,22 +26,25 @@ In this file we introduce Hamiltonian paths, cycles and graphs.
 open Finset Function
 
 namespace SimpleGraph
-variable {α β : Type*} [DecidableEq α] [DecidableEq β] {G : SimpleGraph α}
-  {a b : α} {p : G.Walk a b}
+
+variable {α : Type*} [DecidableEq α] {G : SimpleGraph α}
+variable {β : Type*} [DecidableEq β] {H : SimpleGraph β}
+variable {a b : α} {p : G.Walk a b} {f : G →g H}
 
 namespace Walk
 
 /-- A Hamiltonian path is a walk `p` that visits every vertex exactly once. Note that while
 this definition doesn't contain that `p` is a path, `p.isPath` gives that. -/
 def IsHamiltonian (p : G.Walk a b) : Prop := ∀ a, p.support.count a = 1
 
-lemma IsHamiltonian.map {H : SimpleGraph β} (f : G →g H) (hf : Bijective f) (hp : p.IsHamiltonian) :
+variable (f) in
+lemma IsHamiltonian.map (hf : Bijective f) (hp : p.IsHamiltonian) :
     (p.map f).IsHamiltonian := by
   simp [IsHamiltonian, hf.surjective.forall, hf.injective, hp _]
 
 /-- A Hamiltonian path visits every vertex. -/
-@[simp] lemma IsHamiltonian.mem_support (hp : p.IsHamiltonian) (c : α) : c ∈ p.support := by
-  simp only [← List.count_pos_iff, hp _, Nat.zero_lt_one]
+@[simp] lemma IsHamiltonian.mem_support (hp : p.IsHamiltonian) (c : α) : c ∈ p.support :=
+  p.support.one_le_count_iff.mp <| hp c |>.symm.le
 
 /-- Hamiltonian paths are paths. -/
 lemma IsHamiltonian.isPath (hp : p.IsHamiltonian) : p.IsPath :=
@@ -69,14 +72,21 @@ section
 variable [Fintype α]
 
 /-- The support of a Hamiltonian walk is the entire vertex set. -/
-lemma IsHamiltonian.support_toFinset (hp : p.IsHamiltonian) : p.support.toFinset = Finset.univ := by
+lemma IsHamiltonian.toFinset_support (hp : p.IsHamiltonian) : p.support.toFinset = Finset.univ := by
   simp [eq_univ_iff_forall, hp]
 
+@[deprecated (since := "2026-03-11")]
+alias IsHamiltonian.support_toFinset := IsHamiltonian.toFinset_support
+
+omit [Fintype α] in
+theorem IsHamiltonian.setOf_support (hp : p.IsHamiltonian) : {v | v ∈ p.support} = Set.univ :=
+  Set.eq_univ_iff_forall.mpr hp.mem_support
+
 /-- The length of a Hamiltonian path is one less than the number of vertices of the graph. -/
 lemma IsHamiltonian.length_eq (hp : p.IsHamiltonian) : p.length = Fintype.card α - 1 :=
   eq_tsub_of_add_eq <| by
     rw [← length_support, ← List.sum_toFinset_count_eq_length, Finset.sum_congr rfl fun _ _ ↦ hp _,
-      ← card_eq_sum_ones, hp.support_toFinset, card_univ]
+      ← card_eq_sum_ones, hp.toFinset_support, card_univ]
 
 /-- The length of the support of a Hamiltonian path equals the number of vertices of the graph. -/
 lemma IsHamiltonian.length_support (hp : p.IsHamiltonian) : p.support.length = Fintype.card α := by
@@ -107,6 +117,12 @@ theorem IsHamiltonian.getVert_surjective (hp : p.IsHamiltonian) : p.getVert.Surj
   .of_comp <| p.getVert_comp_val_eq_get_support ▸
     isHamiltonian_iff_support_get_bijective.mp hp |>.surjective
 
+omit [DecidableEq β] in
+theorem IsHamiltonian.injective_of_isPath_map (hp : p.IsHamiltonian) (h : (p.map f).IsPath) :
+    Function.Injective f := by
+  rw [← Set.injOn_univ, ← hp.setOf_support]
+  exact h.injOn_support_of_isPath_map
+
 lemma isHamiltonian_iff_isPath_and_length_eq [Fintype α] :
     p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1 := by
   by_cases! h : IsEmpty α
@@ -126,7 +142,7 @@ variable {p : G.Walk a a}
 lemma IsHamiltonianCycle.isCycle (hp : p.IsHamiltonianCycle) : p.IsCycle :=
   hp.toIsCycle
 
-lemma IsHamiltonianCycle.map {H : SimpleGraph β} (f : G →g H) (hf : Bijective f)
+lemma IsHamiltonianCycle.map (hf : Bijective f)
     (hp : p.IsHamiltonianCycle) : (p.map f).IsHamiltonianCycle where
   toIsCycle := hp.isCycle.map hf.injective
   isHamiltonian_tail := by
@@ -187,7 +203,7 @@ def IsHamiltonian (G : SimpleGraph α) : Prop :=
 
 lemma IsHamiltonian.mono {H : SimpleGraph α} (hGH : G ≤ H) (hG : G.IsHamiltonian) :
     H.IsHamiltonian :=
-  fun hα ↦ let ⟨_, p, hp⟩ := hG hα; ⟨_, p.map <| .ofLE hGH, hp.map _ bijective_id⟩
+  fun hα ↦ let ⟨_, p, hp⟩ := hG hα; ⟨_, p.map <| .ofLE hGH, hp.map bijective_id⟩
 
 lemma not_isHamiltonian_of_isEmpty [IsEmpty α] : ¬G.IsHamiltonian :=
   (IsEmpty.exists_iff.mp <| · <| by simp)

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -60,7 +60,7 @@ variable (G : SimpleGraph V) (G' : SimpleGraph V')
 
 namespace Walk
 
-variable {G} {u u' v w : V}
+variable {G G'} {u u' v w : V} {p : G.Walk u v} {f : G →g G'}
 
 /-! ### Trails, paths, circuits, cycles -/
 
@@ -459,6 +459,17 @@ theorem IsPath.eq_penultimate_of_mem_edges {p : G.Walk u v} (hp : p.IsPath)
     (hmem : s(v, w) ∈ p.edges) : w = p.penultimate := by
   simpa [hmem] using isPath_reverse_iff p |>.mpr hp |>.eq_snd_of_mem_edges (w := w)
 
+theorem IsPath.injOn_support_of_isPath_map (h : (p.map f).IsPath) :
+    Set.InjOn f {w | w ∈ p.support} := by
+  intro u hu v hv hf
+  obtain ⟨u, rfl⟩ := List.get_of_mem hu
+  obtain ⟨v, rfl⟩ := List.get_of_mem hv
+  congr
+  have := List.nodup_iff_injective_getElem.mp h.support_nodup
+  rw! (castMode := .all) [support_map, List.length_map] at this
+  apply this
+  simpa
+
 /-! ### About cycles -/
 
 -- TODO: These results could possibly be less laborious with a periodic function getCycleVert