English
If (F', α) is a left Kan extension of F along L, then for every G there is a natural bijection (F' ⇒ G) ≃ (F ⇒ L ⇒ G). The bijection is given by β ↦ α ≫ whiskerLeft β with inverse provided by descOfIsLeftKanExtension.
Русский
Если (F', α) является левой канонической проекции F вдоль L, то для любого G существует натуральная биекция (F' ⇒ G) ≃ (F ⇒ L ⇒ G). Биекция задаётся β ↦ α ≫ whiskerLeft β с обратной операцией, заданной descOfIsLeftKanExtension.
LaTeX
$$$\exists\; \text{Equiv}(F' ⟶ G, F ⟶ L ∘ G)$,\; \text{with } toFun(β) = α ≫ \mathrm{whiskerLeft}_- (β),\; invFun(β) = \mathrm{descOfIsLeftKanExtension}(-, α, -, β)$$$
Lean4
/-- If `(F', α)` is a left Kan extension of `F` along `L`, then this
is the induced bijection `(F' ⟶ G) ≃ (F ⟶ L ⋙ G)` for all `G`. -/
@[simps!]
noncomputable def homEquivOfIsLeftKanExtension (G : D ⥤ H) : (F' ⟶ G) ≃ (F ⟶ L ⋙ G)
where
toFun β := α ≫ whiskerLeft _ β
invFun β := descOfIsLeftKanExtension _ α _ β
left_inv β := Functor.hom_ext_of_isLeftKanExtension _ α _ _ (by simp)
right_inv := by cat_disch
