English
If L is a localization of C with respect to W and F has a pointwise right derived functor for W, then the pointwise left Kan extension of F along L exists.
Русский
Если L является локализацией C по отношению к W и F имеет точечную правую производную по W, тогда существует точечное левое Кан-пространение функторa F вдоль L.
LaTeX
$$[L.IsLocalization(W)] \Rightarrow [F.HasPointwiseRightDerivedFunctor(W)] \Rightarrow \mathrm{HasPointwiseLeftKanExtension}(L,F)$$
Lean4
theorem hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor [L.IsLocalization W] :
HasPointwiseLeftKanExtension L F := fun Y ↦
by
have := Localization.essSurj L W
rw [← hasPointwiseLeftKanExtensionAt_iff_of_iso _ F (L.objObjPreimageIso Y), ←
F.hasPointwiseRightDerivedFunctorAt_iff L W]
infer_instance
