English
If every φ.star_u is surjective, then for every u, φ.pathStar_u is surjective.
Русский
Если для всех u отображение φ.star_u сюръективно, то φ.pathStar_u сюръективно для каждого u.
LaTeX
$$PathStar_surjective$$
Lean4
theorem pathStar_surjective (hφ : ∀ u, Surjective (φ.star u)) (u : U) : Surjective (φ.pathStar u) :=
by
dsimp +unfoldPartialApp [Prefunctor.pathStar, Quiver.PathStar.mk]
rintro ⟨v, p⟩
induction p with
| nil =>
use ⟨u, Path.nil⟩
simp only [Prefunctor.mapPath_nil]
| cons p' ev ih =>
obtain ⟨⟨u', q'⟩, h⟩ := ih
simp only at h
obtain ⟨rfl, rfl⟩ := h
obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩
simp only [star_apply, Sigma.mk.inj_iff] at k
obtain ⟨rfl, k⟩ := k
simp only [heq_eq_eq] at k
subst k
use ⟨_, q'.cons eu⟩
simp only [Prefunctor.mapPath_cons]
