English
If F has a pointwise right derived functor with respect to W, then F possesses a right derived functor in the usual sense.
Русский
Если F имеет точечную правую производную по W, то она существует в обычном смысле.
LaTeX
$$[F.HasPointwiseRightDerivedFunctor(W)] \Rightarrow [F.HasRightDerivedFunctor(W)]$$
Lean4
theorem hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor : F.HasRightDerivedFunctor W where
hasLeftKanExtension' :=
by
have := F.hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor W.Q W
infer_instance
