English
If the hypotheses ensure the existence of pointwise left Kan extensions along L for all F, then the Lan unit is an isomorphism in the target functor category. In other words, L defines a coreflective situation for the functor L with respect to the pointwise left Kan extensions.
Русский
Если выполняются условия существования точечного левого канонического расширения вдоль L для всех F, то единичный натурализованный преобразователь Lan является изоморфизмом. Другими словами, L задаёт ситуацию корефлексии относительно точечных левых канонических расширений.
LaTeX
$$$ \\forall F:\\, C \\to H,\\; \\operatorname{HasPointwiseLeftKanExtension}L F \\Rightarrow \\operatorname{IsIso}(L.\\mathrm{lanUnit}).$$$
Lean4
instance coreflective [∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] : IsIso (L.lanUnit (H := H)) := by
apply NatIso.isIso_of_isIso_app _
