English
For every F : C → H, if there is a pointwise left Kan extension of F along L and LeftKanExtensions exist for all F, then the unit at F of the lanAdjunction is an isomorphism.
Русский
Для каждого F : C → H, если существует точечное левое каноническое расширение F вдоль L и существуют левые канонические расширения для всех F, то единица lanAdjunction на F является изоморфизмом.
LaTeX
$$$ \\forall F:\\, C \\to H,\\; \\operatorname{HasPointwiseLeftKanExtension} L F \\land \\forall G:\\, C \\to H, \\operatorname{HasLeftKanExtension} L G \\Rightarrow \\operatorname{IsIso}((L.\\mathrm{lanAdjunction} H).\\mathrm{unit}.app F). $$$
Lean4
instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
IsIso ((L.lanAdjunction H).unit.app F) := by
rw [lanAdjunction_unit]
infer_instance
