English
A refined form: if Φ and φ satisfy the same lifting condition, then Φ = lift φ; equivalently, lift is the unique extension of φ to Paths V.
Русский
Уточненная форма: если Φ и φ удовлетворяют одинаковому условию поднятия, то Φ = lift φ; по существу, lift является единственным продолжением φ в Paths V.
LaTeX
$$$\forall φ:\, V \to_q C, \; \forall Φ:\Paths V \to C,\; (Paths.of V) \circ Φ^{toPrefunctor} = φ \Rightarrow Φ = \mathrm{lift}\, φ$$$
Lean4
theorem lift_unique {C} [Category C] (φ : V ⥤q C) (Φ : Paths V ⥤ C) (hΦ : of V ⋙q Φ.toPrefunctor = φ) : Φ = lift φ :=
by
subst_vars
fapply Functor.ext
· rintro X
rfl
· rintro X Y f
dsimp [lift]
induction f with
| nil =>
simp only [Category.comp_id]
apply Functor.map_id
| cons p f'
ih =>
simp only [Category.comp_id,
Category.id_comp] at ih
⊢
-- Porting note: Had to do substitute `p.cons f'` and `f'.toPath` by their fully qualified
-- versions in this `have` clause (elsewhere too).
have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
convert Functor.map_comp Φ p (Quiver.Hom.toPath f')
rw [this, ih]
