English
Let φ be a Prefunctor V → V′, Φ a functor FreeGroupoid V → V′, and hΦ the equation (of V) ⋙ Φ.toPrefunctor = φ. Then Φ = lift φ.
Русский
Пусть φ — префунктор, Φ — функтор FreeGroupoid V → V′ и дано равенство, затем Φ = lift φ.
LaTeX
$$$\\Phi = \\mathrm{lift}\\; φ$ given $h\\Phi : (\\mathrm{of}\\ V) \\; ⋙ \\; Φ.toPrefunctor = φ$$$
Lean4
theorem lift_unique (φ : V ⥤q V') (Φ : FreeGroupoid V ⥤ V') (hΦ : of V ⋙q Φ.toPrefunctor = φ) : Φ = lift φ :=
by
apply Quotient.lift_unique
apply Paths.lift_unique
fapply @Quiver.Symmetrify.lift_unique _ _ _ _ _ _ _ _ _
· rw [← Functor.toPrefunctor_comp]
exact hΦ
· rintro X Y f
simp only [← Functor.toPrefunctor_comp, Prefunctor.comp_map, Paths.of_map]
change
Φ.map (Groupoid.inv ((Quotient.functor redStep).toPrefunctor.map f.toPath)) =
Groupoid.inv (Φ.map ((Quotient.functor redStep).toPrefunctor.map f.toPath))
have := Functor.map_inv Φ ((Quotient.functor redStep).toPrefunctor.map f.toPath)
convert this <;> simp only [Groupoid.inv_eq_inv]
