English
If every φ.star_u is injective, then for every u, φ.pathStar_u is injective.
Русский
Если для всех u отображение φ.star_u инъективно, то для каждого u отображение φ.pathStar_u инъективно.
LaTeX
$$PathStar_injective$$
Lean4
theorem pathStar_injective (hφ : ∀ u, Injective (φ.star u)) (u : U) : Injective (φ.pathStar u) :=
by
dsimp +unfoldPartialApp [Prefunctor.pathStar, Quiver.PathStar.mk]
rintro ⟨v₁, p₁⟩
induction p₁ with
| nil =>
rintro ⟨y₂, p₂⟩
rcases p₂ with - | ⟨p₂, e₂⟩
· intro;
rfl -- Porting note: goal not present in lean3.
· intro h
simp only [mapPath_cons, Sigma.mk.inj_iff] at h
exfalso
obtain ⟨h, h'⟩ := h
rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h'
exact (Path.nil_ne_cons _ _) h'
| cons p₁ e₁ ih =>
rename_i x₁ y₁
rintro ⟨y₂, p₂⟩
rcases p₂ with - | ⟨p₂, e₂⟩
· intro h
simp only [mapPath_cons, Sigma.mk.inj_iff] at h
exfalso
obtain ⟨h, h'⟩ := h
rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h'
exact (Path.cons_ne_nil _ _) h'
· rename_i x₂
intro h
simp only [mapPath_cons, Sigma.mk.inj_iff] at h
obtain ⟨hφy, h'⟩ := h
rw [← Path.cast_eq_iff_heq rfl hφy, Path.cast_cons, Path.cast_rfl_rfl] at h'
have hφx := Path.obj_eq_of_cons_eq_cons h'
have hφp := Path.heq_of_cons_eq_cons h'
have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons h')
have h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩ := by
simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]; exact ⟨hφx, hφp⟩
cases ih h_path_star
have h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩ := by simp only [Prefunctor.star_apply, Sigma.mk.inj_iff];
exact ⟨hφy, hφe⟩
cases hφ x₁ h_star
rfl
