English
Let F' be a left Kan extension of F along L. For every target G and morphisms γ1, γ2 : F' ⇒ G, if α ≫ whiskerLeft L γ1 = α ≫ whiskerLeft L γ2, then γ1 = γ2. In words, the map γ ↦ α ≫ whiskerLeft L γ is injective (the universal property yields a unique lift).
Русский
Пусть F' является левой канонической проекции F вдоль L. Для любого отклонения G и гомоморфизмов γ1, γ2 : F' ⇒ G, если α ≫ whiskerLeft L γ1 = α ≫ whiskerLeft L γ2, то γ1 = γ2. Иными словами, отображение γ ↦ α ≫ whiskerLeft L γ инъективно (уникальное поднятие следует из универсальности).
LaTeX
$$$\forall G, \gamma_1, \gamma_2: F' ⟶ G,\; \alpha: F ⟶ L \circ F' :\; \alpha \;\circ\; \mathrm{whiskerLeft}_L(\gamma_1) = \alpha \circ \mathrm{whiskerLeft}_L(\gamma_2) \Rightarrow \gamma_1 = \gamma_2$$$
Lean4
theorem hom_ext_of_isLeftKanExtension {G : D ⥤ H} (γ₁ γ₂ : F' ⟶ G) (hγ : α ≫ whiskerLeft L γ₁ = α ≫ whiskerLeft L γ₂) :
γ₁ = γ₂ :=
(F'.isUniversalOfIsLeftKanExtension α).hom_ext hγ
